Resolution proofs

Derivability by resolution (Cslib.Logic.PL.CNF.Derives) records only that a clause can be derived. Proof complexity measures derivations, so this file gives them their usual line-based form: a resolution proof from a formula φ is a sequence of clauses, each of which is a clause of φ or the resolvent (Cslib.Logic.PL.Clause.resolvent) of two earlier clauses on a variable occurring positively in the first and negatively in the second (Cslib.Logic.PL.CNF.IsProof). Proofs are listed from their last line to their first, so that a proof grows by adding a line in front. A clause is derivable exactly when it is a line of some proof (Cslib.Logic.PL.CNF.derives_iff_exists_isProof).

A refutation is a proof with the empty clause among its lines. Its size is its number of lines, and its width the largest width of a line, where the width of a clause (Cslib.Logic.PL.Clause.width) is its number of distinct literals [Ben-Sasson and Wigderson] [BSW01]. Clauses are lists, so a line may repeat a literal; repetitions do not count towards its width.

Fixing a variable transforms proofs in both directions:

• a proof from φ becomes a proof from the restricted formula φ.restrict v b (Cslib.Logic.PL.CNF.IsProof.restrict). It has at most as many lines; every line of the original proof that v = b does not satisfy is replaced by a line with a subset of its literals, and a line of the new proof is wider than any given bound only if the line it replaces is;
• a proof from φ.restrict v b lifts to a proof from φ (Cslib.Logic.PL.CNF.IsProof.lift) whose lines contain the lines they lift and, besides their literals, at most the literal of v that b falsifies. This is Cslib.Logic.PL.CNF.Derives.exists_of_restrict for proofs, keeping track of the lines.

Proofs also compose: a proof from ψ replays on top of a proof from φ among whose lines are the clauses of ψ (Cslib.Logic.PL.CNF.IsProof.comp).

Main definitions

• Cslib.Logic.PL.Clause.width: the number of distinct literals of a clause.
• Cslib.Logic.PL.CNF.IsProof: resolution proofs.
• Cslib.Logic.PL.CNF.RefutableInSize, Cslib.Logic.PL.CNF.RefutableInWidth: refutability by a refutation with a bounded number of lines, or with lines of bounded width.
• Cslib.Logic.PL.CNF.restrictBy: restricting a formula by a partial assignment.

Main results

• Cslib.Logic.PL.CNF.derives_iff_exists_isProof: derivable clauses are the lines of proofs.
• Cslib.Logic.PL.CNF.exists_refutableInSize_iff_not_satisfiable: resolution refutes exactly the unsatisfiable formulas.
• Cslib.Logic.PL.CNF.IsProof.restrict, Cslib.Logic.PL.CNF.IsProof.lift, Cslib.Logic.PL.CNF.IsProof.restrictBy: restricting and lifting proofs along a fixed variable or a partial assignment.
• Cslib.Logic.PL.CNF.IsProof.comp: composing proofs.

References

• E. Ben-Sasson, A. Wigderson, Short proofs are narrow—resolution made simple
• J. A. Robinson, A machine-oriented logic based on the resolution principle

Width

def Cslib.Logic.PL.Clause.width {V : Type u_1} [DecidableEq V] (c : Clause V) : ℕ

The width of a clause: its number of distinct literals.

@[simp]

theorem Cslib.Logic.PL.Clause.width_nil {V : Type u_1} [DecidableEq V] : width [] = 0

theorem Cslib.Logic.PL.Clause.width_le_width {V : Type u_1} [DecidableEq V] {c d : Clause V} (h : ∀ l ∈ c, l ∈ d) : c.width ≤ d.width

A clause whose literals occur in another clause is at most as wide.

theorem Cslib.Logic.PL.Clause.width_le_width_add_one {V : Type u_1} [DecidableEq V] {c d : Clause V} {x : Literal V} (h : ∀ l ∈ c, l ∈ d ∨ l = x) : c.width ≤ d.width + 1

A clause whose literals occur in another clause, apart from the literal x, is at most one wider.

theorem Cslib.Logic.PL.Clause.eq_nil_of_width_eq_zero {V : Type u_1} [DecidableEq V] {c : Clause V} (h : c.width = 0) : c = []

A clause of width zero is empty.

Proofs

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

