Propositional Proof Skeletons

Autor: Joseph E. Reeves, Benjamin Kiesl-Reiter, Marijn J. H. Heule
Rok vydání: 2023
Zdroj: Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783031308222
DOI: 10.1007/978-3-031-30823-9_17
Popis: Modern SAT solvers produce proofs of unsatisfiability to justify the correctness of their results. These proofs, which are usually represented in the well-known DRAT format, can often become huge, requiring multiple gigabytes of disk storage. We present a technique for semantic proof compression that selects a subset of important clauses from a proof and stores them as a so-called proof skeleton. This proof skeleton can later be used to efficiently reconstruct a full proof by exploiting parallelism. We implemented our approach on top of the award-winning SAT solver CaDiCaL and the proof checker DRAT-trim. In an experimental evaluation, we demonstrate that we can compress proofs into skeletons that are 100 to 5, 000 times smaller than the original proofs. For almost all problems, proof reconstruction using a skeleton improves the solving time on a single core, and is around five times faster when using 24 cores.
Databáze: OpenAIRE