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
):
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
π
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:
p
(
v
)
=
add
(
v
,
π
i
)
∑
x
add
(
x
,
π
i
)
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
π
:
π
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
)
Also, let
o
be the empty clause in
π
. Then,
π
x
and
π
¬
x
are obtained by computing
π
x
(
o
)
and
π
¬
x
(
o
)
, respectively.
