2SAT

Cslib.Complexity.TwoSAT is the set of satisfiable formulas in conjunctive normal form whose clauses have at most two literals, over variables numbered by ℕ and encoded as for SAT (Cslib.Complexity.encCNF) [Pap94a]. A formula outside TwoSAT has a clause of width greater than two, the empty clause, or a variable x with a path from x to ¬x and one back in its implication graph (Cslib.Complexity.notMem_TwoSAT_iff), by the theorem of Aspvall, Plass and Tarjan (Cslib.Logic.PL.CNF.not_satisfiable_iff_of_width_le_two) [APT79].

Main definitions

• Cslib.Complexity.TwoSAT.

Main results

• Cslib.Complexity.notMem_TwoSAT_iff: the formulas outside TwoSAT.

References

• B. Aspvall, M. F. Plass, R. E. Tarjan, A linear-time algorithm for testing the truth of certain quantified boolean formulas
• C. H. Papadimitriou, Computational Complexity

def Cslib.Complexity.TwoSAT : Set (Logic.PL.CNF ℕ)

The satisfiable formulas whose clauses have at most two literals.

theorem Cslib.Complexity.mem_TwoSAT {φ : Logic.PL.CNF ℕ} : φ ∈ TwoSAT ↔ (∀ c ∈ φ, List.length c ≤ 2) ∧ φ.Satisfiable

theorem Cslib.Complexity.notMem_TwoSAT_iff {φ : Logic.PL.CNF ℕ} : φ ∉ TwoSAT ↔ (∃ c ∈ φ, 2 < List.length c) ∨ [] ∈ φ ∨ ∃ (v : ℕ), Relation.ReflTransGen φ.Implies (v, true) (v, false) ∧ Relation.ReflTransGen φ.Implies (v, false) (v, true)

The formulas outside TwoSAT: those with a clause of width greater than two, the empty clause, or a variable x with a path from x to ¬x and one back in the implication graph.