2SAT: definition

The problem 2SAT, over the same vocabulary FirstOrder.Language.sat as SAT and 3SAT: a CNF structure is a yes-instance iff every clause has at most two literal occurrences (DescriptiveComplexity.WidthAtMostTwo) and the CNF is satisfiable (DescriptiveComplexity.TwoSatisfiable, bundled as DescriptiveComplexity.TwoSAT).

As for 3SAT, folding the width bound into the yes-instances rather than into the vocabulary is what keeps 2SAT a decision problem on arbitrary Language.sat-structures, and the bound "at most two" is expressed without counting: among any three literal occurrences of a clause, two coincide.

Two facts about the bound are needed by the Krom program of DescriptiveComplexity.Problems.TwoSat.Membership, and both are here: the bound is first-order expressible over the ordered expansion (DescriptiveComplexity.wideTwoOrdF, its violation), and a clause of a width-two structure has two signed occurrences covering all of them (DescriptiveComplexity.exists_covering_pair), the shape a 2-clause can talk about.

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

Every clause of a Language.sat-structure has at most two literal occurrences: among any three occurrences of a clause, two coincide (as signed occurrences).

Equations

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

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

A Language.sat-structure is a yes-instance of 2SAT if every clause has at most two literal occurrences and the CNF is satisfiable.

Equations

• DescriptiveComplexity.TwoSatisfiable A = (DescriptiveComplexity.WidthAtMostTwo A ∧ DescriptiveComplexity.Satisfiable A)

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

Some clause has at least three distinct literal occurrences: the negation of the width bound (DescriptiveComplexity.wideTwo_iff_not_widthAtMostTwo).

Equations

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

theorem DescriptiveComplexity.wideTwo_iff_not_widthAtMostTwo {A : Type} [FirstOrder.Language.sat.Structure A] : WideTwo A ↔ ¬WidthAtMostTwo A

theorem DescriptiveComplexity.exists_covering_pair {A : Type} [FirstOrder.Language.sat.Structure A] (h : WidthAtMostTwo A) {c x : A} {s : Bool} (hocc : SatOcc.OccIn c x s) : ∃ (y : A) (u : Bool), SatOcc.OccIn c y u ∧ ∀ (z : A) (t : Bool), SatOcc.OccIn c z t → z = x ∧ t = s ∨ z = y ∧ t = u

Two occurrences cover a clause of a width-two structure: if the clause c has an occurrence at all, there are two signed occurrences of c such that every occurrence of c is one of them. This is what lets a single 2-clause speak for the whole clause.

theorem DescriptiveComplexity.widthAtMostTwo_iso {A B : Type} [FirstOrder.Language.sat.Structure A] [FirstOrder.Language.sat.Structure B] (e : FirstOrder.Language.sat.Equiv A B) : WidthAtMostTwo A ↔ WidthAtMostTwo B

The width-two bound is isomorphism-invariant.

theorem DescriptiveComplexity.twoSatisfiable_iso {A B : Type} [FirstOrder.Language.sat.Structure A] [FirstOrder.Language.sat.Structure B] (e : FirstOrder.Language.sat.Equiv A B) : TwoSatisfiable A ↔ TwoSatisfiable B

2-satisfiability is isomorphism-invariant.

def DescriptiveComplexity.TwoSAT : DecisionProblem FirstOrder.Language.sat

2SAT, as a problem on Language.sat-structures: the same vocabulary as SAT, with the width-two bound folded into the yes-instances.

Equations

• DescriptiveComplexity.TwoSAT = { Holds := fun (A : Type) (inst : FirstOrder.Language.sat.Structure A) => DescriptiveComplexity.TwoSatisfiable A, iso_invariant := ⋯ }

The width bound as a formula

The Krom program defining 2SAT enforces the width bound by a guard: guards are first-order over the input vocabulary, so the bound costs nothing beyond one goal clause. The formula is the width-two analogue of DescriptiveComplexity.ThreeSatToSat.wideOrdF.

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

Some clause has at least three distinct literal occurrences, as a formula over the ordered expansion: the clause is variable 0 and the three occurrence variables are 1, 2, 3; 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.realize_wideTwoOrdF {α A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {v : α → A} : wideTwoOrdF.Realize v ↔ WideTwo A