Skip to content

2-satisfiability

Definition2-CNF formulas#✓fully proved

A CNF formula is a 2-CNF formula when each of its clauses, viewed as a list of literals, has length at most \(2\) (repeated literals are counted with multiplicity).

def IsTwoCNF (φ : CNF) : Prop := ∀ C ∈ φ, C.length ≤ 2
Uses 2 · Used by 3
Statement usesCNF formula · CNF clause
Used by2-SAT characterization · Correctness of the SCC-based 2-SAT procedure · Satisfying assignments respect implication edges

AbbreviationComplement of a literal#✓fully proved

The complement of a literal \((x, b)\), with variable index \(x \in \mathbb{N}\) and polarity \(b\), is the literal \((x, \lnot b)\): same variable, opposite polarity.

abbrev neg (l : Nat × Bool) : Nat × Bool := (l.1, !l.2)
Used by 10
Used byResolution refutations give contradictory cycles · Implication edge · Reachability in the finite implication graph · Resolution invariant of the implication graph · Implication edges end over variables of the formula · A positive literal reaching its complement lies over a variable of the formula · Complement of a literal over a formula · Satisfying assignments respect implication edges · Skew symmetry of the implication graph · Successors in the implication graph

TheoremClauses with at most two literals#✓fully proved

In a clause with at most two literals, any two different members \(a\) and \(b\) are all of its members: every member \(c\) of the clause equals \(a\) or \(b\).

theorem eq_or_eq_of_length_le_two {C : CNFClause} (hC : C.length ≤ 2) {a b c : Nat × Bool}
    (ha : a ∈ C) (hb : b ∈ C) (hab : a ≠ b) (hc : c ∈ C) : c = a ∨ c = b
Uses 1 · Used by 1
Statement usesCNF clause
Used bySatisfying assignments respect implication edges
22 fully proved

The implication graph on literals

DefinitionImplication edge#✓fully proved

For a CNF formula \(\varphi\) and literals \(l\) and \(m\), there is an implication edge from \(l\) to \(m\) when some clause of \(\varphi\) contains both \(\neg l\) and \(m\), either as two different literals or with \(m\) as its only literal (so a unit clause \(m\) gives the edge from \(\neg m\) to \(m\)).

def ImpEdge (φ : CNF) (l m : Nat × Bool) : Prop :=
  ∃ C ∈ φ, neg l ∈ C ∧ m ∈ C ∧ (neg l ≠ m ∨ ∀ c ∈ C, c = m)
Uses 3 · Used by 9
Statement usesComplement of a literal · CNF formula · CNF clause
Used by2-SAT characterization · Resolution refutations give contradictory cycles · Reachability in the implication graph · Reachability in the finite implication graph · Implication edges end over variables of the formula · A positive literal reaching its complement lies over a variable of the formula · Satisfying assignments respect implication edges · Skew symmetry of the implication graph · Successors in the implication graph

DefinitionReachability in the implication graph#✓fully proved

For a CNF formula \(\varphi\), a literal \(l\) reaches a literal \(m\) when there is a path of zero or more implication edges of \(\varphi\) from \(l\) to \(m\); that is, reachability is the reflexive-transitive closure of the implication edge relation.

def ImpReach (φ : CNF) : Nat × Bool → Nat × Bool → Prop :=
  Relation.ReflTransGen (ImpEdge φ)
Uses 2 · Used by 6
Statement usesImplication edge · CNF formula
Used by2-SAT characterization · Correctness of the SCC-based 2-SAT procedure · Resolution refutations give contradictory cycles · Reachability in the finite implication graph · Resolution invariant of the implication graph · A positive literal reaching its complement lies over a variable of the formula

TheoremSkew symmetry of the implication graph#✓fully proved

For a CNF formula \(\varphi\) and literals \(l\) and \(m\), if the implication graph of \(\varphi\) has an edge from \(l\) to \(m\), then it also has the contrapositive edge from \(\lnot m\) to \(\lnot l\), where \(\lnot\) denotes the complementary literal.

theorem ImpEdge.skew {φ : CNF} {l m : Nat × Bool} (h : ImpEdge φ l m) :
    ImpEdge φ (neg m) (neg l)
Uses 4 · Used by 1
Statement usesImplication edge · Complement of a literal · CNF formula
Proof usesCNF clause
Used byResolution refutations give contradictory cycles

TheoremSatisfying assignments respect implication edges#✓fully proved

Let \(\varphi\) be a 2-CNF formula and \(\sigma\) an assignment of truth values to the variables that satisfies \(\varphi\). If the implication graph of \(\varphi\) has an edge from a literal \(l\) to a literal \(m\) and \(\sigma\) satisfies \(l\), then \(\sigma\) satisfies \(m\).

