The criterion for 2-satisfiability, abstractly

A 2-CNF over a type V of propositional variables is a relation Cl on literals (DescriptiveComplexity.TwoCnf.Lit, a variable and a sign): Cl p q says that p ∨ q is one of its clauses. Unit clauses are the case q = p; the empty clause has no place here and is handled by whoever builds the formula, since it is unsatisfiable outright.

This file proves the classical criterion (Aspvall, Plass & Tarjan 1979) in this abstract setting: over a finite variable type, the 2-CNF is satisfiable iff no literal reaches its own negation and back in the implication graph, where the clause p ∨ q contributes the implications ¬p → q and ¬q → p (DescriptiveComplexity.TwoCnf.Step).

Nothing here mentions first-order logic. That is the point: the criterion is needed twice over, once for CNF structures over FirstOrder.Language.sat (DescriptiveComplexity.Problems.TwoSat.Ptime, where it puts 2SAT in PTIME) and once for the atoms of an arbitrary Krom program (where it turns a Krom definition into a transitive closure), and the two differ only in what plays the part of a variable.

The proof of the substantial direction builds a satisfying assignment greedily: a set of literals that is closed under reachability and consistent (never containing a literal together with its negation) can always be extended to decide one more variable, by picking the sign whose literal does not reach its own negation and adding everything reachable from it. Consistency survives by contraposition (DescriptiveComplexity.TwoCnf.reach_neg), which turns a clash inside the new part into the forbidden cycle and a clash with the old part into a variable that was already decided. Deciding every variable in turn gives the assignment, and closedness makes every clause true.

Literals

@[reducible, inline]

abbrev DescriptiveComplexity.TwoCnf.Lit (V : Type) : Type

A literal: a variable together with a sign (true for the variable itself, false for its negation).

Equations

• DescriptiveComplexity.TwoCnf.Lit V = (V × Bool)

def DescriptiveComplexity.TwoCnf.neg {V : Type} (p : Lit V) : Lit V

The negation of a literal.

Equations

• DescriptiveComplexity.TwoCnf.neg p = (p.1, !p.2)

@[simp]

theorem DescriptiveComplexity.TwoCnf.neg_neg {V : Type} (p : Lit V) : neg (neg p) = p

@[simp]

theorem DescriptiveComplexity.TwoCnf.neg_fst {V : Type} (p : Lit V) : (neg p).1 = p.1

def DescriptiveComplexity.TwoCnf.LitTrue {V : Type} (ν : V → Prop) (p : Lit V) : Prop

The literal is true under the assignment ν.

Equations

• DescriptiveComplexity.TwoCnf.LitTrue ν p = if p.2 = true then ν p.1 else ¬ν p.1

theorem DescriptiveComplexity.TwoCnf.litTrue_neg {V : Type} {ν : V → Prop} {p : Lit V} : LitTrue ν (neg p) ↔ ¬LitTrue ν p

The implication graph

def DescriptiveComplexity.TwoCnf.Satisfies {V : Type} (Cl : Lit V → Lit V → Prop) (ν : V → Prop) : Prop

The assignment satisfies the 2-CNF: every clause has a true literal.

Equations

• DescriptiveComplexity.TwoCnf.Satisfies Cl ν = ∀ (p q : DescriptiveComplexity.TwoCnf.Lit V), Cl p q → DescriptiveComplexity.TwoCnf.LitTrue ν p ∨ DescriptiveComplexity.TwoCnf.LitTrue ν q

def DescriptiveComplexity.TwoCnf.Step {V : Type} (Cl : Lit V → Lit V → Prop) (p q : Lit V) : Prop

One step of the implication graph: the clause ¬p ∨ q, in either order, is the implication p → q.

Equations

• DescriptiveComplexity.TwoCnf.Step Cl p q = (Cl (DescriptiveComplexity.TwoCnf.neg p) q ∨ Cl q (DescriptiveComplexity.TwoCnf.neg p))

@[reducible, inline]

abbrev DescriptiveComplexity.TwoCnf.Reach {V : Type} (Cl : Lit V → Lit V → Prop) : Lit V → Lit V → Prop

Reachability in the implication graph.

Equations

• DescriptiveComplexity.TwoCnf.Reach Cl = Relation.ReflTransGen (DescriptiveComplexity.TwoCnf.Step Cl)

