3SAT FO-reduces to SAT

This file constructs a first-order reduction from 3SAT to SAT, DescriptiveComplexity.threeSat_fo_reduction_sat : ThreeSAT ≤ᶠᵒ SAT, over the identity of vocabularies. The point of the reduction is the width bound: a 3SAT instance is a SAT instance plus the promise that every clause has at most three literals, and the promise is checked by a closed first-order sentence.

The interpretation (DescriptiveComplexity.ThreeSatToSat.threeSatToSat) is identity-like – one tag, dimension one – with all relation formulas gated on the sentence DescriptiveComplexity.ThreeSatToSat.wideS (“some clause has at least four distinct literal occurrences”):

• if the input is not wide, the output is a copy of the input, so the output is satisfiable iff the input is (and the width promise holds);
• if the input is wide, every element of the output becomes an empty clause, so the output is unsatisfiable, matching the violated promise.

The order is not needed: this is an order-free FO reduction (though not a quantifier-free one, since wideS quantifies over clauses and occurrences).

Order-free formulas over the vocabulary of CNF instances

def DescriptiveComplexity.ThreeSatToSat.clF {α : Type} (c : α) : FirstOrder.Language.sat.Formula α

c is a clause, as a formula.

Equations

• DescriptiveComplexity.ThreeSatToSat.clF c = FirstOrder.Language.satIsClause.formula₁ (FirstOrder.Language.var c)

def DescriptiveComplexity.ThreeSatToSat.posF {α : Type} (c x : α) : FirstOrder.Language.sat.Formula α

x occurs positively in c, as a formula.

Equations

• DescriptiveComplexity.ThreeSatToSat.posF c x = FirstOrder.Language.satPosIn.formula₂ (FirstOrder.Language.var c) (FirstOrder.Language.var x)

def DescriptiveComplexity.ThreeSatToSat.negF {α : Type} (c x : α) : FirstOrder.Language.sat.Formula α

x occurs negatively in c, as a formula.

Equations

• DescriptiveComplexity.ThreeSatToSat.negF c x = FirstOrder.Language.satNegIn.formula₂ (FirstOrder.Language.var c) (FirstOrder.Language.var x)

def DescriptiveComplexity.ThreeSatToSat.eqF {α : Type} (x y : α) : FirstOrder.Language.sat.Formula α

x = y, as a formula.

Equations

• DescriptiveComplexity.ThreeSatToSat.eqF x y = (FirstOrder.Language.var x).equal (FirstOrder.Language.var y)

def DescriptiveComplexity.ThreeSatToSat.occF {α : Type} (s : Bool) (c x : α) : FirstOrder.Language.sat.Formula α

The literal (x, s) occurs in the clause c, as a formula.

Equations

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

noncomputable def DescriptiveComplexity.ThreeSatToSat.wideS : FirstOrder.Language.sat.Sentence

Some clause has at least four distinct literal occurrences, as a sentence: the clause is variable 0 and the four occurrence variables are 1, …, 4; the disjunction ranges over the sign vectors, and distinctness is only required between occurrences carrying the same sign.

Equations

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

@[simp]

theorem DescriptiveComplexity.ThreeSatToSat.realize_clF {A : Type} [FirstOrder.Language.sat.Structure A] {α : Type} {v : α → A} {c : α} : (clF c).Realize v ↔ SatOcc.IsCl (v c)

@[simp]

theorem DescriptiveComplexity.ThreeSatToSat.realize_posF {A : Type} [FirstOrder.Language.sat.Structure A] {α : Type} {v : α → A} {c x : α} : (posF c x).Realize v ↔ SatOcc.PosIn (v c) (v x)

@[simp]

theorem DescriptiveComplexity.ThreeSatToSat.realize_negF {A : Type} [FirstOrder.Language.sat.Structure A] {α : Type} {v : α → A} {c x : α} : (negF c x).Realize v ↔ SatOcc.NegIn (v c) (v x)

@[simp]

