Resolution proof compression by splitting

{{single source|date=May 2025}}

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".Cotton, Scott. "Two Techniques for Minimizing Resolution Proofs". 13th International Conference on Theory and Applications of Satisfiability Testing, 2010.

The Splitting algorithm is based on the following observation:

Given a proof of unsatisfiability $\backslash pi$ and a variable $x$, it is easy to re-arrange (split) the proof in a proof of $x$ and a proof of $\backslash 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 $\backslash 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 $\backslash pi\_1\; \backslash pi\_2\; \backslash ldots$, where each proof $\backslash pi\_\{i+1\}$ is the result of applying Splitting to $\backslash pi\_i$. During the construction of the sequence, if a proof $\backslash pi\_j$ happens to be too large, $\backslash pi\_\{j+1\}$ is set to be the smallest proof in $\backslash \{\backslash pi\_1,\; \backslash pi\_2,\; \backslash ldots,\; \backslash pi\_j\backslash \}$.

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

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

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

: $p(v)\; =\; \backslash frac\{\backslash operatorname\{add\}(v,\; \backslash pi\_i)\}\{\backslash sum\_x\{\backslash operatorname\{add\}(x,\; \backslash pi\_i)\}\}$

To split a proof of unsatisfiability $\backslash pi$ in a proof $\backslash pi\_x$ of $x$ and a proof $\backslash pi\_\{\backslash neg\; x\}$ of $\backslash neg\; x$, Cotton proposes the following:

Let $l$ denote a literal and $p\; \backslash oplus\; \_x\; n$ denote the resolvent of clauses $p$ and $n$ where $x\; \backslash in\; p$ and $\backslash neg\; x\; \backslash in\; n$. Then, define the map $\backslash pi\_l$ on nodes in the resolution dag of $\backslash pi$:

:$\backslash pi\_l(c)\; :=\; \backslash 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 $\backslash pi$. Then, $\backslash pi\_x$ and $\backslash pi\_\{\backslash neg\; x\}$ are obtained by computing $\backslash pi\_x(o)$ and $\backslash pi\_\{\backslash neg\; x\}(o)$, respectively.