theorem DescriptiveComplexity.TwoCnf.step_neg {V : Type} (Cl : Lit V → Lit V → Prop) {p q : Lit V} (h : Step Cl p q) : Step Cl (neg q) (neg p)

Contraposition, one step: the implication p → q is also ¬q → ¬p.

theorem DescriptiveComplexity.TwoCnf.reach_neg {V : Type} (Cl : Lit V → Lit V → Prop) {p q : Lit V} (h : Reach Cl p q) : Reach Cl (neg q) (neg p)

Contraposition: p ⇝ q gives ¬q ⇝ ¬p.

Soundness

theorem DescriptiveComplexity.TwoCnf.litTrue_of_step {V : Type} {Cl : Lit V → Lit V → Prop} {ν : V → Prop} (hν : Satisfies Cl ν) {p q : Lit V} (hstep : Step Cl p q) (hp : LitTrue ν p) : LitTrue ν q

One implication step preserves truth.

theorem DescriptiveComplexity.TwoCnf.litTrue_of_reach {V : Type} {Cl : Lit V → Lit V → Prop} {ν : V → Prop} (hν : Satisfies Cl ν) {p q : Lit V} (h : Reach Cl p q) (hp : LitTrue ν p) : LitTrue ν q

Implications are sound: reachability preserves truth.

theorem DescriptiveComplexity.TwoCnf.no_bad_cycle_of_satisfies {V : Type} (Cl : Lit V → Lit V → Prop) {ν : V → Prop} (hν : Satisfies Cl ν) (p : Lit V) : ¬(Reach Cl p (neg p) ∧ Reach Cl (neg p) p)

A satisfiable 2-CNF has no bad cycle: a literal reaching its own negation and back would be both true and false.

Closed consistent sets of literals

def DescriptiveComplexity.TwoCnf.Closed {V : Type} (Cl : Lit V → Lit V → Prop) (T : Set (Lit V)) : Prop

A set of literals closed under reachability.

Equations

• DescriptiveComplexity.TwoCnf.Closed Cl T = ∀ p ∈ T, ∀ (q : DescriptiveComplexity.TwoCnf.Lit V), DescriptiveComplexity.TwoCnf.Reach Cl p q → q ∈ T

def DescriptiveComplexity.TwoCnf.Consistent {V : Type} (T : Set (Lit V)) : Prop

A set of literals containing no literal together with its negation.

Equations

• DescriptiveComplexity.TwoCnf.Consistent T = ∀ p ∈ T, DescriptiveComplexity.TwoCnf.neg p ∉ T

def DescriptiveComplexity.TwoCnf.Decides {V : Type} (T : Set (Lit V)) (x : V) : Prop

The variable x is decided by T: one of its two literals is in T.

Equations

• DescriptiveComplexity.TwoCnf.Decides T x = ((x, true) ∈ T ∨ (x, false) ∈ T)

theorem DescriptiveComplexity.TwoCnf.closed_empty {V : Type} (Cl : Lit V → Lit V → Prop) : Closed Cl ∅

theorem DescriptiveComplexity.TwoCnf.consistent_empty {V : Type} : Consistent ∅

