The GRAT tool chain -- efficient (UN)SAT certificate checking with formal correctness guarantees. We present the GRAT tool chain, which provides an efficient and formally verified SAT and UNSAT certificate checker. It utilizes a two phase approach: The highly optimized gratgen tool converts a DRAT certificate to a GRAT certificate, which is then checked by the formally verified gratchk tool. On a realistic benchmark suite drawn from the 2016 SAT competition, our approach is faster than the unverified standard tool drat-trim, and significantly faster than the formally verified LRAT tool. An optional multithreaded mode allows for even faster checking of a single certificate.
Keywords for this software
References in zbMATH (referenced in 5 articles )
Showing results 1 to 5 of 5.
- Lammich, Peter: Efficient verified (UN)SAT certificate checking (2020)
- Tonello, Elisa; Farcot, Etienne; Chaouiya, Claudine: Local negative circuits and cyclic attractors in Boolean networks with at most five components (2019)
- Lochbihler, Andreas: Fast machine words in Isabelle/HOL (2018)
- Schlichtkrull, Anders: Formalization of the resolution calculus for first-order logic (2018)
- Lammich, Peter: The GRAT tool chain -- efficient (UN)SAT certificate checking with formal correctness guarantees (2017)