Computer Science Speaking Skills Talk

— 1:00pm

In Person - Gates Hillman 8102

JOSEPH REEVES , Ph.D. Student, Computer Science Department, Carnegie Mellon University

Propositional Proof Skeletons

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. Presented at PLunch Seminar Series

Presented in Partial Fulfillment of the CSD Speaking Skills Requirement.