Skip to main content
main-content

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

04.06.2019 | Ausgabe 3/2020 Open Access

Journal of Automated Reasoning 3/2020

Efficient Verified (UN)SAT Certificate Checking

Zeitschrift:
Journal of Automated Reasoning > Ausgabe 3/2020
Autor:
Peter Lammich
Wichtige Hinweise

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

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.
Literatur
Über diesen Artikel

Weitere Artikel der Ausgabe 3/2020

Journal of Automated Reasoning 3/2020 Zur Ausgabe

Premium Partner