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".^[1]

The Splitting algorithm is based on the following observation:

Given a proof of unsatisfiability ${\displaystyle \pi }$ and a variable ${\displaystyle x}$, it is easy to re-arrange (split) the proof in a proof of ${\displaystyle x}$ and a proof of ${\displaystyle \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 ${\displaystyle \pi }$ using a variable ${\displaystyle x}$ does not invalidates a latter application of the algorithm using a differente variable ${\displaystyle y}$. Actually, the method proposed by Cotton^[1] generates a sequence of proofs ${\displaystyle \pi _{1}\pi _{2}\ldots }$, where each proof ${\displaystyle \pi _{i+1}}$ is the result of applying Splitting to ${\displaystyle \pi _{i}}$. During the construction of the sequence, if a proof ${\displaystyle \pi _{j}}$ happens to be too large, ${\displaystyle \pi _{j+1}}$ is set to be the smallest proof in ${\displaystyle \{\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^[1] defines the "additivity" of a resolution step (with antecedents ${\displaystyle p}$ and ${\displaystyle n}$ and resolvent ${\displaystyle r}$):

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

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

${\displaystyle p(v)={\frac {\operatorname {add} (v,\pi _{i})}{\sum _{x}{\operatorname {add} (x,\pi _{i})}}}}$

To split a proof of unsatisfiability ${\displaystyle \pi }$ in a proof ${\displaystyle \pi _{x}}$ of ${\displaystyle x}$ and a proof ${\displaystyle \pi _{\neg x}}$ of ${\displaystyle \neg x}$, Cotton ^[1] proposes the following:

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

${\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}}}$

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