Marijn Heule, Armin Biere,
"Clausal Proof Compression"
: Proc. 11th Intl. Workshop on the Implementation of Logics, Serie EPiC Series in Computing, Vol. 40, EasyChair, Seite(n) 21-26, 2016
Clausal Proof Compression
Sprache des Titels:
Proc. 11th Intl. Workshop on the Implementation of Logics
Although clausal propositional proofs are significantly smaller compared to resolution proofs, their
size on disk is still too large for several applications. In this paper we present several methods to
compress clausal proofs. These methods are based on a two phase approach. The first phase consists
of a light-weight compression algorithm that can easily be added to satisfiability solvers that support
the emission of clausal proofs. In the second phase, we propose to use a powerful off-the-shelf generalpurpose
compression tool, such as bzip2 and 7z. Sorting literals before compression facilitates a delta
encoding, which combined with variable-byte encoding improves the quality of the compression. We
show that clausal proofs can be compressed by one order of magnitude by applying both phases.