NAE-3SAT ordered-FO-reduces to Max Cut

Correctness of the gadget of DescriptiveComplexity.Problems.MaxCut.Interp. The whole argument runs through one map, DescriptiveComplexity.MaxCutRed.cutMap, which charges every edge of the cut to a threshold unit:

• a cut variable edge is charged to the mark of its element;
• a cut occurrence edge is charged to the mark of its occurrence;
• a cut clause edge {u, v} of a clause c is charged to whichever of u, v is not the last occurrence of c – the tie, when neither is, broken towards the side the last occurrence lies on.

The map is injective on the cut (DescriptiveComplexity.MaxCutRed.cutMap_injOn), and this is exactly where the width bound is used: two cut clause edges with the same charge would give four distinct occurrences of one clause, two on each side of the cut. Injectivity gives cut ≤ threshold for every S.

Conversely, given a not-all-equal assignment, the side that puts a literal vertex with its literal and an occurrence vertex with the negation of its literal makes the map hit every mark (DescriptiveComplexity.MaxCutRed.marked_subset_image), so threshold ≤ cut.

Both halves together say that a cut reaches the threshold iff it is “perfect”: every variable edge cut (which reads off an assignment), every occurrence edge cut (which ties the occurrence vertices to it), and every clause gadget non-monochromatic (which is not-all-equal satisfaction). The penalty marks of clauses with at most one occurrence are never charged, which is what rules those clauses out – as it must, since such a clause is never not-all-equal satisfiable.

Occurrence bookkeeping

theorem DescriptiveComplexity.MaxCutRed.maxOcc_unique {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c x y : A} {s t : Bool} (h₁ : SatOcc.MaxOcc c x s) (h₂ : SatOcc.MaxOcc c y t) : x = y ∧ s = t

The last occurrence of a clause is unique.

noncomputable def DescriptiveComplexity.MaxCutRed.maxVert {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c : A) : MaxCutInterp.mcInterp.Map A

The occurrence vertex of the last occurrence of c (a penalty vertex if c has no occurrence at all).

Equations

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

theorem DescriptiveComplexity.MaxCutRed.maxVert_eq {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c x : A} {s : Bool} (h : SatOcc.MaxOcc c x s) : maxVert c = MaxCutInterp.occPt s c x

theorem DescriptiveComplexity.MaxCutRed.no_four_occPt {A : Type} [FirstOrder.Language.sat.Structure A] (hwidth : WidthAtMostThree A) {c : A} {v₁ v₂ v₃ v₄ : MaxCutInterp.mcInterp.Map A} (h₁ : ∃ (x : A) (s : Bool), SatOcc.OccIn c x s ∧ v₁ = MaxCutInterp.occPt s c x) (h₂ : ∃ (x : A) (s : Bool), SatOcc.OccIn c x s ∧ v₂ = MaxCutInterp.occPt s c x) (h₃ : ∃ (x : A) (s : Bool), SatOcc.OccIn c x s ∧ v₃ = MaxCutInterp.occPt s c x) (h₄ : ∃ (x : A) (s : Bool), SatOcc.OccIn c x s ∧ v₄ = MaxCutInterp.occPt s c x) (h₁₂ : v₁ ≠ v₂) (h₁₃ : v₁ ≠ v₃) (h₁₄ : v₁ ≠ v₄) (h₂₃ : v₂ ≠ v₃) (h₂₄ : v₂ ≠ v₄) (h₃₄ : v₃ ≠ v₄) : False

No clause has four distinct occurrence vertices: the width bound, read on the gadget.

