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".

The Splitting algorithm is based on the following observation:

Given a proof of unsatisfiability π and a variable x , it is easy to re-arrange (split) the proof in a proof of x and a proof of ¬ 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 π 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 π 1 π 2 … , where each proof π i + 1 is the result of applying Splitting to π i . During the construction of the sequence, if a proof π j happens to be too large, π j + 1 is set to be the smallest proof in { π 1 , π 2 , … , π 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 ):

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

To split a proof of unsatisfiability π in a proof π x of x and a proof π ¬ x of ¬ x , Cotton proposes the following:

Let l denote a literal and p ⊕ x n denote the resolvent of clauses p and n where x ∈ p and ¬ x ∈ n . Then, define the map π l on nodes in the resolution dag of π :

Also, let o be the empty clause in π . Then, π x and π ¬ x are obtained by computing π x ( o ) and π ¬ x ( o ) , respectively.