{{single source|date=May 2025}} In [[mathematical logic]], '''[[proof compression]] by splitting''' is an [[algorithm]] that operates as a post-process on [[resolution (logic)|resolution]] proofs. It was proposed by Scott Cotton in his paper "Two Techniques for Minimizing Resolution Proof".<ref name=Cotton>Cotton, Scott. "Two Techniques for Minimizing Resolution Proofs". 13th International Conference on Theory and Applications of Satisfiability Testing, 2010.</ref>
The Splitting algorithm is based on the following observation:
Given a proof of unsatisfiability <math>\pi</math> and a variable <math>x</math>, it is easy to re-arrange (split) the proof in a proof of <math>x</math> and a proof of <math>\neg x </math> 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 <math>\pi</math> using a variable <math>x</math> does not invalidates a latter application of the algorithm using a differente variable <math>y</math>. Actually, the method proposed by Cotton<ref name=Cotton /> generates a sequence of proofs <math>\pi_1 \pi_2 \ldots</math>, where each proof <math>\pi_{i+1}</math> is the result of applying Splitting to <math>\pi_i</math>. During the construction of the sequence, if a proof <math>\pi_j</math> happens to be too large, <math>\pi_{j+1}</math> is set to be the smallest proof in <math>\{\pi_1, \pi_2, \ldots, \pi_j\}</math>.
For achieving a better compression/time ratio, a heuristic for variable selection is desirable. For this purpose, Cotton<ref name=Cotton /> defines the "additivity" of a resolution step (with antecedents <math>p</math> and <math>n</math> and resolvent <math>r</math>):
: <math>\operatorname{add}(r) := \max(|r|-\max(|p|, |n|), 0) </math>
Then, for each variable <math>v</math>, a score is calculated summing the additivity of all the resolution steps in <math>\pi</math> with pivot <math>v</math> together with the number of these resolution steps. Denoting each score calculated this way by <math>add(v, \pi)</math>, each variable is selected with a probability proportional to its score:
: <math>p(v) = \frac{\operatorname{add}(v, \pi_i)}{\sum_x{\operatorname{add}(x, \pi_i)}}</math>
To split a proof of unsatisfiability <math>\pi</math> in a proof <math>\pi_x</math> of <math>x</math> and a proof <math>\pi_{\neg x}</math> of <math>\neg x</math>, Cotton <ref name=Cotton /> proposes the following:
Let <math>l</math> denote a literal and <math>p \oplus _x n</math> denote the resolvent of clauses <math>p</math> and <math>n</math> where <math>x \in p</math> and <math>\neg x \in n</math>. Then, define the map <math>\pi_l</math> on nodes in the resolution dag of <math>\pi</math>:
:<math>\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} </math>
Also, let <math>o</math> be the empty clause in <math>\pi</math>. Then, <math>\pi_x</math> and <math>\pi_{\neg x}</math> are obtained by computing <math>\pi_x(o)</math> and <math>\pi_{\neg x}(o)</math>, respectively.
== Notes == {{reflist}}
[[Category:Proof theory]]