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 SeriesPresented in Partial Fulfillment of the CSD Speaking Skills Requirement.