A resolution proof from φ, listed from its last line to its first: every line is a clause of φ, or the resolvent of two lines below it on a variable occurring positively in the first and negatively in the second.

• nil {V : Type u_1} [DecidableEq V] {φ : CNF V} : φ.IsProof []

  The empty proof.

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

  A clause of φ is a new line.

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

  The resolvent of two lines, on a variable occurring positively in the first and negatively in the second, is a new line.

def Cslib.Logic.PL.CNF.RefutableInSize {V : Type u_1} [DecidableEq V] (φ : CNF V) (s : ℕ) : Prop

φ has a resolution refutation with at most s lines.

def Cslib.Logic.PL.CNF.RefutableInWidth {V : Type u_1} [DecidableEq V] (φ : CNF V) (w : ℕ) : Prop

φ has a resolution refutation all of whose lines have width at most w.

theorem Cslib.Logic.PL.CNF.IsProof.derives {V : Type u_1} [DecidableEq V] {φ : CNF V} {ls : List (Clause V)} {c : Clause V} (h : φ.IsProof ls) (hc : c ∈ ls) : φ.Derives c

Every line of a proof is derivable.

theorem Cslib.Logic.PL.CNF.IsProof.append {V : Type u_1} [DecidableEq V] {φ : CNF V} {ls ls' : List (Clause V)} (h : φ.IsProof ls) (h' : φ.IsProof ls') : φ.IsProof (ls ++ ls')

A proof placed above another proof from the same formula gives a proof.

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

Proofs survive adding clauses to the formula.

theorem Cslib.Logic.PL.CNF.IsProof.fst_mem_vars {V : Type u_1} [DecidableEq V] {φ : CNF V} {ls : List (Clause V)} {c : Clause V} (h : φ.IsProof ls) (hc : c ∈ ls) {l : Literal V} (hl : l ∈ c) : l.1 ∈ φ.vars

The lines of a proof only mention variables of the formula.

theorem Cslib.Logic.PL.CNF.derives_iff_exists_isProof {V : Type u_1} [DecidableEq V] {φ : CNF V} {c : Clause V} : φ.Derives c ↔ ∃ (ls : List (Clause V)), φ.IsProof ls ∧ c ∈ ls

Derivable clauses are the lines of proofs.

theorem Cslib.Logic.PL.CNF.exists_refutableInSize_iff_not_satisfiable {V : Type u_1} [DecidableEq V] {φ : CNF V} : (∃ (s : ℕ), φ.RefutableInSize s) ↔ ¬φ.Satisfiable

Resolution refutes exactly the unsatisfiable formulas, by refutations of some size.

theorem Cslib.Logic.PL.CNF.RefutableInWidth.exists_refutableInSize {V : Type u_1} [DecidableEq V] {φ : CNF V} {w : ℕ} (h : φ.RefutableInWidth w) : ∃ (s : ℕ), φ.RefutableInSize s

A refutation within some width is a refutation of some size.

theorem Cslib.Logic.PL.CNF.RefutableInSize.mono {V : Type u_1} [DecidableEq V] {φ : CNF V} {s t : ℕ} (h : φ.RefutableInSize s) (hst : s ≤ t) : φ.RefutableInSize t

