The gadget graph of the reduction from NAE-3SAT to Max Cut

This file builds the interpretation DescriptiveComplexity.MaxCutInterp.mcInterp of Max Cut instances in ordered CNF instances, and characterizes its two relations. The correctness of the reduction is in DescriptiveComplexity.Problems.MaxCut.Reduction.

The gadget

Vertices come in three tags over pairs (Fin 2 → A):

• litPt s x, the literal vertex of (x, s), on diagonal pairs;
• occPt s c x, the occurrence vertex of the occurrence (x, s) of the clause c;
• penPt c, an isolated penalty vertex, used only to carry a threshold unit.

and edges in three families:

• litPt s x — litPt (!s) x, one per element of the universe;
• occPt s c x — litPt s x, one per occurrence;
• occPt s c x — occPt t c y, for distinct occurrences of the same clause.

The threshold marks one pair per element (the variable edge), one pair per occurrence (the occurrence edge), one pair per non-maximal occurrence of a clause (charged against the maximal one, so k − 1 per clause of width k), and one pair per clause with at most one occurrence – a penalty, since such a clause is never not-all-equal satisfiable while its gadget carries no edge at all.

Two design points are worth recording.

• Giving every occurrence its own vertex, joined to its literal vertex by a single edge, is what makes the three edge families live on disjoint pairs of tags, hence edge-disjoint: putting the clause gadgets directly on literal vertices would let two clauses over the same two literals share an edge, and a clause containing both x and ¬x reuse a variable edge, and the count would break. The occurrence vertex then carries the negation of its literal, which is harmless: not-all-equal satisfaction is invariant under flipping all the literals of a clause.
• No edge weight or multiplicity is needed anywhere. The cut splits as a sum over the three families, each maximal on its own, so a single edge per variable already forces the two literal vertices apart.

Everything is gated on the first-order width check ThreeSatToSat.Wide, as in the reduction of 3SAT to SAT: on a wide input the graph has no edge at all, while the threshold stays positive, so the output is a no-instance. The gate is what makes the per-clause budget k − 1 an upper bound, a clique on k vertices having a larger cut as soon as k ≥ 4.

inductive DescriptiveComplexity.MaxCutInterp.MCTag : Type

Tags for the gadget graph: literal vertices, occurrence vertices, and the isolated penalty vertices carrying a threshold unit for degenerate clauses.

• lit (s : Bool) : MCTag

  litPt s x is the vertex of the literal (x, s).

• occ (s : Bool) : MCTag

  occPt s c x is the vertex of the occurrence (x, s) of the clause c.

• pen : MCTag

  penPt c is the isolated penalty vertex of the clause c.

@[instance_reducible]

instance DescriptiveComplexity.MaxCutInterp.instDecidableEqMCTag : DecidableEq MCTag

Equations

• DescriptiveComplexity.MaxCutInterp.instDecidableEqMCTag = DescriptiveComplexity.MaxCutInterp.instDecidableEqMCTag.decEq

def DescriptiveComplexity.MaxCutInterp.instDecidableEqMCTag.decEq (x✝ x✝¹ : MCTag) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.MaxCutInterp.instDecidableEqMCTag.decEq (DescriptiveComplexity.MaxCutInterp.MCTag.lit s) (DescriptiveComplexity.MaxCutInterp.MCTag.occ s_1) = isFalse ⋯
• DescriptiveComplexity.MaxCutInterp.instDecidableEqMCTag.decEq (DescriptiveComplexity.MaxCutInterp.MCTag.lit s) DescriptiveComplexity.MaxCutInterp.MCTag.pen = isFalse ⋯
• DescriptiveComplexity.MaxCutInterp.instDecidableEqMCTag.decEq (DescriptiveComplexity.MaxCutInterp.MCTag.occ s) (DescriptiveComplexity.MaxCutInterp.MCTag.lit s_1) = isFalse ⋯
• DescriptiveComplexity.MaxCutInterp.instDecidableEqMCTag.decEq (DescriptiveComplexity.MaxCutInterp.MCTag.occ s) DescriptiveComplexity.MaxCutInterp.MCTag.pen = isFalse ⋯
• DescriptiveComplexity.MaxCutInterp.instDecidableEqMCTag.decEq DescriptiveComplexity.MaxCutInterp.MCTag.pen (DescriptiveComplexity.MaxCutInterp.MCTag.lit s) = isFalse ⋯
• DescriptiveComplexity.MaxCutInterp.instDecidableEqMCTag.decEq DescriptiveComplexity.MaxCutInterp.MCTag.pen (DescriptiveComplexity.MaxCutInterp.MCTag.occ s) = isFalse ⋯
• DescriptiveComplexity.MaxCutInterp.instDecidableEqMCTag.decEq DescriptiveComplexity.MaxCutInterp.MCTag.pen DescriptiveComplexity.MaxCutInterp.MCTag.pen = isTrue ⋯

