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 $\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)={\frac {\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 x}$ of $\neg x$, Cotton proposes the following:

Let $l$ denote a literal and $p\oplus _{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,&{\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}}$

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