Clausal Proof Compression

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.