Tree-like resolution

A tree-like resolution derivation (Cslib.Logic.PL.CNF.Derivation) is a derivation by resolution in which every derived clause is used once: a tree whose leaves are clauses of the formula and whose inner nodes resolve the clauses of their two children. Its size is its number of nodes (Cslib.Logic.PL.CNF.Derivation.size). A tree-like derivation unfolds a resolution proof in which a line may be used many times, and conversely gives a proof with at most as many lines (Cslib.Logic.PL.CNF.Derivation.exists_isProof).

Tree-like resolution and DPLL search trees. A decision tree whose leaves are clauses finds a falsified clause of φ (Cslib.DecisionTree.FindsFalsifiedClause) if, on every assignment, the leaf it reaches is a clause of φ that the assignment falsifies. This models the search-tree certificates of Davis, Logemann and Loveland, allowing repeated queries. The correspondence concerns certificates; no solver implementation or runtime bound is given. A tree-like refutation is such a tree, with one leaf for each leaf of the refutation, querying the variable resolved at each node (Cslib.Logic.PL.CNF.Derivation.findsFalsifiedClause_toDecisionTree). Conversely, a decision tree finding falsified clauses gives a tree-like refutation with fewer nodes than twice its number of leaves (Cslib.DecisionTree.FindsFalsifiedClause.exists_derivation): along a path, the clauses reached below each node resolve on the variable queried there to a clause falsified by the answers above it.

Short tree-like refutations are narrow [Ben-Sasson and Wigderson, Theorem 3.3] [BSW01]: a formula with clauses of width at most k and a tree-like refutation of at most 2 ^ b nodes is refutable in width at most k + b (Cslib.Logic.PL.CNF.RefutableInWidth.of_derivation). The two subtrees of the root refute the two restrictions of the formula by the variable resolved there; the smaller has at most half the nodes, so by induction its restriction is refutable in width k + b - 1, and the other in width k + b, which Cslib.Logic.PL.CNF.RefutableInWidth.of_restrict combines.

Main definitions

• Cslib.Logic.PL.CNF.Derivation, Cslib.Logic.PL.CNF.Derivation.size: tree-like derivations and their number of nodes.
• Cslib.Logic.PL.CNF.Derivation.toDecisionTree: the decision tree of a tree-like derivation.
• Cslib.DecisionTree.FindsFalsifiedClause: decision trees finding falsified clauses.

Main results

• Cslib.Logic.PL.CNF.Derivation.restrict: restricting a tree-like derivation.
• Cslib.Logic.PL.CNF.Derivation.findsFalsifiedClause_toDecisionTree, Cslib.DecisionTree.FindsFalsifiedClause.exists_derivation: tree-like refutations and decision trees finding falsified clauses convert into each other.
• Cslib.Logic.PL.CNF.RefutableInWidth.of_derivation: short tree-like refutations are narrow.

References

• E. Ben-Sasson, A. Wigderson, Short proofs are narrow—resolution made simple
• M. Davis, G. Logemann, D. Loveland, A machine program for theorem-proving

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

A tree-like resolution derivation of c from φ: a clause of φ, or the resolvent of the conclusions of two tree-like derivations on a variable occurring positively in the first and negatively in the second.

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

  A clause of φ.

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

  The resolvent of the conclusions of two derivations.

def Cslib.Logic.PL.CNF.Derivation.size {V : Type u_1} [DecidableEq V] {φ : CNF V} {c : Clause V} : φ.Derivation c → ℕ

The number of nodes of a tree-like derivation.

@[simp]

theorem Cslib.Logic.PL.CNF.Derivation.size_mem {V : Type u_1} [DecidableEq V] {φ : CNF V} {c : Clause V} (hc : c ∈ φ) : (mem hc).size = 1

@[simp]

theorem Cslib.Logic.PL.CNF.Derivation.size_resolvent {V : Type u_1} [DecidableEq V] {φ : CNF V} {c₁ c₂ : Clause V} (v : V) (d₁ : φ.Derivation c₁) (d₂ : φ.Derivation c₂) (hv₁ : (v, true) ∈ c₁) (hv₂ : (v, false) ∈ c₂) : (resolvent v d₁ d₂ hv₁ hv₂).size = d₁.size + d₂.size + 1

theorem Cslib.Logic.PL.CNF.Derivation.size_pos {V : Type u_1} [DecidableEq V] {φ : CNF V} {c : Clause V} (d : φ.Derivation c) : 0 < d.size

A tree-like derivation has a node.

theorem Cslib.Logic.PL.CNF.Derivation.derives {V : Type u_1} [DecidableEq V] {φ : CNF V} {c : Clause V} : ∀ (a : φ.Derivation c), φ.Derives c

