Thursday, November 14, 2024, 3pm

One reason for the widespread adoption of SAT solvers is that they are trustworthy: their answers can be checked with verified software. In particular, many SAT solvers can emit proof certificates of unsatisfiability that are efficient to check. However, the standard proof systems in use today struggle to succinctly express proofs for problem instances with a high degree of symmetry.

In this talk, we discuss our recent work on proof checking tools for the substitution redundancy (SR) proof system. We discuss a few problems that admit short SR proofs, as well as how we can express and check those proofs. Our verified proof checker was developed in the Lean theorem prover.

Presented in Partial Fulfillment of the CSD Speaking Skills Requirement

Event Type: Speaking Skills
Room Number: In Person
Building: Newell-Simon 3305
Speaker's Name: CAYDEN CODEL
Speaker Website: crcodel.com
Speaker's Professional Title: Ph.D. Student, Computer Science Department, Carnegie Mellon University
Talk Title: Verified Substitution Redundancy Checking for SAT Solving
Event Poster Title: Poster
Event Poster URL: www.cs.cmu.edu…
For More Information: matthewstewart@cmu.edu
Affiliations: Computer Science Department (CSD)
Organization(s): School of Computer Science
Event Website Title: Event Website
Event Website URL: csd.cmu.edu…