Encyclopedia

Resolution proof compression by splitting

Wikipedia contributorsAdapted for Fathomly · View authors

1 min read
Source updated May 8, 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".

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

$\operatorname {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 {\operatorname {add} (v,\pi _{i})}{\sum _{x}{\operatorname {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,&{\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 $\pi$ . Then, $\pi _{x}$ and $\pi _{\neg x}$ are obtained by computing $\pi _{x}(o)$ and $\pi _{\neg x}(o)$ , respectively.

Watch videos about Resolution proof compression by splittingExplainers and documentaries on YouTube (opens in a new tab)

Sources and credits

This article is adapted from the Wikipedia article “Resolution proof compression by splitting”, written by its contributors and licensed under CC BY-SA 4.0. Fathomly has changed the layout, removed citation markers, navigation and maintenance notices, and adjusted punctuation. This adapted version is shared under the same license. For references, see the original article.

Fathomly is not affiliated with or endorsed by the Wikimedia Foundation. Spotted a problem? Tell us.