Documentation

Complexity.Logics.Propositional.CNF.TwoCNF

The implication graph of a formula with clauses of width two #

A clause a ∨ b says both ¬a → b and ¬b → a, and a unit clause a says ¬a → a. The implication graph of a formula (Cslib.Logic.PL.CNF.Implies) has these arcs between literals: an arc from ℓ to ℓ' when some clause contains ¬ℓ and ℓ' and no other literal. Every arc is an implication that holds under a satisfying assignment, so a formula with a path from some literal x to ¬x and one back is unsatisfiable (Cslib.Logic.PL.CNF.not_satisfiable_of_reach). For clauses of width at most two the converse holds: a formula without the empty clause and without such a pair of paths is satisfiable (Cslib.Logic.PL.CNF.not_satisfiable_iff_of_width_le_two) Aspvall, Plass and Tarjan. The proof picks a literal ℓ with no path to ¬ℓ, makes every literal reachable from ℓ true, which is consistent and satisfies every clause it touches, and continues with the remaining clauses, which mention fewer variables. The empty clause, which has no arcs, is excluded separately; this proof is the library's own.

Main definitions #

Main results #

References #

source
def Cslib.Logic.PL.CNF.Implies {V : Type u_1} (φ : CNF V) (ℓ ℓ' : Literal V) :
Prop

The implication graph of a formula: an arc from ℓ to ℓ' when some clause contains ¬ℓ and ℓ' and no other literal. A clause a ∨ b gives the arcs ¬a → b and ¬b → a, and a unit clause a the arc ¬a → a.

Instances For
    source
    @[simp]
    theorem Cslib.Logic.PL.negate_negate {V : Type u_1} (ℓ : Literal V) :
    (Std.Sat.Literal.negate ℓ).negate = ℓ
    source
    theorem Cslib.Logic.PL.holds_negate {V : Type u_1} (σ : V → Bool) (ℓ : Literal V) :
    σ (Std.Sat.Literal.negate ℓ).1 = (Std.Sat.Literal.negate ℓ).2 ↔ ¬σ ℓ.1 = ℓ.2

    The negation of a literal holds exactly when the literal does not.

    source
    theorem Cslib.Logic.PL.CNF.Implies.negate {V : Type u_1} {φ : CNF V} {ℓ ℓ' : Literal V} (h : φ.Implies ℓ ℓ') :
    φ.Implies (Std.Sat.Literal.negate ℓ') (Std.Sat.Literal.negate ℓ)

    The implication graph is skew-symmetric: the contrapositive of an arc is an arc.

    source
    theorem Cslib.Logic.PL.CNF.Implies.eval {V : Type u_1} {φ : CNF V} {ℓ ℓ' : Literal V} {σ : V → Bool} (hσ : CNF.eval σ φ = true) (h : φ.Implies ℓ ℓ') (hℓ : σ ℓ.1 = ℓ.2) :
    σ ℓ'.1 = ℓ'.2

    An arc is an implication under every satisfying assignment.

    source
    theorem Cslib.Logic.PL.CNF.Implies.mono {V : Type u_1} {φ ψ : CNF V} {ℓ ℓ' : Literal V} (h : φ.Implies ℓ ℓ') (hφ : ∀ c ∈ φ, c ∈ ψ) :
    ψ.Implies ℓ ℓ'

    The implication graph grows with the formula.

    source
    theorem Cslib.Logic.PL.CNF.reach_negate {V : Type u_1} {φ : CNF V} {ℓ ℓ' : Literal V} (h : Relation.ReflTransGen φ.Implies ℓ ℓ') :
    Relation.ReflTransGen φ.Implies (Std.Sat.Literal.negate ℓ') (Std.Sat.Literal.negate ℓ)

    Paths of the implication graph are skew-symmetric too.

    source
    theorem Cslib.Logic.PL.CNF.eval_of_reach {V : Type u_1} {φ : CNF V} {σ : V → Bool} (hσ : eval σ φ = true) {ℓ ℓ' : Literal V} (h : Relation.ReflTransGen φ.Implies ℓ ℓ') (hℓ : σ ℓ.1 = ℓ.2) :
    σ ℓ'.1 = ℓ'.2

    Paths of the implication graph are implications under every satisfying assignment.

    source
    theorem Cslib.Logic.PL.CNF.not_satisfiable_of_reach {V : Type u_1} {φ : CNF V} {ℓ : Literal V} (h₁ : Relation.ReflTransGen φ.Implies ℓ (Std.Sat.Literal.negate ℓ)) (h₂ : Relation.ReflTransGen φ.Implies (Std.Sat.Literal.negate ℓ) ℓ) :
    ¬φ.Satisfiable

    A path from a literal to its negation and back refutes a formula.

    source
    theorem Cslib.Logic.PL.CNF.not_satisfiable_of_nil_mem {V : Type u_1} {φ : CNF V} (h : [] ∈ φ) :
    ¬φ.Satisfiable

    The empty clause refutes a formula.

    source
    theorem Cslib.Logic.PL.CNF.satisfiable_of_width_le_two {V : Type u_1} {φ : CNF V} (hw : ∀ c ∈ φ, List.length c ≤ 2) (hnil : [] ∉ φ) (hreach : ∀ (v : V), ¬(Relation.ReflTransGen φ.Implies (v, true) (v, false) ∧ Relation.ReflTransGen φ.Implies (v, false) (v, true))) :
    φ.Satisfiable

    A formula of width at most two is satisfiable when it has no empty clause and no variable x with a path from x to ¬x and one back Aspvall, Plass and Tarjan.

    source
    theorem Cslib.Logic.PL.CNF.not_satisfiable_iff_of_width_le_two {V : Type u_1} {φ : CNF V} (hw : ∀ c ∈ φ, List.length c ≤ 2) :
    ¬φ.Satisfiable ↔ [] ∈ φ ∨ ∃ (v : V), Relation.ReflTransGen φ.Implies (v, true) (v, false) ∧ Relation.ReflTransGen φ.Implies (v, false) (v, true)

    A formula of width at most two is unsatisfiable exactly when it has the empty clause or a variable x with a path from x to ¬x and one back Aspvall, Plass and Tarjan.