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".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 $\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_$ 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_$ is set to be the smallest proof in $\$.

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(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$

To split a proof of unsatisfiability $\pi$ in a proof $\pi_x$ of $x$ and a proof $\pi_$ 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 c, & \text c \text \\ \pi_l(p), & \text c = p \oplus_x n \text (l = x \text x \notin \pi_l(p)) \\ \pi_l(n), & \text c = p \oplus_x n \text (l = \neg x \mbox \neg x \notin \pi_l(n)) \\ \pi_l(p) \oplus_x \pi_l(p), & \text x \in \pi_l(p) \text \neg x \in \pi_l(n) \end$

Also, let $o$ be the empty clause in $\pi$. Then, $\pi_x$ and $\pi_$ are obtained by computing $\pi_x(o)$ and $\pi_(o)$, respectively.

Notes

{{reflist

Proof theory