Resolution

The single resolution step on CNF clauses and its soundness (roadmap track L5). The resolvent of c₁ and c₂ on a variable v drops the positive literal x_v from c₁ and the negative literal ¬x_v from c₂ and disjoins the remainder. Soundness — any assignment satisfying both parents satisfies the resolvent — is the semantic core underlying resolution proof systems.

Main definitions and results

• Clause.resolvent — the resolvent of two clauses on a variable
• Clause.resolvent_sound — soundness of one resolution step
• CNF.Derives — the resolution proof system as an inductive derivation relation
• CNF.refutation_sound — soundness of resolution: a derivation of the empty clause proves the formula unsatisfiable

def Complexity.SAT.Clause.resolvent (c₁ c₂ : Clause) (v : ℕ) : Clause

The resolvent of clauses c₁ and c₂ on variable v: drop the positive literal x_v from c₁ and the negative literal ¬x_v from c₂, then take the disjunction of what remains.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.SAT.Clause.resolvent_sound (α : Assignment) (c₁ c₂ : Clause) (v : ℕ) (h₁ : eval α c₁ = true) (h₂ : eval α c₂ = true) : eval α (c₁.resolvent c₂ v) = true

Soundness of one resolution step. Any assignment satisfying both parent clauses satisfies their resolvent: whichever way the assignment sets x_v, the pivot literal it kills off in one parent forces a surviving literal there.

Entailment and refutation soundness

A resolution refutation of a CNF φ derives the empty clause from φ's clauses by repeated resolution. The following three facts — axioms are entailed, resolvents preserve entailment, and the empty clause is entailed only by an unsatisfiable formula — are the semantic core: any such derivation of the empty clause proves φ unsatisfiable.

def Complexity.SAT.CNF.Entails (φ : CNF) (c : Clause) : Prop

φ entails clause c when every satisfying assignment of φ satisfies c.

Equations

• φ.Entails c = ∀ (α : Complexity.SAT.Assignment), Complexity.SAT.CNF.eval α φ = true → Complexity.SAT.Clause.eval α c = true

theorem Complexity.SAT.CNF.entails_of_mem {φ : CNF} {c : Clause} (hc : c ∈ φ) : φ.Entails c

Every clause of φ is entailed by φ (resolution axioms are sound).

theorem Complexity.SAT.CNF.entails_resolvent {φ : CNF} {c₁ c₂ : Clause} {v : ℕ} (h₁ : φ.Entails c₁) (h₂ : φ.Entails c₂) : φ.Entails (c₁.resolvent c₂ v)

Resolution preserves entailment: if φ entails both parents, it entails the resolvent.

theorem Complexity.SAT.CNF.not_satisfiable_of_entails_nil {φ : CNF} (h : φ.Entails []) : ¬φ.Satisfiable

Refutation soundness. If φ entails the empty clause — as it does when the empty clause is derivable from φ by resolution — then φ is unsatisfiable (the empty clause is false under every assignment).

theorem Complexity.SAT.Clause.resolvent_length_le (c₁ c₂ : Clause) (v : ℕ) : List.length (c₁.resolvent c₂ v) ≤ List.length c₁ + List.length c₂

Width bound for one resolution step. The resolvent has at most as many literals as its two parents combined (dropping the pivot only shrinks each parent) — the basic width fact behind width-based resolution lower bounds.

theorem Complexity.SAT.CNF.entails_cons {φ : CNF} {c c' : Clause} (h : φ.Entails c) : Entails (c' :: φ) c

Entailment is monotone under adding clauses: a stronger formula still entails everything the weaker one did. Lets a resolution derivation carry its axioms along as the clause set grows.

The resolution proof system

Packaging the resolution steps as a derivation relation makes a resolution proof a first-class object: CNF.Derives φ c holds when c is derivable from the clauses of φ by resolution. Its soundness (entails_of_derives) collapses an entire derivation to a single entailment, and refuting via the empty clause (refutation_sound) is then a certificate of unsatisfiability.

inductive Complexity.SAT.CNF.Derives (φ : CNF) : Clause → Prop

The resolution proof system: CNF.Derives φ c holds when the clause c is derivable from the clauses of φ by resolution — either c is an axiom (a clause of φ) or it is the resolvent of two already-derived clauses.

• axm {φ : CNF} {c : Clause} (hc : c ∈ φ) : φ.Derives c

  A clause of φ is derivable (an axiom).

• res {φ : CNF} {c₁ c₂ : Clause} {v : ℕ} (h₁ : φ.Derives c₁) (h₂ : φ.Derives c₂) : φ.Derives (c₁.resolvent c₂ v)

  The resolvent of two derivable clauses is derivable.

theorem Complexity.SAT.CNF.entails_of_derives {φ : CNF} {c : Clause} (h : φ.Derives c) : φ.Entails c

Soundness of resolution derivations. Everything derivable from φ by resolution is entailed by φ — proved by induction on the derivation, using axiom soundness at the leaves and resolvent soundness at each step.

theorem Complexity.SAT.CNF.refutation_sound {φ : CNF} (h : φ.Derives []) : ¬φ.Satisfiable

Resolution refutation soundness. A resolution derivation of the empty clause from φ proves that φ is unsatisfiable. This is the correctness of resolution as a refutation system.

theorem Complexity.SAT.CNF.derives_cons {φ : CNF} {c c' : Clause} (h : φ.Derives c) : Derives (c' :: φ) c

Derivations survive the addition of clauses: anything derivable from φ is derivable from any extension c' :: φ. (Weakening / monotonicity of the proof system.)

The unit contradiction

The smallest resolution refutation: resolving the complementary unit clauses [x_v] and [¬x_v] on v yields the empty clause in a single step. A formula containing both is therefore refutable, hence unsatisfiable.

theorem Complexity.SAT.Clause.resolvent_units_nil (v : ℕ) : resolvent [{ sign := true, var := v }] [{ sign := false, var := v }] v = []

Resolving the complementary unit clauses [x_v] and [¬x_v] on v yields the empty clause.

theorem Complexity.SAT.CNF.derives_nil_of_units {φ : CNF} (v : ℕ) (h₁ : [{ sign := true, var := v }] ∈ φ) (h₂ : [{ sign := false, var := v }] ∈ φ) : φ.Derives []

A formula containing both unit clauses [x_v] and [¬x_v] refutes to the empty clause in one resolution step.

theorem Complexity.SAT.CNF.not_satisfiable_of_units {φ : CNF} (v : ℕ) (h₁ : [{ sign := true, var := v }] ∈ φ) (h₂ : [{ sign := false, var := v }] ∈ φ) : ¬φ.Satisfiable

Complementary unit clauses are unsatisfiable. Any formula containing both [x_v] and [¬x_v] is unsatisfiable, certified by the one-step resolution refutation.