5th Year Master of Computer Science Thesis Presentation
— 10:30am
Location:
In Person
-
Charlotte, North Carolina
Speaker:
CAYDEN CODEL
,
Masters StudentComputer Science DepartmentCarnegie Mellon University
https://www.linkedin.com/in/cayden-codel-28b143181
Verifying SAT Encodings in Lean
Satisfiability (SAT) solvers are versatile tools that can help solve a wide array of problems. For satisfiable instances, solvers output candidate solutions that can be efficiently checked. For unsatisfiable instances, many solvers emit proofs of unsatisfiability that can also be efficiently and formally checked. Thus, we can formally check—we can trust—SAT solver results for any given problem instance.
However, many applications have problem instances that are encoded into SAT, rather than expressed in SAT natively. For any problem instance, there are often many choices of encoding. These encodings range in size and complexity, and the choice of encoding has a direct impact on solver performance. But crucially, if the encoding is not correct, we cannot trust solver results. Formal correctness proofs of the encodings are required to ensure that trust.
In this work, we introduce a library for formally verifying SAT encodings. We present formal verifications of several encodings for the n-variable XOR function and the at-most-one function. We also verify an encoding of the at-most-k function. Our proofs were completed using the interactive theorem prover Lean. The methods of formally verifying these encodings extend beyond their applications, and so this library serves as a basis for future encoding verification efforts.
Thesis Committee:
Marijn Heule (Chair)
Jeremy Avigad
Bryan Parno
For More Information:
tracyf@cs.cmu.edu