Resolution

The resolvent of clauses c₁ and c₂ on a variable v drops the positive literal of v from c₁ and the negative literal of v from c₂ and joins what remains (Clause.resolvent). A clause is derivable from a formula φ by resolution if it is a clause of φ or the resolvent of two derivable clauses on a variable occurring positively in the first and negatively in the second (CNF.Derives). Resolution is sound: an assignment satisfying both parents satisfies the resolvent, so a formula from which the empty clause is derivable is unsatisfiable (CNF.Derives.not_satisfiable). It is also refutation complete, the ground resolution theorem of [Rob65]: the empty clause is derivable from every unsatisfiable formula (CNF.derives_nil_of_not_satisfiable).

Completeness goes by induction on the number of variables, splitting on a variable as in the procedure of [DP60]. Fixing a variable v of an unsatisfiable formula to either value (CNF.restrict) leaves two unsatisfiable formulas without v, from which the empty clause is derivable. Replaying such a derivation on the original formula derives a clause all of whose literals are the literal of v falsified by the fixed value (CNF.Derives.exists_of_restrict). Either one of the two clauses obtained this way is empty, or they resolve on v to the empty clause.

Clauses are lists, so derivability depends on the order and repetition of literals; there is no weakening rule.

Main definitions

• Cslib.Logic.PL.Clause.resolvent: the resolvent of two clauses on a variable.
• Cslib.Logic.PL.CNF.Derives: derivability by resolution.
• Cslib.Logic.PL.CNF.restrict: a formula with one variable fixed.

Main results

• Cslib.Logic.PL.CNF.Derives.not_satisfiable: soundness of resolution refutations.
• Cslib.Logic.PL.CNF.derives_nil_iff_not_satisfiable: resolution refutes exactly the unsatisfiable formulas.

References

• J. A. Robinson, A machine-oriented logic based on the resolution principle
• M. Davis, H. Putnam, A computing procedure for quantification theory

The resolution rule

def Cslib.Logic.PL.Clause.resolvent {V : Type u_1} [DecidableEq V] (c₁ c₂ : Clause V) (v : V) : Clause V

The resolvent of c₁ and c₂ on v: the literals of c₁ other than v and those of c₂ other than ¬v.

@[simp]

theorem Cslib.Logic.PL.Clause.mem_resolvent {V : Type u_1} [DecidableEq V] {c₁ c₂ : Clause V} {v : V} {l : Literal V} : l ∈ c₁.resolvent c₂ v ↔ l ∈ c₁ ∧ l ≠ (v, true) ∨ l ∈ c₂ ∧ l ≠ (v, false)

theorem Cslib.Logic.PL.Clause.length_resolvent_le {V : Type u_1} [DecidableEq V] (c₁ c₂ : Clause V) (v : V) : List.length (c₁.resolvent c₂ v) ≤ List.length c₁ + List.length c₂

The resolvent has at most as many literals as its parents together.

theorem Cslib.Logic.PL.Clause.eval_resolvent {V : Type u_1} [DecidableEq V] {σ : V → Bool} {c₁ c₂ : Clause V} (v : V) (h₁ : eval σ c₁ = true) (h₂ : eval σ c₂ = true) : eval σ (c₁.resolvent c₂ v) = true

Soundness of one resolution step: an assignment satisfying both parents satisfies the resolvent.

Derivations and soundness

inductive Cslib.Logic.PL.CNF.Derives {V : Type u_1} [DecidableEq V] (φ : CNF V) : Clause V → Prop

The clauses derivable from φ by resolution: the clauses of φ, and the resolvents of derivable clauses.

• mem {V : Type u_1} [DecidableEq V] {φ : CNF V} {c : Clause V} (hc : c ∈ φ) : φ.Derives c

  A clause of φ is derivable.

• resolvent {V : Type u_1} [DecidableEq V] {φ : CNF V} {c₁ c₂ : Clause V} (v : V) (h₁ : φ.Derives c₁) (h₂ : φ.Derives c₂) (hv₁ : (v, true) ∈ c₁) (hv₂ : (v, false) ∈ c₂) : φ.Derives (c₁.resolvent c₂ v)

  The resolvent of two derivable clauses on a variable occurring positively in the first and negatively in the second is derivable.