The conclusion of a tree-like derivation is derivable.

theorem Cslib.Logic.PL.CNF.Derivation.exists_isProof {V : Type u_1} [DecidableEq V] {φ : CNF V} {c : Clause V} (d : φ.Derivation c) : ∃ (ls : List (Clause V)), φ.IsProof ls ∧ c ∈ ls ∧ ls.length ≤ d.size

A tree-like derivation gives a proof with at most as many lines as it has nodes.

theorem Cslib.Logic.PL.CNF.Derivation.refutableInSize {V : Type u_1} [DecidableEq V] {φ : CNF V} (d : φ.Derivation []) : φ.RefutableInSize d.size

A tree-like refutation of s nodes gives a refutation of at most s lines.

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

A clause derived from φ with v fixed does not mention v.

theorem Cslib.Logic.PL.CNF.Derivation.restrict {V : Type u_1} [DecidableEq V] {φ : CNF V} {c : Clause V} (v : V) (b : Bool) (d : φ.Derivation c) (hvc : (v, b) ∉ c) : ∃ (c' : Clause V) (d' : (φ.restrict v b).Derivation c'), (∀ l ∈ c', l ∈ c) ∧ d'.size ≤ d.size

Restricting a tree-like derivation. A tree-like derivation from φ of a clause without the literal (v, b) becomes a tree-like derivation from φ with v fixed to b, with at most as many nodes, of a clause with a subset of its literals.

Decision trees

def Cslib.Logic.PL.CNF.Derivation.toDecisionTree {V : Type u_1} [DecidableEq V] {φ : CNF V} {c : Clause V} : φ.Derivation c → DecisionTree V (Clause V)

The decision tree of a tree-like derivation: a leaf for each clause of the formula used, and a query of the resolved variable at each resolution step, answering false towards the premise with the variable positive.

theorem Cslib.Logic.PL.CNF.Derivation.two_mul_leafCount_toDecisionTree {V : Type u_1} [DecidableEq V] {φ : CNF V} {c : Clause V} (d : φ.Derivation c) : 2 * d.toDecisionTree.leafCount = d.size + 1

The decision tree of a tree-like derivation has one leaf for each leaf of the derivation.

theorem Cslib.Logic.PL.CNF.Derivation.eval_toDecisionTree {V : Type u_1} [DecidableEq V] {φ : CNF V} {c : Clause V} (d : φ.Derivation c) {σ : V → Bool} : Clause.eval σ c = false → d.toDecisionTree.eval σ ∈ φ ∧ Clause.eval σ (d.toDecisionTree.eval σ) = false

On an assignment falsifying the conclusion of a tree-like derivation, its decision tree reaches a clause of the formula falsified by the assignment.

def Cslib.DecisionTree.FindsFalsifiedClause {V : Type u_1} (t : DecisionTree V (Logic.PL.Clause V)) (φ : Logic.PL.CNF V) : Prop

A decision tree with clauses at its leaves finds a falsified clause of φ if, on every assignment, the clause at the leaf it reaches is a clause of φ that the assignment falsifies. These are the search trees of the DPLL procedure on φ.

theorem Cslib.Logic.PL.CNF.Derivation.findsFalsifiedClause_toDecisionTree {V : Type u_1} [DecidableEq V] {φ : CNF V} (d : φ.Derivation []) : d.toDecisionTree.FindsFalsifiedClause φ

A tree-like refutation is a DPLL tree: its decision tree finds a falsified clause.

theorem Cslib.DecisionTree.FindsFalsifiedClause.exists_derivation {V : Type u_1} [DecidableEq V] {φ : Logic.PL.CNF V} {t : DecisionTree V (Logic.PL.Clause V)} (ht : t.FindsFalsifiedClause φ) : ∃ (d : φ.Derivation []), d.size + 1 ≤ 2 * t.leafCount

A DPLL tree is a tree-like refutation: a decision tree finding a falsified clause of φ gives a tree-like refutation of φ with fewer nodes than twice its number of leaves.

Short tree-like refutations are narrow

theorem Cslib.Logic.PL.CNF.RefutableInWidth.of_derivation {V : Type u_1} [DecidableEq V] {φ : CNF V} {k b : ℕ} (hk : ∀ c ∈ φ, c.width ≤ k) {c : Clause V} (d : φ.Derivation c) (hc : c = []) (hd : d.size ≤ 2 ^ b) : φ.RefutableInWidth (k + b)

Short tree-like refutations are narrow [Ben-Sasson and Wigderson, Theorem 3.3] [BSW01]. A formula whose clauses have width at most k, with a tree-like refutation of at most 2 ^ b nodes, is refutable in width at most k + b.