5th Year Master of Computer Science Thesis Presentation
Speaker
CAYDEN CODEL
Masters Student
Computer Science Department
Carnegie Mellon University
When
-
Where
In Person
Description
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 Additional Information