Resolution proof compression by splitting

Proof compression by splitting was proposed by Scott Cotton in his paper "Two Techniques for Minimizing Resolution Proof". Cotton's Splitting algorithm operates as a post-process on resolution proofs.

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 setted 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$):

$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 {add(v,\pi _{i})}{\sum _{x}{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,&{\mbox{if }}c{\mbox{ is an input}}\\\pi _{l}(p),&{\mbox{if }}c=p\oplus _{x}n{\mbox{ and }}(l=x{\mbox{ or }}x\notin \pi _{l}(p))\\\pi _{l}(n),&{\mbox{if }}c=p\oplus _{x}n{\mbox{ and }}(l=\neg x{\mbox{ or }}\neg x\notin \pi _{l}(n))\\\pi _{l}(p)\oplus _{x}\pi _{l}(p),&{\mbox{if }}x\in \pi _{l}(p){\mbox{ 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.