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 $\pi$ and a variable $x$, it is easy to re-arrange (split) the proof in a proof of $x$ and a proof of $\mathrm{\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\dots$, 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,\dots ,{\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$):

$\mathrm{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{\mathrm{add}(v,{\pi }_i)}{\sum _x\mathrm{add}(x,{\pi }_i)}$

To split a proof of unsatisfiability $\pi$ in a proof ${\pi }_x$ of $x$ and a proof ${\pi }_{\mathrm{\neg }x}$ of $\mathrm{\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 $\mathrm{\neg }x\in n$. Then, define the map ${\pi }_l$ on nodes in the resolution dag of $\pi$:

${\pi }_l(c):=\{\begin{array}{ll}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=\mathrm{\neg }x\text{ or }\mathrm{\neg }x\notin {\pi }_l(n))\\ {\pi }_l(p){\oplus }_x{\pi }_l(p),& \text{if }x\in {\pi }_l(p)\text{ and }\mathrm{\neg }x\in {\pi }_l(n)\end{array}$

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