@[instance_reducible]

instance DescriptiveComplexity.MaxCutInterp.instFintypeMCTag : Fintype MCTag

Equations

• DescriptiveComplexity.MaxCutInterp.instFintypeMCTag = Fintype.ofEquiv (Bool ⊕ Bool ⊕ Unit) DescriptiveComplexity.MaxCutInterp.MCTag.proxyTypeEquiv

instance DescriptiveComplexity.MaxCutInterp.instNonemptyMCTag : Nonempty MCTag

Two more formulas over the ordered expansion

noncomputable def DescriptiveComplexity.MaxCutInterp.noChainedF {α : Type} (c : α) : SatOcc.satOrd.Formula α

No occurrence of c is a non-first one, as a formula: this says exactly that the clause c has at most one occurrence.

Equations

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

@[simp]

theorem DescriptiveComplexity.MaxCutInterp.realize_noChainedF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {c : α} : (noChainedF c).Realize v ↔ ∀ (x : A) (s : Bool), ¬SatOcc.Chained (v c) x s

The interpretation

noncomputable def DescriptiveComplexity.MaxCutInterp.adjF : MCTag → MCTag → SatOcc.satOrd.Formula (Fin 2 × Fin 2)

Defining formula for adjacency, before the width gate: the three edge families.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.MaxCutInterp.adjF x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.MaxCutInterp.markF : MCTag → MCTag → SatOcc.satOrd.Formula (Fin 2 × Fin 2)

Defining formula for the threshold marks: one pair per element, one per occurrence, one per non-maximal occurrence, one per degenerate clause.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.MaxCutInterp.markF x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.MaxCutInterp.mcInterp : FOInterpretation SatOcc.satOrd FirstOrder.Language.markedArcGraph MCTag 2

The interpretation of Max Cut instances in ordered CNF instances: the gadget graph, with every edge gated on the width check.

Equations

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

The vertices

def DescriptiveComplexity.MaxCutInterp.litPt {A : Type} (s : Bool) (x : A) : mcInterp.Map A

The literal vertex of (x, s).

Equations

• DescriptiveComplexity.MaxCutInterp.litPt s x = (DescriptiveComplexity.MaxCutInterp.MCTag.lit s, fun (x_1 : Fin 2) => x)

def DescriptiveComplexity.MaxCutInterp.occPt {A : Type} (s : Bool) (c x : A) : mcInterp.Map A

The occurrence vertex of the occurrence (x, s) of c.

Equations

• DescriptiveComplexity.MaxCutInterp.occPt s c x = (DescriptiveComplexity.MaxCutInterp.MCTag.occ s, ![c, x])

def DescriptiveComplexity.MaxCutInterp.penPt {A : Type} (c : A) : mcInterp.Map A

The penalty vertex of the clause c.

Equations

• DescriptiveComplexity.MaxCutInterp.penPt c = (DescriptiveComplexity.MaxCutInterp.MCTag.pen, fun (x : Fin 2) => c)

theorem DescriptiveComplexity.MaxCutInterp.litPt_eq_iff {A : Type} {s t : Bool} {x y : A} : litPt s x = litPt t y ↔ s = t ∧ x = y

theorem DescriptiveComplexity.MaxCutInterp.occPt_eq_iff {A : Type} {s t : Bool} {c d x y : A} : occPt s c x = occPt t d y ↔ s = t ∧ c = d ∧ x = y