theorem Cslib.Logic.PL.CNF.RefutableInWidth.mono {V : Type u_1} [DecidableEq V] {φ : CNF V} {w w' : ℕ} (h : φ.RefutableInWidth w) (hww' : w ≤ w') : φ.RefutableInWidth w'

Restricting and lifting proofs

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

The lines of a proof from a formula with v fixed do not mention v.

theorem Cslib.Logic.PL.CNF.IsProof.restrict {V : Type u_1} [DecidableEq V] {φ : CNF V} {ls : List (Clause V)} (h : φ.IsProof ls) (v : V) (b : Bool) : ∃ (ls' : List (Clause V)), (φ.restrict v b).IsProof ls' ∧ ls'.length ≤ ls.length ∧ (∀ c ∈ ls, (v, b) ∉ c → ∃ c' ∈ ls', ∀ l ∈ c', l ∈ c) ∧ ∀ (w : ℕ), List.countP (fun (c : Clause V) => decide (w < c.width)) ls' ≤ List.countP (fun (c : Clause V) => decide ((v, b) ∉ c ∧ w < c.width)) ls

Restricting a proof. A proof from φ becomes a proof from φ with v fixed to b, with at most as many lines. Every line of the original proof that does not contain the literal (v, b) is replaced by a line of the new proof with a subset of its literals, and for every w the new proof has at most as many lines wider than w as the original proof has lines without (v, b) wider than w.

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

Lifting a proof. A proof from φ with v fixed to b lifts to a proof from φ. Every line of the original proof is contained in a line of the lifted proof that has, besides its literals, at most the literal (v, !b) falsified by b, and every line of the lifted proof has, besides the literals of a line of the original proof, at most that literal.

theorem Cslib.Logic.PL.CNF.IsProof.comp {V : Type u_1} [DecidableEq V] {φ ψ : CNF V} {ls ls' : List (Clause V)} (hψ : ψ.IsProof ls') (h : φ.IsProof ls) (hψφ : ∀ c ∈ ψ, c ∈ ls) : ∃ (ls'' : List (Clause V)), φ.IsProof (ls'' ++ ls) ∧ (∀ c ∈ ls', c ∈ ls'' ++ ls) ∧ ∀ c ∈ ls'', c ∈ ls'

Composing proofs. A proof from ψ replays on top of a proof from φ among whose lines are all clauses of ψ. The lines added are lines of the proof from ψ, and every line of the proof from ψ is a line of the result.

Restricting proofs by partial assignments

def Cslib.Logic.PL.CNF.restrictBy {V : Type u_1} (φ : CNF V) (ρ : V → Option Bool) : CNF V

φ restricted by the partial assignment ρ, which fixes every variable v with ρ v = some b to b: the clauses that ρ satisfies are dropped, and the literals of fixed variables are removed from the others.

@[simp]

theorem Cslib.Logic.PL.CNF.mem_restrictBy {V : Type u_1} {φ : CNF V} {c : Clause V} {ρ : V → Option Bool} : c ∈ φ.restrictBy ρ ↔ ∃ d ∈ φ, (∀ l ∈ d, ρ l.1 ≠ some l.2) ∧ List.filter (fun (l : Literal V) => decide (ρ l.1 = none)) d = c

theorem Cslib.Logic.PL.CNF.eq_none_of_mem_restrictBy {V : Type u_1} {φ : CNF V} {c : Clause V} {ρ : V → Option Bool} (hc : c ∈ φ.restrictBy ρ) {l : Literal V} (hl : l ∈ c) : ρ l.1 = none

A formula restricted by ρ mentions only variables that ρ does not fix.

theorem Cslib.Logic.PL.CNF.IsProof.eq_none_of_restrictBy {V : Type u_1} [DecidableEq V] {φ : CNF V} {ls : List (Clause V)} {c : Clause V} {ρ : V → Option Bool} (h : (φ.restrictBy ρ).IsProof ls) (hc : c ∈ ls) {l : Literal V} (hl : l ∈ c) : ρ l.1 = none

The lines of a proof from a formula restricted by ρ mention only variables that ρ does not fix.

theorem Cslib.Logic.PL.CNF.IsProof.restrictBy {V : Type u_1} [DecidableEq V] {φ : CNF V} {ls : List (Clause V)} (h : φ.IsProof ls) (ρ : V → Option Bool) : ∃ (ls' : List (Clause V)), (φ.restrictBy ρ).IsProof ls' ∧ (∀ c ∈ ls, (∀ l ∈ c, ρ l.1 ≠ some l.2) → ∃ c' ∈ ls', ∀ l ∈ c', l ∈ c) ∧ ∃ (ks : List (Clause V)), ks.Sublist ls ∧ (∀ c ∈ ks, ∀ l ∈ c, ρ l.1 ≠ some l.2) ∧ List.Forall₂ (fun (c' c : Clause V) => ∀ l ∈ c', l ∈ c) ls' ks

Restricting a proof by a partial assignment. A proof from φ becomes a proof from φ restricted by ρ. Every line of the original proof that ρ does not satisfy is replaced by a line of the new proof with a subset of its literals, and the lines of the new proof have, in order, subsets of the literals of distinct lines of the original proof that ρ does not satisfy. In particular the new proof has at most as many lines with any property inherited by clauses with more literals as the original proof has unsatisfied lines with that property.