Resolution proof compression by splitting explained

In mathematical logic, proof compression by splitting is an algorithm that operates as a post-process on resolution proofs. It was proposed by Scott Cotton in his paper "Two Techniques for Minimizing Resolution Proof".^[1]

The Splitting algorithm is based on the following observation:

Given a proof of unsatisfiability

\pi and a variable x , it is easy to re-arrange (split) the proof in a proof of x and a proof of \neg x and the recombination of these two proofs (by an additional resolution step) may result in a proof smaller than the original.

Note that applying Splitting in a proof

\pi using a variable x does not invalidates a latter application of the algorithm using a differente variable y . Actually, the method proposed by Cotton generates a sequence of proofs \pi _{1} \pi _{2} \ldots , where each proof \pi _{i+1} is the result of applying Splitting to \pi _{i} . During the construction of the sequence, if a proof \pi _{j} happens to be too large, \pi _{j+1} is set to be the smallest proof in \{\pi _{1,} \pi _{2,} \ldots, \pi _{j\}} .

For achieving a better compression/time ratio, a heuristic for variable selection is desirable. For this purpose, Cotton defines the "additivity" of a resolution step (with antecedents

p and n and resolvent r ):\operatorname{add}(r) : = max (|r| -max (|p|, |n|), 0 )

Then, for each variable

v , a score is calculated summing the additivity of all the resolution steps in \pi with pivot v together with the number of these resolution steps. Denoting each score calculated this way by add(v, \pi) , each variable is selected with a probability proportional to its score:p(v) = (\operatorname{add)/((v,) \pi _{i)}{\sum} _{x{\operatorname{add}(x,} \pi _{i)}}}

To split a proof of unsatisfiability

\pi in a proof \pi _{x} of x and a proof \pi _{\neg} of \neg x , Cotton proposes the following:

Let

l denote a literal and p ⊕ _{x} n denote the resolvent of clauses p and n where x \in p and \neg x \in n . Then, define the map \pi _{l} on nodes in the resolution dag of \pi :\pi _{l(c)} : = \begin{cases} c, & if c isaninput \\ \pi _{l(p),} & if c = p ⊕ _{x} n and (l = x or x \notin \pi _{l(p))} \ \pi _{l(n),} & if c = p ⊕ _{x} n and (l = \neg x or \neg x \notin \pi _{l(n))} \\ \pi _{l(p)} ⊕ _{x} \pi _{l(p),} & if x \in \pi _{l(p)} and \neg x \in \pi _{l(n) \end{cases}}

Also, let

o be the empty clause in \pi . Then, \pi _{x} and \pi _{\neg} are obtained by computing \pi _{x(o)} and \pi _{\neg} (o) , respectively.

Notes and References

1. Cotton, Scott. "Two Techniques for Minimizing Resolution Proofs". 13th International Conference on Theory and Applications of Satisfiability Testing, 2010.