theorem DescriptiveComplexity.MaxCutInterp.litPt_ne_occPt {A : Type} {s t : Bool} {c x y : A} : litPt s x ≠ occPt t c y

theorem DescriptiveComplexity.MaxCutInterp.litPt_ne_penPt {A : Type} {s : Bool} {c x : A} : litPt s x ≠ penPt c

theorem DescriptiveComplexity.MaxCutInterp.occPt_ne_penPt {A : Type} {s : Bool} {c d x : A} : occPt s c x ≠ penPt d

@[simp]

theorem DescriptiveComplexity.MaxCutInterp.litPt_eq_occPt_iff {A : Type} {s t : Bool} {c x y : A} : litPt s x = occPt t c y ↔ False

@[simp]

theorem DescriptiveComplexity.MaxCutInterp.occPt_eq_litPt_iff {A : Type} {s t : Bool} {c x y : A} : occPt t c y = litPt s x ↔ False

@[simp]

theorem DescriptiveComplexity.MaxCutInterp.litPt_eq_penPt_iff {A : Type} {s : Bool} {c x : A} : litPt s x = penPt c ↔ False

@[simp]

theorem DescriptiveComplexity.MaxCutInterp.penPt_eq_litPt_iff {A : Type} {s : Bool} {c x : A} : penPt c = litPt s x ↔ False

@[simp]

theorem DescriptiveComplexity.MaxCutInterp.occPt_eq_penPt_iff {A : Type} {s : Bool} {c d x : A} : occPt s c x = penPt d ↔ False

@[simp]

theorem DescriptiveComplexity.MaxCutInterp.penPt_eq_occPt_iff {A : Type} {s : Bool} {c d x : A} : penPt d = occPt s c x ↔ False

theorem DescriptiveComplexity.MaxCutInterp.litPt_eta {A : Type} {s : Bool} {w : Fin 2 → A} (h : w 0 = w 1) : (MCTag.lit s, w) = litPt s (w 0)

theorem DescriptiveComplexity.MaxCutInterp.occPt_eta {A : Type} {s : Bool} {w : Fin 2 → A} : (MCTag.occ s, w) = occPt s (w 0) (w 1)

theorem DescriptiveComplexity.MaxCutInterp.penPt_eta {A : Type} {w : Fin 2 → A} (h : w 0 = w 1) : (MCTag.pen, w) = penPt (w 0)

Characterization of the two relations

def DescriptiveComplexity.MaxCutInterp.AdjShape {A : Type} [FirstOrder.Language.sat.Structure A] : MCTag → MCTag → (Fin 2 → A) → (Fin 2 → A) → Prop

The shape of an edge, read on tags and coordinates.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.MaxCutInterp.AdjShape x✝³ x✝² x✝¹ x✝ = False

def DescriptiveComplexity.MaxCutInterp.MarkShape {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] : MCTag → MCTag → (Fin 2 → A) → (Fin 2 → A) → Prop

The shape of a threshold mark, read on tags and coordinates.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.MaxCutInterp.MarkShape x✝³ x✝² x✝¹ x✝ = False