theorem DescriptiveComplexity.ThreeSatToSat.realize_eqF {A : Type} [FirstOrder.Language.sat.Structure A] {α : Type} {v : α → A} {x y : α} : (eqF x y).Realize v ↔ v x = v y

@[simp]

theorem DescriptiveComplexity.ThreeSatToSat.realize_occF {A : Type} [FirstOrder.Language.sat.Structure A] {α : Type} {v : α → A} {s : Bool} {c x : α} : (occF s c x).Realize v ↔ SatOcc.OccIn (v c) (v x) s

def DescriptiveComplexity.ThreeSatToSat.Wide (A : Type) [FirstOrder.Language.sat.Structure A] : Prop

Some clause has at least four distinct literal occurrences. This is the negation of the width bound of 3SAT (wide_iff_not_widthAtMostThree).

Equations

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

theorem DescriptiveComplexity.ThreeSatToSat.wide_iff_not_widthAtMostThree (A : Type) [FirstOrder.Language.sat.Structure A] : Wide A ↔ ¬WidthAtMostThree A

@[simp]

theorem DescriptiveComplexity.ThreeSatToSat.realize_wideS (A : Type) [FirstOrder.Language.sat.Structure A] {w : Empty → A} : FirstOrder.Language.Formula.Realize wideS w ↔ Wide A

Realization of the formula wideS (under any assignment of its – absent – free variables).

The same check over the ordered expansion

The reductions that build gadgets over SatOcc.satOrd (Max Cut, 1-in-SAT) gate themselves on the width check too, and need it as a formula of the ordered vocabulary.

noncomputable def DescriptiveComplexity.ThreeSatToSat.wideOrdF {α : Type} : SatOcc.satOrd.Formula α

Some clause has at least four distinct literal occurrences, as a formula over the ordered expansion: wideS read there.

Equations

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

@[simp]

theorem DescriptiveComplexity.ThreeSatToSat.realize_wideOrdF {α A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {v : α → A} : wideOrdF.Realize v ↔ Wide A

The interpretation

noncomputable def DescriptiveComplexity.ThreeSatToSat.threeSatToSat : FOInterpretation FirstOrder.Language.sat FirstOrder.Language.sat Unit 1

The identity-like interpretation of SAT instances in 3SAT instances, gated on the width check: a faithful copy if no clause is wide, an unsatisfiable structure made of empty clauses otherwise.

Equations

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

@[simp]

theorem DescriptiveComplexity.ThreeSatToSat.isClause_iff {A : Type} [FirstOrder.Language.sat.Structure A] (w : Fin 1 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![((), w)] ↔ SatOcc.IsCl (w 0) ∨ Wide A

@[simp]

theorem DescriptiveComplexity.ThreeSatToSat.posIn_iff {A : Type} [FirstOrder.Language.sat.Structure A] (wc wx : Fin 1 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![((), wc), ((), wx)] ↔ SatOcc.PosIn (wc 0) (wx 0) ∧ ¬Wide A

@[simp]

theorem DescriptiveComplexity.ThreeSatToSat.negIn_iff {A : Type} [FirstOrder.Language.sat.Structure A] (wc wx : Fin 1 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![((), wc), ((), wx)] ↔ SatOcc.NegIn (wc 0) (wx 0) ∧ ¬Wide A

Correctness

theorem DescriptiveComplexity.ThreeSatToSat.threeSatisfiable_iff_satisfiable (A : Type) [FirstOrder.Language.sat.Structure A] : ThreeSatisfiable A ↔ Satisfiable (threeSatToSat.Map A)

Correctness of the reduction: a CNF structure is a yes-instance of 3SAT iff the interpreted CNF structure is satisfiable.

noncomputable def DescriptiveComplexity.threeSat_fo_reduction_sat : FOReduction ThreeSAT SAT

3SAT FO-reduces to SAT. The identity-like interpretation ThreeSatToSat.threeSatToSat, gated on the first-order width check, maps a CNF structure to a satisfiable CNF instance iff it is a yes-instance of 3SAT.

Equations

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