Efficient Certified RAT Verification

TL;DR

This paper introduces LRAT, an extended proof format for SAT solvers that enables faster and simpler validation, with certified checkers implemented in Coq and ACL2 to ensure correctness.

Contribution

The paper proposes LRAT, a new proof format extending DRAT with hints, and provides certified checkers in Coq and ACL2 for reliable validation.

Findings

LRAT significantly speeds up proof validation.

Certified checkers in Coq and ACL2 verify LRAT proofs correctly.

LRAT facilitates integration with trusted proof systems.

Abstract

Clausal proofs have become a popular approach to validate the results of SAT solvers. However, validating clausal proofs in the most widely supported format (DRAT) is expensive even in highly optimized implementations. We present a new format, called LRAT, which extends the DRAT format with hints that facilitate a simple and fast validation algorithm. Checking validity of LRAT proofs can be implemented using trusted systems such as the languages supported by theorem provers. We demonstrate this by implementing two certified LRAT checkers, one in Coq and one in ACL2.