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

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

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

p ( v ) = add ⁡ ( v , π i ) ∑ x add ⁡ ( x , π i ) {\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 π x {\displaystyle \pi _{x}} of x {\displaystyle x} and a proof π ¬ x {\displaystyle \pi _{\neg x}} of ¬ x {\displaystyle \neg x} , Cotton proposes the following:

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

π l ( c ) := { c , if  c  is an input π l ( p ) , if  c = p ⊕ x n  and  ( l = x  or  x ∉ π l ( p ) ) π l ( n ) , if  c = p ⊕ x n  and  ( l = ¬ x  or  ¬ x ∉ π l ( n ) ) π l ( p ) ⊕ x π l ( p ) , if  x ∈ π l ( p )  and  ¬ x ∈ π l ( n ) {\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 o {\displaystyle o} be the empty clause in π {\displaystyle \pi } . Then, π x {\displaystyle \pi _{x}} and π ¬ x {\displaystyle \pi _{\neg x}} are obtained by computing π x ( o ) {\displaystyle \pi _{x}(o)} and π ¬ x ( o ) {\displaystyle \pi _{\neg x}(o)} , respectively.