theorem Cslib.Logic.PL.CNF.Derives.eval_eq_true {V : Type u_1} [DecidableEq V] {φ : CNF V} {c : Clause V} (h : φ.Derives c) {σ : V → Bool} (hσ : eval σ φ = true) : Clause.eval σ c = true

A derivable clause is true under every assignment satisfying the formula.

theorem Cslib.Logic.PL.CNF.Derives.not_satisfiable {V : Type u_1} [DecidableEq V] {φ : CNF V} (h : φ.Derives []) : ¬φ.Satisfiable

Soundness of resolution: a formula from which the empty clause is derivable is unsatisfiable.

theorem Cslib.Logic.PL.CNF.Derives.mono {V : Type u_1} [DecidableEq V] {φ ψ : CNF V} {c : Clause V} (h : φ.Derives c) (hφψ : φ ⊆ ψ) : ψ.Derives c

Derivations survive adding clauses.

Completeness

def Cslib.Logic.PL.CNF.restrict {V : Type u_1} [DecidableEq V] (φ : CNF V) (v : V) (b : Bool) : CNF V

φ with the variable v fixed to b: the clauses satisfied by v = b are dropped, and the literal of v falsified by v = b is removed from the others.

@[simp]

theorem Cslib.Logic.PL.CNF.mem_restrict {V : Type u_1} [DecidableEq V] {φ : CNF V} {v : V} {b : Bool} {c : Clause V} : c ∈ φ.restrict v b ↔ ∃ d ∈ φ, (v, b) ∉ d ∧ List.filter (fun (x : V × Bool) => decide (x ≠ (v, !b))) d = c

theorem Cslib.Logic.PL.CNF.fst_ne_of_mem_restrict {V : Type u_1} [DecidableEq V] {φ : CNF V} {v : V} {b : Bool} {c : Clause V} (hc : c ∈ φ.restrict v b) {l : Literal V} (hl : l ∈ c) : l.1 ≠ v

A restricted formula no longer mentions the fixed variable.

theorem Cslib.Logic.PL.CNF.vars_restrict_subset {V : Type u_1} [DecidableEq V] {φ : CNF V} {v : V} {b : Bool} : (φ.restrict v b).vars.toFinset ⊆ φ.vars.toFinset.erase v

The variables of a restricted formula are variables of the formula other than the fixed one.

theorem Cslib.Logic.PL.CNF.eval_update_of_eval_restrict {V : Type u_1} [DecidableEq V] {φ : CNF V} {v : V} {b : Bool} {σ : V → Bool} (h : eval σ (φ.restrict v b) = true) : eval (Function.update σ v b) φ = true

If σ satisfies the restricted formula, then σ with v set to b satisfies the formula.

theorem Cslib.Logic.PL.CNF.not_satisfiable_restrict {V : Type u_1} [DecidableEq V] {φ : CNF V} {v : V} {b : Bool} (h : ¬φ.Satisfiable) : ¬(φ.restrict v b).Satisfiable

Fixing a variable of an unsatisfiable formula leaves an unsatisfiable formula.

theorem Cslib.Logic.PL.CNF.Derives.exists_of_restrict {V : Type u_1} [DecidableEq V] {φ : CNF V} {v : V} {b : Bool} {c : Clause V} (h : (φ.restrict v b).Derives c) : ∃ (d : Clause V), φ.Derives d ∧ (∀ l ∈ d, l ∈ c ∨ l = (v, !b)) ∧ ∀ l ∈ c, l ∈ d

Lifting a derivation: a clause derivable from φ with v fixed to b is contained in a clause derivable from φ that may also contain the literal of v falsified by b.

theorem Cslib.Logic.PL.CNF.derives_nil_of_not_satisfiable {V : Type u_1} [DecidableEq V] {φ : CNF V} (h : ¬φ.Satisfiable) : φ.Derives []

Refutation completeness of resolution: the empty clause is derivable from every unsatisfiable formula.

theorem Cslib.Logic.PL.CNF.derives_nil_iff_not_satisfiable {V : Type u_1} [DecidableEq V] {φ : CNF V} : φ.Derives [] ↔ ¬φ.Satisfiable

Resolution refutes exactly the unsatisfiable formulas.