theorem satisfies_of_impEdge {φ : CNF} (h2 : IsTwoCNF φ) {σ : Nat → Bool}
    (hσ : φ.Satisfies σ) {l m : Nat × Bool} (h : ImpEdge φ l m)
    (hl : CNFLiteral.Satisfies σ l) : CNFLiteral.Satisfies σ m
Uses 9 · Used by 1
Statement usesImplication edge · 2-CNF formulas · CNF formula · Satisfaction of a CNF formula · Satisfaction of a literal
Proof usesClauses with at most two literals · Complement of a literal · CNF clause · Satisfaction of a clause
Used by2-SAT characterization

Resolution derivations from a 2-CNF formula

DefinitionResolution invariant of the implication graph#✓fully proved

A clause \(C\) satisfies the invariant with respect to a CNF formula \(\varphi\) when for every literal \(a\) of \(C\) there is a literal \(b\) of \(C\) such that the complementary literal \(\lnot a\) reaches \(b\) in the implication graph of \(\varphi\) (by a path of zero or more edges).

Every clause derivable from \(\varphi\) by resolution satisfies this invariant.

def Inv (φ : CNF) (C : CNFClause) : Prop := ∀ a ∈ C, ∃ b ∈ C, ImpReach φ (neg a) b
Uses 4 · Used by 1
Statement usesReachability in the implication graph · Complement of a literal · CNF formula · CNF clause
Used byResolution refutations give contradictory cycles

TheoremResolution refutations give contradictory cycles#✓fully proved

If a CNF formula \(\varphi\) does not contain the empty clause and the empty clause is derivable from \(\varphi\) by resolution, then there is a variable \(x\) such that the literals \(x\) and \(\neg x\) reach each other in the implication graph of \(\varphi\).

theorem exists_contradictory_of_resolutionDerivable_nil {φ : CNF} (hnil : [] ∉ φ)
    (h : φ.ResolutionDerivable []) :
    ∃ x, ImpReach φ (x, true) (x, false) ∧ ImpReach φ (x, false) (x, true)
Uses 9 · Used by 1
Statement usesReachability in the implication graph · CNF formula · Resolution derivability · CNF clause
Proof usesImplication edge · Skew symmetry of the implication graph · Resolution invariant of the implication graph · Complement of a literal · Resolvent of two clauses
Used by2-SAT characterization

Theorem2-SAT characterization#✓fully proved

2-SAT characterization (Aspvall, Plass, Tarjan): a 2-CNF formula is satisfiable iff it has no empty clause and no variable x such that x and ¬x reach each other in the implication graph.

theorem cnfSat_iff_of_isTwoCNF {φ : CNF} (h2 : IsTwoCNF φ) :
    CNFSat φ ↔ [] ∉ φ ∧
      ∀ x, ¬ (ImpReach φ (x, true) (x, false) ∧ ImpReach φ (x, false) (x, true))
Uses 13 · Used by 1
Statement usesReachability in the implication graph · 2-CNF formulas · CNF formula · CNF clause · Satisfiability of a CNF formula
Proof usesImplication edge · Resolution refutations give contradictory cycles · Satisfying assignments respect implication edges · Satisfaction of a CNF formula · Refutation completeness · Satisfaction of a clause · Satisfaction of a literal · Satisfiability means having a satisfying assignment
Used byCorrectness of the SCC-based 2-SAT procedure

The implication graph as a finite directed graph, and the SCC decision procedure

AbbreviationLiterals over the variables of a formula#✓fully proved

For a CNF formula \(\varphi\), a literal over \(\varphi\) is a pair \((x, b)\) of a variable index \(x \in \mathbb{N}\) and a polarity \(b \in \{\mathrm{true}, \mathrm{false}\}\) such that the variable \(x\) occurs in \(\varphi\). These literals are the vertices of the implication graph of \(\varphi\).

