Computer Science Speaking Skills Talk

— 1:00pm

Location:
In Person - Gates Hillman 8102

Speaker:
JOSEPH REEVES , Ph.D. Student, Computer Science Department, Carnegie Mellon University
https://www.cs.cmu.edu/~jereeves/

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.