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 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, then solver results are not trustworthy. Formal correctness proofs of the encodings ensure that trust.

In this work, we introduce a library for formally verifying SAT encodings. We present formal verifications of encodings for the n-variable XOR function and the at-most-one function. We also verify an encoding of the at-most-k function. We completed our proofs using the interactive theorem prover Lean. The methods we developed of formally verifying these encodings extend beyond their applications, and so this library serves as a basis for future encoding verification efforts.

60 pages

Thesis Committee:
Marijn Heule (Co-Chair)
Jeremy Avigad (Co-Chair)
Bryan Parno

Srinivasan Seshan, Head, Computer Science Department
Martial Hebert, Dean, School of Computer Science

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu