Philosophy:Resolution proof compression by splitting

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". The Splitting algorithm is based on the following observation:

Given a proof of unsatisfiability [math]\displaystyle{ \pi }[/math] and a variable [math]\displaystyle{ x }[/math], it is easy to re-arrange (split) the proof in a proof of [math]\displaystyle{ x }[/math] and a proof of [math]\displaystyle{ \neg x }[/math] 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 [math]\displaystyle{ \pi }[/math] using a variable [math]\displaystyle{ x }[/math] does not invalidates a latter application of the algorithm using a differente variable [math]\displaystyle{ y }[/math]. Actually, the method proposed by Cotton generates a sequence of proofs [math]\displaystyle{ \pi_1 \pi_2 \ldots }[/math], where each proof [math]\displaystyle{ \pi_{i+1} }[/math] is the result of applying Splitting to [math]\displaystyle{ \pi_i }[/math]. During the construction of the sequence, if a proof [math]\displaystyle{ \pi_j }[/math] happens to be too large, [math]\displaystyle{ \pi_{j+1} }[/math] is set to be the smallest proof in [math]\displaystyle{ \{\pi_1, \pi_2, \ldots, \pi_j\} }[/math].

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 [math]\displaystyle{ p }[/math] and [math]\displaystyle{ n }[/math] and resolvent [math]\displaystyle{ r }[/math]):

[math]\displaystyle{ \operatorname{add}(r) := \max(|r|-\max(|p|, |n|), 0) }[/math]

Then, for each variable [math]\displaystyle{ v }[/math], a score is calculated summing the additivity of all the resolution steps in [math]\displaystyle{ \pi }[/math] with pivot [math]\displaystyle{ v }[/math] together with the number of these resolution steps. Denoting each score calculated this way by [math]\displaystyle{ add(v, \pi) }[/math], each variable is selected with a probability proportional to its score:

[math]\displaystyle{ p(v) = \frac{\operatorname{add}(v, \pi_i)}{\sum_x{\operatorname{add}(x, \pi_i)}} }[/math]

To split a proof of unsatisfiability [math]\displaystyle{ \pi }[/math] in a proof [math]\displaystyle{ \pi_x }[/math] of [math]\displaystyle{ x }[/math] and a proof [math]\displaystyle{ \pi_{\neg x} }[/math] of [math]\displaystyle{ \neg x }[/math], Cotton proposes the following:

Let [math]\displaystyle{ l }[/math] denote a literal and [math]\displaystyle{ p \oplus _x n }[/math] denote the resolvent of clauses [math]\displaystyle{ p }[/math] and [math]\displaystyle{ n }[/math] where [math]\displaystyle{ x \in p }[/math] and [math]\displaystyle{ \neg x \in n }[/math]. Then, define the map [math]\displaystyle{ \pi_l }[/math] on nodes in the resolution dag of [math]\displaystyle{ \pi }[/math]:

[math]\displaystyle{ \pi_l(c) := \begin{cases} c, & \text{if } c \text{ is an input} \\ \pi_l(p), & \text{if } c = p \oplus_x n \text{ and } (l = x \text{ or } x \notin \pi_l(p)) \\ \pi_l(n), & \text{if } c = p \oplus_x n \text{ and } (l = \neg x \mbox{ or } \neg x \notin \pi_l(n)) \\ \pi_l(p) \oplus_x \pi_l(p), & \text{if } x \in \pi_l(p) \text{ and } \neg x \in \pi_l(n) \end{cases} }[/math]

Also, let [math]\displaystyle{ o }[/math] be the empty clause in [math]\displaystyle{ \pi }[/math]. Then, [math]\displaystyle{ \pi_x }[/math] and [math]\displaystyle{ \pi_{\neg x} }[/math] are obtained by computing [math]\displaystyle{ \pi_x(o) }[/math] and [math]\displaystyle{ \pi_{\neg x}(o) }[/math], respectively.