Expanderizing a constraint system

The second half of Dinur's preprocessing. Degree reduction makes the graph regular; this step makes it an expander, by superposing a member of an ExpanderFamily whose edges carry the trivially true constraint.

Adding constraints that are never violated cannot create unsatisfiability, and it cannot destroy it either: the broken darts are exactly the old ones, while the total number of darts grows from order · deg to order · (deg + E.degree). So the value is scaled by exactly deg / (deg + E.degree) — a constant factor, since both degrees are constants after degree reduction — and satisfiability is unchanged. The spectral bound is inherited from spectralBound_union.

Main definitions

• RegCSP.addTrivial — superpose a graph's edges with trivial constraints
• RegCSP.expanderize — the case of a family expander

Main results

• RegCSP.card_unsatDarts_addTrivial — the broken darts are unchanged
• RegCSP.unsatFrac_addTrivial, unsatVal_addTrivial — the value scales by deg / (deg + deg')
• RegCSP.satisfiable_addTrivial_iff
• RegCSP.spectralBound_expanderize — the result is an expander

def Complexity.RegCSP.addTrivial {α : Type} (R : RegCSP α) (H : RegGraph) (e : H.V ≃ R.graph.V) : RegCSP α

R with the edges of H superposed, carrying the trivially true constraint.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Complexity.RegCSP.graph_addTrivial {α : Type} (R : RegCSP α) (H : RegGraph) (e : H.V ≃ R.graph.V) : (R.addTrivial H e).graph = R.graph.union H e

theorem Complexity.RegCSP.card_unsatDarts_addTrivial {α : Type} (R : RegCSP α) (H : RegGraph) (e : H.V ≃ R.graph.V) (a : R.Assignment) : ((R.addTrivial H e).unsatDarts a).card = (R.unsatDarts a).card

Only the original constraints can fail.

theorem Complexity.RegCSP.unsatFrac_addTrivial {α : Type} (R : RegCSP α) (H : RegGraph) (e : H.V ≃ R.graph.V) (a : R.Assignment) : (R.addTrivial H e).unsatFrac a = R.unsatFrac a * ↑R.graph.deg / (↑R.graph.deg + ↑H.deg)

Superposing trivial constraints scales the value by deg / (deg + deg').

theorem Complexity.RegCSP.unsatVal_addTrivial {α : Type} (R : RegCSP α) (H : RegGraph) (e : H.V ≃ R.graph.V) [Fintype α] [Nonempty α] : (R.addTrivial H e).unsatVal = R.unsatVal * ↑R.graph.deg / (↑R.graph.deg + ↑H.deg)

The scaling passes to the value, since it is the same factor for every assignment and the assignments are the same.

theorem Complexity.RegCSP.satisfiable_addTrivial_iff {α : Type} (R : RegCSP α) (H : RegGraph) (e : H.V ≃ R.graph.V) : (R.addTrivial H e).Satisfiable ↔ R.Satisfiable

noncomputable def Complexity.RegCSP.expanderize {α : Type} (R : RegCSP α) [NumEnc R.graph.V] (E : ExpanderFamily) : RegCSP α

R with a family expander superposed.

Equations

• R.expanderize E = R.addTrivial (E.graph R.graph.order) (E.vertexEquiv R.graph)

@[simp]

theorem Complexity.RegCSP.graph_expanderize {α : Type} (R : RegCSP α) [NumEnc R.graph.V] (E : ExpanderFamily) : (R.expanderize E).graph = E.expanderize R.graph

theorem Complexity.RegCSP.spectralBound_expanderize {α : Type} (R : RegCSP α) [NumEnc R.graph.V] (E : ExpanderFamily) : (R.expanderize E).graph.SpectralBound ((↑R.graph.deg + ↑E.degree * E.lam) / (↑R.graph.deg + ↑E.degree))

The expanderized system is an expander.

theorem Complexity.RegCSP.unsatFrac_expanderize {α : Type} (R : RegCSP α) [NumEnc R.graph.V] (E : ExpanderFamily) (a : R.Assignment) : (R.expanderize E).unsatFrac a = R.unsatFrac a * ↑R.graph.deg / (↑R.graph.deg + ↑E.degree)

theorem Complexity.RegCSP.unsatVal_expanderize {α : Type} (R : RegCSP α) [Fintype α] [Nonempty α] [NumEnc R.graph.V] (E : ExpanderFamily) : (R.expanderize E).unsatVal = R.unsatVal * ↑R.graph.deg / (↑R.graph.deg + ↑E.degree)

theorem Complexity.RegCSP.satisfiable_expanderize_iff {α : Type} (R : RegCSP α) [NumEnc R.graph.V] (E : ExpanderFamily) : (R.expanderize E).Satisfiable ↔ R.Satisfiable