Efficient Verified (UN)SAT Certificate Checking

Research output: Contribution to journalArticle

Abstract

SAT solvers decide the satisfiability of Boolean formulas in conjunctive
normal form. They are commonly used for software and hardware verification.
Modern SAT solvers are highly complex and optimized programs. As a single bug in the solver may invalidate the verification of many systems, SAT solvers output certificates for their answer, which are then checked independently. However, even certificate checking requires highly optimized non-trivial programs. This paper presents the first SAT solver certificate checker that is formally verified down to the integer sequence representing the formula. Our tool supports the full DRAT standard, and is even faster than the unverified state-of-the-art tool drat-trim, on a realistic set of benchmarks drawn from the 2016 and 2017 SAT competitions. An optional multi-threaded mode further reduces the runtime, in particular for big certificates.

Bibliographical metadata

Original languageEnglish
JournalJournal of Automated Reasoning
Publication statusAccepted/In press - 30 Apr 2019

Related information

Researchers

View all