The size–width tradeoff for resolution

Ben-Sasson and Wigderson showed that short resolution refutations can be made narrow: a formula whose clauses have width at most k, over N variables, with a refutation of s lines has a refutation of width at most k + O(√(N log s)) (Cslib.Logic.PL.CNF.exists_refutableInWidth_le_of_refutableInSize). Lower bounds on width thus give lower bounds on size.

The proof fixes variables one at a time. Its core is a lemma about a single variable (Cslib.Logic.PL.CNF.RefutableInWidth.of_restrict): if fixing v to b leaves a formula refutable in width w, and fixing v to !b leaves one refutable in width w + 1, then the formula is refutable in width w + 1, provided its clauses have width at most w + 1. Lifting the first refutation derives the unit clause of v with the value !b, at the cost of one more literal per line, or the empty clause outright. Resolving that unit clause with the clauses containing v with the value b derives the clauses of the second restricted formula, and the second refutation then replays on top.

A line of a refutation is wide when its width exceeds a threshold d. If a refutation has f wide lines, some literal occurs in at least a d / 2N fraction of them, and fixing it to be true satisfies those lines and leaves a refutation of the restricted formula with at most f (1 - d / 2N) wide lines; fixing it to be false leaves at most f of them, over fewer variables. By induction, if f (2N - d) ^ b < (2N) ^ b then the formula is refutable in width max d k + b (Cslib.Logic.PL.CNF.RefutableInWidth.of_refutableInSize). Choosing d and b of order √(N log s) gives the tradeoff.

Main results

• Cslib.Logic.PL.CNF.RefutableInWidth.of_restrict: the key lemma on fixing one variable.
• Cslib.Logic.PL.CNF.RefutableInWidth.of_refutableInSize: refutations with few wide lines can be made narrow.
• Cslib.Logic.PL.CNF.exists_refutableInWidth_le_of_refutableInSize: the size–width tradeoff: a formula with clauses of width at most k over N variables, refutable with s lines, is refutable in width at most k + 2 √(2 N log s) + 2.
• Cslib.Logic.PL.CNF.exp_le_of_refutableInSize: the same as a size lower bound: if refutations need width W ≥ k + 2, they need exp ((W - k - 2)² / 8N) lines.

References

• E. Ben-Sasson, A. Wigderson, Short proofs are narrow—resolution made simple

Fixing one variable

theorem Cslib.Logic.PL.CNF.IsProof.append_of_forall {V : Type u_1} [DecidableEq V] {φ : CNF V} {ls es : List (Clause V)} (h : φ.IsProof ls) (hes : ∀ e ∈ es, e ∈ φ ∨ ∃ c₁ ∈ ls, ∃ c₂ ∈ ls, ∃ (u : V), (u, true) ∈ c₁ ∧ (u, false) ∈ c₂ ∧ e = c₁.resolvent c₂ u) : φ.IsProof (es ++ ls)

Lines resolved from lines of a proof, or clauses of the formula, extend the proof.

theorem Cslib.Logic.PL.CNF.IsProof.of_forall_mem {V : Type u_1} [DecidableEq V] {φ : CNF V} {es : List (Clause V)} (hes : ∀ e ∈ es, e ∈ φ) : φ.IsProof es

Clauses of a formula, listed in any order, form a proof from it.

theorem Cslib.Logic.PL.CNF.width_le_of_mem_restrict {V : Type u_1} [DecidableEq V] {φ : CNF V} {v : V} {b : Bool} {k : ℕ} (hk : ∀ c ∈ φ, c.width ≤ k) {c : Clause V} (hc : c ∈ φ.restrict v b) : c.width ≤ k

Fixing a variable does not widen clauses.

theorem Cslib.Logic.PL.CNF.RefutableInWidth.of_restrict {V : Type u_1} [DecidableEq V] {φ : CNF V} {v : V} {b : Bool} {w : ℕ} (hφ : ∀ c ∈ φ, c.width ≤ w + 1) (h₁ : (φ.restrict v b).RefutableInWidth w) (h₂ : (φ.restrict v !b).RefutableInWidth (w + 1)) : φ.RefutableInWidth (w + 1)

Fixing one variable Ben-Sasson and Wigderson, Lemma 3.2. If the clauses of φ have width at most w + 1, φ with v fixed to b is refutable in width w, and φ with v fixed to !b is refutable in width w + 1, then φ is refutable in width w + 1.

Wide lines

theorem Cslib.Logic.PL.CNF.RefutableInWidth.of_refutableInSize {V : Type u_1} [DecidableEq V] {φ : CNF V} {k s N d b : ℕ} (hk : ∀ c ∈ φ, c.width ≤ k) (hN : φ.vars.toFinset.card ≤ N) (hs : φ.RefutableInSize s) (hsdb : s * (2 * N - d) ^ b < (2 * N) ^ b) : φ.RefutableInWidth (max d k + b)

Refutations with few wide lines can be made narrow [Ben-Sasson and Wigderson, Theorem 3.5] [BSW01]. Let the clauses of φ have width at most k, and let φ have at most N variables. If φ has a refutation of s lines, and s (2N - d) ^ b < (2N) ^ b, then φ is refutable in width at most max d k + b.

The size–width tradeoff

theorem Cslib.Logic.PL.CNF.exists_refutableInWidth_le_of_refutableInSize {V : Type u_1} [DecidableEq V] {φ : CNF V} {k s N : ℕ} (hk : ∀ c ∈ φ, c.width ≤ k) (hN : φ.vars.toFinset.card ≤ N) (hs : φ.RefutableInSize s) : ∃ (w : ℕ), φ.RefutableInWidth w ∧ ↑w ≤ ↑k + 2 * √(2 * ↑N * Real.log ↑s) + 2

The size–width tradeoff [Ben-Sasson and Wigderson, Theorem 3.5 and Corollary 3.6] [BSW01]. A formula whose clauses have width at most k, with at most N variables, that has a refutation of s lines has a refutation of width at most k + 2 √(2 N log s) + 2. Equivalently, a formula that needs width w ≥ k + 2, with N > 0, needs refutations of at least exp ((w - k - 2)² / 8N) lines.

theorem Cslib.Logic.PL.CNF.exp_le_of_refutableInSize {V : Type u_1} [DecidableEq V] {φ : CNF V} {k N W s : ℕ} (hk : ∀ c ∈ φ, c.width ≤ k) (hN : φ.vars.toFinset.card ≤ N) (hW : ∀ (w : ℕ), φ.RefutableInWidth w → W ≤ w) (hkW : k + 2 ≤ W) (hs : φ.RefutableInSize s) : Real.exp ((↑W - ↑k - 2) ^ 2 / (8 * ↑N)) ≤ ↑s

Width lower bounds give size lower bounds [Ben-Sasson and Wigderson, Corollary 3.6] [BSW01]. Let the clauses of φ have width at most k, and let φ have at most N variables. If every resolution refutation of φ has width at least W ≥ k + 2, then every resolution refutation of φ has at least exp ((W - k - 2)² / 8N) lines.