abbrev Lit (φ : CNF) := {l : Nat × Bool // l.1 ∈ φ.vars}
Uses 2 · Used by 8
Statement usesCNF formula · Variables of a CNF formula
Used byAdjacency table of the implication graph · SCC-based 2-SAT decision procedure · Correctness of the SCC-based 2-SAT procedure · Implication graph as a finite directed graph · Reachability in the finite implication graph · List of the literals of a CNF formula · Complement of a literal over a formula · Successors in the implication graph

DefinitionComplement of a literal over a formula#✓fully proved

For a CNF formula \(\varphi\), the complement of a literal \((x, b)\) over the variables of \(\varphi\) is the literal \((x, \lnot b)\), which is again a literal over the variables of \(\varphi\).

def Lit.neg {φ : CNF} (l : Lit φ) : Lit φ := ⟨TwoSAT.neg l.val, l.prop⟩
Uses 4 · Used by 2
Statement usesLiterals over the variables of a formula · Complement of a literal · CNF formula · Variables of a CNF formula
Used bySCC-based 2-SAT decision procedure · Correctness of the SCC-based 2-SAT procedure

DefinitionDuplicate-free list of the variables of a CNF formula#✓fully proved

For a CNF formula \(\varphi\), this is the list of the variables occurring in the literals of \(\varphi\), each exactly once, in the order of their last occurrences when the clauses of \(\varphi\) and their literals are read from first to last.

def varList (φ : CNF) : List Nat := (φ.flatMap fun C ↦ C.map Prod.fst).dedup
Uses 2 · Used by 3
Statement usesCNF formula · CNF clause
Used byImplication graph as a finite directed graph · Reachability in the finite implication graph · List of the literals of a CNF formula

DefinitionList of the literals of a CNF formula#✓fully proved

For a CNF formula \(\varphi\), this is the list of all literals over the variables of \(\varphi\), each appearing exactly once, arranged variable by variable: for each variable \(x\) of \(\varphi\), the positive literal \((x, \mathrm{true})\) is immediately followed by the negative literal \((x, \mathrm{false})\).

def litList (φ : CNF) : List (Lit φ) :=
  (varList φ).attach.flatMap fun x ↦
    [⟨(x.1, true), mem_varList.mp x.2⟩, ⟨(x.1, false), mem_varList.mp x.2⟩]
Uses 6 · Used by 4
Statement usesLiterals over the variables of a formula · Duplicate-free list of the variables of a CNF formula · CNF formula · Variables of a CNF formula · CNF clause · Variables of a clause
Used byAdjacency table of the implication graph · Implication graph as a finite directed graph · Reachability in the finite implication graph · Successors in the implication graph

DefinitionSuccessors in the implication graph#✓fully proved

Let \(\varphi\) be a CNF formula and \(l\) a literal over the variables of \(\varphi\), and write \(\neg l\) for the complementary literal. The successors of \(l\) are the literals \(m\) over the variables of \(\varphi\) such that the implication graph of \(\varphi\) has an edge from \(l\) to \(m\): some clause of \(\varphi\) contains \(\neg l\) and \(m\), either as two different literals or as its only literal. They are listed without repetition, in the order of the list of all literals over the variables of \(\varphi\).

def successors (φ : CNF) (l : Lit φ) : List (Lit φ) :=
  (litList φ).filter fun m ↦ decide (ImpEdge φ l.val m.val)
Uses 7 · Used by 2
Statement usesImplication edge · Literals over the variables of a formula · List of the literals of a CNF formula · Complement of a literal · CNF formula · Variables of a CNF formula · CNF clause
Used byAdjacency table of the implication graph · Reachability in the finite implication graph

DefinitionAdjacency table of the implication graph#✓fully proved

For a CNF formula \(\varphi\), the hash map that sends each literal over the variables of \(\varphi\) to the list of its implication-graph successors, that is, of the literals \(m\) over the variables of \(\varphi\) with an implication edge from it to \(m\).

The table is computed once so that the SCC traversal looks successor lists up in expected constant time.

def adjacencyTable (φ : CNF) : Std.HashMap (Lit φ) (List (Lit φ)) :=
  Std.HashMap.ofList ((litList φ).map fun l ↦ (l, successors φ l))
Uses 5 · Used by 2
Statement usesLiterals over the variables of a formula · List of the literals of a CNF formula · Successors in the implication graph · CNF formula · Variables of a CNF formula
Used byImplication graph as a finite directed graph · Reachability in the finite implication graph

DefinitionImplication graph as a finite directed graph#✓fully proved

For a CNF formula \(\varphi\), the finite directed graph whose vertices are the literals over the variables of \(\varphi\), listed without repetition, and whose out-neighbours of a literal \(l\) are the literals \(m\) over the variables of \(\varphi\) with an implication edge from \(l\) to \(m\), read from the adjacency table of \(\varphi\).

def implicationGraph (φ : CNF) : DirectedAdjacency (Lit φ) :=
  let table := adjacencyTable φ
  { vertices := litList φ
    vertices_nodup := nodup_litList φ
    vertices_complete := mem_litList φ
    adjacency := fun l ↦ table.getD l [] }
Uses 9 · Used by 3
Statement usesDirected adjacency graph · Literals over the variables of a formula · Adjacency table of the implication graph · List of the literals of a CNF formula · Duplicate-free list of the variables of a CNF formula · CNF formula · Variables of a CNF formula · CNF clause · Variables of a clause
Used bySCC-based 2-SAT decision procedure · Correctness of the SCC-based 2-SAT procedure · Reachability in the finite implication graph

TheoremImplication edges end over variables of the formula#✓fully proved

For a CNF formula \(\varphi\) and literals \(l\) and \(m\), if the implication graph of \(\varphi\) has an edge from \(l\) to \(m\), then the variable of \(m\) occurs in \(\varphi\).

theorem mem_vars_of_impEdge {φ : CNF} {l m : Nat × Bool} (h : ImpEdge φ l m) :
    m.1 ∈ φ.vars
Uses 6 · Used by 1
Statement usesImplication edge · CNF formula · Variables of a CNF formula
Proof usesComplement of a literal · CNF clause · Variables of a clause
Used byReachability in the finite implication graph

TheoremReachability in the finite implication graph#✓fully proved

For a CNF formula \(\varphi\) and literals \(l\) and \(m\) over the variables of \(\varphi\), \(m\) is reachable from \(l\) in the implication graph of \(\varphi\), viewed as a finite directed graph on these literals, if and only if \(l\) reaches \(m\) by implication edges of \(\varphi\).

theorem implicationGraph_reachable_iff {φ : CNF} {l m : Lit φ} :
    (implicationGraph φ).Reachable l m ↔ ImpReach φ l.val m.val
Uses 17 · Used by 1
Statement usesReachability in a directed graph · Reachability in the implication graph · Literals over the variables of a formula · Implication graph as a finite directed graph · CNF formula · Variables of a CNF formula
Proof usesDirected adjacency graph · Edge of a directed adjacency graph · Implication edge · Adjacency table of the implication graph · List of the literals of a CNF formula · Implication edges end over variables of the formula · Complement of a literal · Successors in the implication graph · Duplicate-free list of the variables of a CNF formula · CNF clause · Variables of a clause
Used byCorrectness of the SCC-based 2-SAT procedure

DefinitionSCC-based 2-SAT decision procedure#✓fully proved

For a CNF formula \(\varphi\), the procedure returns false if \(\varphi\) contains the empty clause; otherwise it returns true if and only if no block of the strongly connected components computed for the implication graph of \(\varphi\) contains a literal together with its complementary literal.

def decide2SAT (φ : CNF) : Bool :=
  !φ.contains [] &&
    (components (implicationGraph φ)).all fun block ↦ block.all fun l ↦ !block.contains l.neg
Uses 7 · Used by 1
Statement usesStrongly connected components algorithm · Literals over the variables of a formula · Complement of a literal over a formula · Implication graph as a finite directed graph · CNF formula · Variables of a CNF formula · CNF clause
Used byCorrectness of the SCC-based 2-SAT procedure

TheoremA positive literal reaching its complement lies over a variable of the formula#✓fully proved

For a CNF formula \(\varphi\) and a variable \(x\), if the positive literal \((x, \mathrm{true})\) reaches the negative literal \((x, \mathrm{false})\) in the implication graph of \(\varphi\), then \(x\) occurs in \(\varphi\).

theorem mem_vars_of_impReach_true_false {φ : CNF} {x : Nat}
    (h : ImpReach φ (x, true) (x, false)) : x ∈ φ.vars
Uses 7 · Used by 1
Statement usesReachability in the implication graph · CNF formula · Variables of a CNF formula
Proof usesImplication edge · Complement of a literal · CNF clause · Variables of a clause
Used byCorrectness of the SCC-based 2-SAT procedure

TheoremCorrectness of the SCC-based 2-SAT procedure#✓fully proved

For every CNF formula \(\varphi\) in which every clause has at most two literals, the SCC-based 2-SAT decision procedure returns true on \(\varphi\) if and only if \(\varphi\) is satisfiable.

theorem decide2SAT_eq_true_iff {φ : CNF} (h2 : IsTwoCNF φ) :
    decide2SAT φ = true ↔ CNFSat φ
Uses 17
Statement uses2-CNF formulas · SCC-based 2-SAT decision procedure · CNF formula · Satisfiability of a CNF formula
Proof usesReachability in a directed graph · Strongly connected vertices · Strongly connected components algorithm · Vertices share a computed component exactly when strongly connected · Reachability in the implication graph · Literals over the variables of a formula · Complement of a literal over a formula · 2-SAT characterization · Implication graph as a finite directed graph · Reachability in the finite implication graph · A positive literal reaching its complement lies over a variable of the formula · Variables of a CNF formula · CNF clause

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.