theorem DescriptiveComplexity.MaxCutInterp.adj_iff_aux {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (t₁ t₂ : MCTag) (w₁ w₂ : Fin 2 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.magAdj ![(t₁, w₁), (t₂, w₂)] ↔ ¬ThreeSatToSat.Wide A ∧ AdjShape t₁ t₂ w₁ w₂

The edges of the gadget graph, on tagged tuples.

theorem DescriptiveComplexity.MaxCutInterp.marked_iff_aux {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (t₁ t₂ : MCTag) (w₁ w₂ : Fin 2 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.magMarked ![(t₁, w₁), (t₂, w₂)] ↔ MarkShape t₁ t₂ w₁ w₂

The threshold marks of the gadget graph, on tagged tuples.

theorem DescriptiveComplexity.MaxCutInterp.adj_cases {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {p q : mcInterp.Map A} (h : MAGAdj p q) : ¬ThreeSatToSat.Wide A ∧ ((∃ (s : Bool) (x : A), p = litPt s x ∧ q = litPt (!s) x) ∨ (∃ (s : Bool) (c : A) (x : A), SatOcc.OccIn c x s ∧ p = occPt s c x ∧ q = litPt s x) ∨ (∃ (s : Bool) (c : A) (x : A), SatOcc.OccIn c x s ∧ p = litPt s x ∧ q = occPt s c x) ∨ ∃ (s : Bool) (t : Bool) (c : A) (x : A) (y : A), SatOcc.OccIn c x s ∧ SatOcc.OccIn c y t ∧ ¬(x = y ∧ s = t) ∧ p = occPt s c x ∧ q = occPt t c y)

Every edge of the gadget graph belongs to one of the three families.

theorem DescriptiveComplexity.MaxCutInterp.marked_cases {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {p q : mcInterp.Map A} (h : MAGMarked p q) : (∃ (x : A), p = litPt true x ∧ q = litPt false x) ∨ (∃ (s : Bool) (c : A) (x : A), SatOcc.OccIn c x s ∧ p = occPt s c x ∧ q = litPt s x) ∨ (∃ (s : Bool) (t : Bool) (c : A) (x : A) (y : A), SatOcc.OccIn c x s ∧ SatOcc.MaxOcc c y t ∧ ¬(x = y ∧ s = t) ∧ p = occPt s c x ∧ q = occPt t c y) ∨ ∃ (c : A), SatOcc.IsCl c ∧ (∀ (x : A) (s : Bool), ¬SatOcc.Chained c x s) ∧ p = penPt c ∧ q = penPt c

Every threshold mark belongs to one of the four families.

theorem DescriptiveComplexity.MaxCutInterp.adj_lit_lit {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (hw : ¬ThreeSatToSat.Wide A) {s t : Bool} (hst : s ≠ t) (x : A) : MAGAdj (litPt s x) (litPt t x)

The variable edge of an element.

theorem DescriptiveComplexity.MaxCutInterp.adj_occ_lit {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (hw : ¬ThreeSatToSat.Wide A) {s : Bool} {c x : A} (h : SatOcc.OccIn c x s) : MAGAdj (occPt s c x) (litPt s x)

The edge joining an occurrence vertex to its literal vertex.

theorem DescriptiveComplexity.MaxCutInterp.adj_lit_occ {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (hw : ¬ThreeSatToSat.Wide A) {s : Bool} {c x : A} (h : SatOcc.OccIn c x s) : MAGAdj (litPt s x) (occPt s c x)

The edge joining a literal vertex to an occurrence vertex.

theorem DescriptiveComplexity.MaxCutInterp.adj_occ_occ {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (hw : ¬ThreeSatToSat.Wide A) {s t : Bool} {c x y : A} (hx : SatOcc.OccIn c x s) (hy : SatOcc.OccIn c y t) (hne : ¬(x = y ∧ s = t)) : MAGAdj (occPt s c x) (occPt t c y)

The edges of the gadget of a clause.

theorem DescriptiveComplexity.MaxCutInterp.marked_lit {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (x : A) : MAGMarked (litPt true x) (litPt false x)

The threshold mark of an element.

theorem DescriptiveComplexity.MaxCutInterp.marked_occ_lit {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {s : Bool} {c x : A} (h : SatOcc.OccIn c x s) : MAGMarked (occPt s c x) (litPt s x)

The threshold mark of an occurrence.

theorem DescriptiveComplexity.MaxCutInterp.marked_tri {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {s t : Bool} {c x y : A} (hx : SatOcc.OccIn c x s) (hy : SatOcc.MaxOcc c y t) (hne : ¬(x = y ∧ s = t)) : MAGMarked (occPt s c x) (occPt t c y)

The threshold mark of a non-maximal occurrence, charged against the maximal occurrence of its clause.

theorem DescriptiveComplexity.MaxCutInterp.marked_pen {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c : A} (hcl : SatOcc.IsCl c) (hch : ∀ (x : A) (s : Bool), ¬SatOcc.Chained c x s) : MAGMarked (penPt c) (penPt c)

The penalty mark of a clause with at most one occurrence.