theorem DescriptiveComplexity.MaxCutRed.atMostOne_iff_noChained {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {c : A} : (∀ (x : A) (s : Bool) (y : A) (t : Bool), SatOcc.OccIn c x s → SatOcc.OccIn c y t → x = y ∧ s = t) ↔ ∀ (x : A) (s : Bool), ¬SatOcc.Chained c x s

A clause has at most one occurrence exactly when none of its occurrences is a non-first one – the first-order form the marks use.

theorem DescriptiveComplexity.MaxCutRed.exists_maxVert {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {c x : A} {s : Bool} (h : SatOcc.OccIn c x s) : ∃ (y : A) (t : Bool), SatOcc.MaxOcc c y t ∧ maxVert c = MaxCutInterp.occPt t c y

The vertex of the last occurrence, as an occurrence vertex.

Charging a cut edge to a threshold unit

def DescriptiveComplexity.MaxCutRed.cutSet {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (S : MaxCutInterp.mcInterp.Map A → Prop) : Set (MaxCutInterp.mcInterp.Map A × MaxCutInterp.mcInterp.Map A)

The cut of the gadget graph determined by S, as a set of pairs.

Equations

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

def DescriptiveComplexity.MaxCutRed.markSet {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] : Set (MaxCutInterp.mcInterp.Map A × MaxCutInterp.mcInterp.Map A)

The threshold, as a set of pairs.

Equations

• DescriptiveComplexity.MaxCutRed.markSet = {p : DescriptiveComplexity.MaxCutInterp.mcInterp.Map A × DescriptiveComplexity.MaxCutInterp.mcInterp.Map A | DescriptiveComplexity.MAGMarked p.1 p.2}

@[simp]

theorem DescriptiveComplexity.MaxCutRed.mem_cutSet {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {S : MaxCutInterp.mcInterp.Map A → Prop} {p : MaxCutInterp.mcInterp.Map A × MaxCutInterp.mcInterp.Map A} : p ∈ cutSet S ↔ MAGAdj p.1 p.2 ∧ S p.1 ∧ ¬S p.2

@[simp]

theorem DescriptiveComplexity.MaxCutRed.mem_markSet {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {p : MaxCutInterp.mcInterp.Map A × MaxCutInterp.mcInterp.Map A} : p ∈ markSet ↔ MAGMarked p.1 p.2

noncomputable def DescriptiveComplexity.MaxCutRed.pick {A : Type} (S : MaxCutInterp.mcInterp.Map A → Prop) (u v m : MaxCutInterp.mcInterp.Map A) : MaxCutInterp.mcInterp.Map A

The endpoint of a clause edge that the threshold unit is charged to.

Equations

• DescriptiveComplexity.MaxCutRed.pick S u v m = if S m then if u = m then v else u else if v = m then u else v

theorem DescriptiveComplexity.MaxCutRed.pick_cases {A : Type} {S : MaxCutInterp.mcInterp.Map A → Prop} {u v m : MaxCutInterp.mcInterp.Map A} (huv : u ≠ v) : (pick S u v m = u ∨ pick S u v m = v) ∧ pick S u v m ≠ m

theorem DescriptiveComplexity.MaxCutRed.pick_left {A : Type} {S : MaxCutInterp.mcInterp.Map A → Prop} {u v m : MaxCutInterp.mcInterp.Map A} (hm : S m) (h : u ≠ m) : pick S u v m = u

theorem DescriptiveComplexity.MaxCutRed.pick_right {A : Type} {S : MaxCutInterp.mcInterp.Map A → Prop} {u v m : MaxCutInterp.mcInterp.Map A} (hm : ¬S m) (h : v ≠ m) : pick S u v m = v

theorem DescriptiveComplexity.MaxCutRed.pick_of_left_eq {A : Type} {S : MaxCutInterp.mcInterp.Map A → Prop} {v m : MaxCutInterp.mcInterp.Map A} (hm : S m) : pick S m v m = v

theorem DescriptiveComplexity.MaxCutRed.pick_of_right_eq {A : Type} {S : MaxCutInterp.mcInterp.Map A → Prop} {u m : MaxCutInterp.mcInterp.Map A} (hm : ¬S m) : pick S u m m = u

noncomputable def DescriptiveComplexity.MaxCutRed.cutMap {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (S : MaxCutInterp.mcInterp.Map A → Prop) (p : MaxCutInterp.mcInterp.Map A × MaxCutInterp.mcInterp.Map A) : MaxCutInterp.mcInterp.Map A × MaxCutInterp.mcInterp.Map A

The charge map: every edge of the cut is charged to a threshold unit.

Equations

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

@[simp]

theorem DescriptiveComplexity.MaxCutRed.cutMap_lit_lit {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (S : MaxCutInterp.mcInterp.Map A → Prop) (s t : Bool) (x y : A) : cutMap S (MaxCutInterp.litPt s x, MaxCutInterp.litPt t y) = (MaxCutInterp.litPt true x, MaxCutInterp.litPt false x)

@[simp]

theorem DescriptiveComplexity.MaxCutRed.cutMap_occ_lit {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (S : MaxCutInterp.mcInterp.Map A → Prop) (s t : Bool) (c x y : A) : cutMap S (MaxCutInterp.occPt s c x, MaxCutInterp.litPt t y) = (MaxCutInterp.occPt s c x, MaxCutInterp.litPt s x)

@[simp]

theorem DescriptiveComplexity.MaxCutRed.cutMap_lit_occ {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (S : MaxCutInterp.mcInterp.Map A → Prop) (s t : Bool) (c x y : A) : cutMap S (MaxCutInterp.litPt s x, MaxCutInterp.occPt t c y) = (MaxCutInterp.occPt t c y, MaxCutInterp.litPt t y)

@[simp]

theorem DescriptiveComplexity.MaxCutRed.cutMap_occ_occ {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (S : MaxCutInterp.mcInterp.Map A → Prop) (s t : Bool) (c d x y : A) : cutMap S (MaxCutInterp.occPt s c x, MaxCutInterp.occPt t d y) = (pick S (MaxCutInterp.occPt s c x) (MaxCutInterp.occPt t d y) (maxVert c), maxVert c)

theorem DescriptiveComplexity.MaxCutRed.cut_charge {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {S : MaxCutInterp.mcInterp.Map A → Prop} {p : MaxCutInterp.mcInterp.Map A × MaxCutInterp.mcInterp.Map A} (hp : p ∈ cutSet S) : (∃ (x : A), cutMap S p = (MaxCutInterp.litPt true x, MaxCutInterp.litPt false x) ∧ (p = (MaxCutInterp.litPt true x, MaxCutInterp.litPt false x) ∨ p = (MaxCutInterp.litPt false x, MaxCutInterp.litPt true x))) ∨ (∃ (s : Bool) (c : A) (x : A), SatOcc.OccIn c x s ∧ cutMap S p = (MaxCutInterp.occPt s c x, MaxCutInterp.litPt s x) ∧ (p = (MaxCutInterp.occPt s c x, MaxCutInterp.litPt s x) ∨ p = (MaxCutInterp.litPt s x, MaxCutInterp.occPt s c x))) ∨ ∃ (s : Bool) (t : Bool) (u : Bool) (c : A) (x : A) (y : A) (z : A), SatOcc.OccIn c x s ∧ SatOcc.OccIn c y t ∧ SatOcc.MaxOcc c z u ∧ ¬(x = y ∧ s = t) ∧ p = (MaxCutInterp.occPt s c x, MaxCutInterp.occPt t c y) ∧ cutMap S p = (pick S (MaxCutInterp.occPt s c x) (MaxCutInterp.occPt t c y) (MaxCutInterp.occPt u c z), MaxCutInterp.occPt u c z)

Every edge of the cut, with its charge in explicit form.

theorem DescriptiveComplexity.MaxCutRed.cutMap_mapsTo {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] (S : MaxCutInterp.mcInterp.Map A → Prop) : Set.MapsTo (cutMap S) (cutSet S) markSet

The charge map sends the cut into the threshold.

theorem DescriptiveComplexity.MaxCutRed.cutMap_injOn {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] (hwidth : WidthAtMostThree A) (S : MaxCutInterp.mcInterp.Map A → Prop) : Set.InjOn (cutMap S) (cutSet S)

The charge map is injective on the cut. This is where the width bound is used: two clause edges with the same charge would exhibit four distinct occurrences of one clause.

The side of the cut given by an assignment

def DescriptiveComplexity.MaxCutRed.cutSide {A : Type} (ν : A → Prop) (p : MaxCutInterp.mcInterp.Map A) : Prop

The side of the cut determined by an assignment: a literal vertex takes the value of its literal, an occurrence vertex the negation of its literal, and the penalty vertices are outside.

Equations

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

@[simp]

theorem DescriptiveComplexity.MaxCutRed.cutSide_lit {A : Type} (ν : A → Prop) (s : Bool) (x : A) : cutSide ν (MaxCutInterp.litPt s x) ↔ SatOcc.LitTrue ν x s

@[simp]

theorem DescriptiveComplexity.MaxCutRed.cutSide_occ {A : Type} (ν : A → Prop) (s : Bool) (c x : A) : cutSide ν (MaxCutInterp.occPt s c x) ↔ ¬SatOcc.LitTrue ν x s

theorem DescriptiveComplexity.MaxCutRed.marked_subset_image {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] (hw : ¬ThreeSatToSat.Wide A) {ν : A → Prop} (hν : NAEProper ν) : markSet ⊆ cutMap (cutSide ν) '' cutSet (cutSide ν)

Given a not-all-equal assignment, the charge map hits every threshold unit, so the cut is at least as large as the threshold.

Correctness

theorem DescriptiveComplexity.MaxCutRed.naeThreeSatisfiable_iff_hasLargeCut (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] : NAEThreeSatisfiable A ↔ HasLargeCut (MaxCutInterp.mcInterp.Map A)

Correctness of the reduction: a CNF structure is a yes-instance of NAE-3SAT iff its gadget graph has a cut at least as large as its marked relation.

noncomputable def DescriptiveComplexity.MaxCutRed.nae3Sat_ordered_fo_reduction_maxCut : OrderedFOReduction NAE3SAT MaxCut

NAE-3SAT ordered-FO-reduces to Max Cut: the gadget graph, whose cut reaches the threshold exactly when the clauses are not-all-equal satisfiable.

Equations

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