{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T04:56:59Z","timestamp":1725425819413},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Although clausal propositional proofs are significantly smaller compared<\/jats:p><jats:p>to resolution proofs, their size is still too large for several<\/jats:p><jats:p>applications. In this paper we present several methods to compress<\/jats:p><jats:p>clausal proofs. These methods are based on a two phase approach. The<\/jats:p><jats:p>first phase consists of a light-weight compression algorithm that can<\/jats:p><jats:p>easily be added to satisfiability solvers that support the emission<\/jats:p><jats:p>of clausal proofs. In the second phase, we propose to use a powerful<\/jats:p><jats:p>off-the-shelf general-purpose compression tool, such as bzip2 and<\/jats:p><jats:p>7z. Sorting literals before compression facilitates a delta encoding,<\/jats:p><jats:p>which combined with variable-byte encoding improves the quality of the<\/jats:p><jats:p>compression. We show that clausal proofs can be compressed by one order<\/jats:p><jats:p>of magnitude by applying both phases.<\/jats:p>","DOI":"10.29007\/sgpl","type":"proceedings-article","created":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T18:04:19Z","timestamp":1516730659000},"page":"21-14","source":"Crossref","is-referenced-by-count":0,"title":["Clausal Proof Compression"],"prefix":"10.29007","volume":"40","author":[{"given":"Marijn","family":"Heule","sequence":"first","affiliation":[]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[]}],"member":"11545","event":{"name":"IWIL-2015. 11th International Workshop on the Implementation of Logics"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T18:04:20Z","timestamp":1516730660000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/fgBF"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/sgpl","relation":{},"ISSN":["2398-7340"],"issn-type":[{"type":"print","value":"2398-7340"}],"subject":[]}}