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

The implication graph

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.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

Closed consistent sets of literals

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.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).