theorem DescriptiveComplexity.TwoCnf.exists_extend {V : Type} {Cl : Lit V → Lit V → Prop} {T : Set (Lit V)} (hclosed : Closed Cl T) (hcons : Consistent T) {x : V} (hx : ¬Decides T x) (hcyc : ∀ (s : Bool), ¬(Reach Cl (x, s) (neg (x, s)) ∧ Reach Cl (neg (x, s)) (x, s))) : ∃ (T' : Set (Lit V)), Closed Cl T' ∧ Consistent T' ∧ T ⊆ T' ∧ Decides T' x

The extension step: a closed consistent set that does not decide x can be extended to one that does, provided x has no bad cycle.

theorem DescriptiveComplexity.TwoCnf.exists_closed_consistent_deciding {V : Type} {Cl : Lit V → Lit V → Prop} (hcyc : ∀ (x : V) (s : Bool), ¬(Reach Cl (x, s) (neg (x, s)) ∧ Reach Cl (neg (x, s)) (x, s))) (S : Finset V) : ∃ (T : Set (Lit V)), Closed Cl T ∧ Consistent T ∧ ∀ x ∈ S, Decides T x

Deciding a whole finite set of variables, one extension at a time.

theorem DescriptiveComplexity.TwoCnf.exists_satisfies_of_no_bad_cycle {V : Type} {Cl : Lit V → Lit V → Prop} [Finite V] (hcyc : ∀ (x : V) (s : Bool), ¬(Reach Cl (x, s) (neg (x, s)) ∧ Reach Cl (neg (x, s)) (x, s))) : ∃ (ν : V → Prop), Satisfies Cl ν

The criterion: a 2-CNF with no literal reaching its own negation and back is satisfiable.

theorem DescriptiveComplexity.TwoCnf.exists_satisfies_iff_no_bad_cycle {V : Type} {Cl : Lit V → Lit V → Prop} [Finite V] : (∃ (ν : V → Prop), Satisfies Cl ν) ↔ ∀ (x : V) (s : Bool), ¬(Reach Cl (x, s) (neg (x, s)) ∧ Reach Cl (neg (x, s)) (x, s))

The criterion, as an equivalence: a 2-CNF over a finite variable type is satisfiable iff no literal reaches its own negation and back.

A bad cycle as a single walk

A bad cycle is a conjunction of two reachabilities, p ⇝ ¬p and ¬p ⇝ p, which no single transitive closure can state. Carrying the literal the walk started from, and a flag recording that its negation has been passed, turns the pair into one walk: from (p, p, false) to (p, p, true). This is what lets a DescriptiveComplexity.TCSpec express unsatisfiability of a 2-CNF, the flag and the two literals being the finite mode and the two tuples of a node.

@[reducible, inline]

abbrev DescriptiveComplexity.TwoCnf.CarryNode (V : Type) : Type

A node of the cycle-witnessing graph: the literal the walk started from, the literal it has reached, and whether it has already passed the negation of the start.

Equations

• DescriptiveComplexity.TwoCnf.CarryNode V = (DescriptiveComplexity.TwoCnf.Lit V × DescriptiveComplexity.TwoCnf.Lit V × Bool)

def DescriptiveComplexity.TwoCnf.CarryStep {V : Type} (Cl : Lit V → Lit V → Prop) (a b : CarryNode V) : Prop

One step of the cycle-witnessing graph: the start is kept, the current literal moves along an implication, and the flag may turn from false to true exactly on arrival at the negation of the start.

Equations

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

theorem DescriptiveComplexity.TwoCnf.reach_of_carryReach {V : Type} {Cl : Lit V → Lit V → Prop} {a b : CarryNode V} (h : Relation.ReflTransGen (CarryStep Cl) a b) : Reach Cl a.2.1 b.2.1

A walk of the cycle-witnessing graph projects to a walk of the implication graph.

theorem DescriptiveComplexity.TwoCnf.start_of_carryReach {V : Type} {Cl : Lit V → Lit V → Prop} {a b : CarryNode V} (h : Relation.ReflTransGen (CarryStep Cl) a b) : b.1 = a.1

The start component is constant along a walk.

theorem DescriptiveComplexity.TwoCnf.carryReach_of_reach {V : Type} {Cl : Lit V → Lit V → Prop} (s : Lit V) (ph : Bool) {a b : Lit V} (h : Reach Cl a b) : Relation.ReflTransGen (CarryStep Cl) (s, a, ph) (s, b, ph)

A walk of the implication graph lifts to one of the cycle-witnessing graph at any fixed start and flag.

theorem DescriptiveComplexity.TwoCnf.reach_neg_of_carryReach {V : Type} {Cl : Lit V → Lit V → Prop} {s a : Lit V} {d : CarryNode V} (h : Relation.ReflTransGen (CarryStep Cl) (s, a, false) d) (hd : d.2.2 = true) : Reach Cl a (neg s) ∧ Reach Cl (neg s) d.2.1

What a walk that has raised its flag witnesses: the start's negation was passed on the way.

theorem DescriptiveComplexity.TwoCnf.carryReach_iff {V : Type} {Cl : Lit V → Lit V → Prop} (p : Lit V) : Relation.ReflTransGen (CarryStep Cl) (p, p, false) (p, p, true) ↔ Reach Cl p (neg p) ∧ Reach Cl (neg p) p

A bad cycle is a single walk: the literal p reaches its own negation and comes back exactly when the cycle-witnessing graph takes (p, p, false) to (p, p, true).