Source-linked AI summary
Efficient Certified RAT Verification
Luís Cruz-Filipe, Marijn Heule, Warren Hunt, Matt Kaufmann, Peter Schneider-Kamp
TL;DR
SAT proof validation needs a trusted and efficient checker because DRAT checking is costly and solver errors can invalidate unsatisfiability claims. The paper introduces LRAT, a hint-extended format implemented in certified Coq and ACL2 checkers. LRAT supports state-of-the-art RAT proofs while enabling certified checking with reasonable overhead and, in ACL2, near non-certified speed.
Problem
SAT solvers need trusted validation of unsatisfiability proofs, but checking the widely supported DRAT format remains costly even with optimized implementations.
Method
The paper introduces LRAT, a hint-extended clausal-proof format, and develops certified checkers for it in Coq and ACL2.
Results
LRAT supports RAT proofs and enables efficient certified checking; the ACL2 checker is almost as fast as, and sometimes faster than, non-certified DRAT-trim checking.
Takeaways & Limitations
Certified checking of unsatisfiability proofs can be achieved with reasonable overhead while retaining support for techniques used by state-of-the-art SAT solvers.
Takeaways & Limitations
At the reported stage, the ACL2 checker had not implemented entailment checking, although the authors state it could be added similarly to the Coq checker.
Abstract
from arXiv · showhide
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.
1 Introduction
SAT solvers should produce checkable unsatisfiability proofs because solver bugs can invalidate correctness claims. LRAT combines an expressive clausal-proof format with hints designed for efficient certified validation.
- SAT proofs provide a trusted-checking layer for unsatisfiability results, which matters because solver bugs could invalidate hardware or software correctness claims.
- Clausal proofs are widely supported because they modify formulas by adding or deleting clauses, while DRAT is the most widely supported format.
- DRAT is easy for solvers to produce, but checking remains costly even with watch pointers and could be strengthened through highly trusted systems.
- LRAT introduces a new expressive format intended to enable efficient certified checkers, including implementations in Coq and ACL2.
- Sorted clauses, hints, and resolution candidates let LRAT validation detect literal issues simply and scan the formula once for resolution candidates.
2 Background on Clausal Proof Checking
Clausal proof checking validates redundant additions while treating deletions as automatically safe. DRAT uses unit propagation to check AT and RAT redundancy as proofs modify the formula step by step.
- Clause additions must preserve satisfiability and be checked, whereas deletions trivially preserve satisfiability and mainly reduce validation costs.
- Unit Clause Propagation repeatedly removes complements of unit literals until no more removals are possible or a clause becomes empty, producing a conflict.
- Asymmetric Tautology holds when propagating the negation of a clause against the formula results in a conflict.
- Resolution Asymmetric Tautology generalizes AT by requiring a pivot whose complementary occurrences yield resolvents satisfying AT.
- DRAT processes proof lines sequentially, deleting marked clauses and adding unmarked clauses only after validating their RAT property against the current formula.
3 Introducing the LRAT Format
LRAT extends hint-based proof checking to RAT clauses while imposing syntax that makes validation straightforward. DRAT-trim can generate LRAT proofs, whose structure is illustrated through examples and formal grammar.
- LRAT extends GRIT with RAT support, preserving efficient hint-guided checking while covering clauses expressible in DRAT.
- RAT lines identify a pivot, enumerate clauses containing its negation, and provide UCP hints for each resulting resolvent.
- LRAT omits original CNF clauses from the proof and extends deletion syntax, with an example showing equivalent DRUP, GRIT, and LRAT proofs without RAT clauses.
- An LRAT line begins with a clause identifier and literals, followed by hints where negative identifiers mark RAT candidates and positive identifiers guide unit propagation.
- AT and RAT lines share LRAT syntax, with AT represented as a special case containing a non-empty list of only positive hints.
- DRAT-trim emits LRAT proofs after validating and optimizing DRAT proofs, avoiding direct solver-side generation overhead.
4 Extending the GRIT Checker to LRAT
The paper extends a formalized GRIT checker to the full LRAT syntax by adding RAT checking, certified oracle actions, and entailment checking. The resulting Coq checker is correct by construction and supports certified validation of complete and partial LRAT proofs.
- The formalization handles both LRAT extensions: positive hints before negative hints and cases with no positive hints after a negative hint.These cases make the RAT results more complex than the earlier GRIT formalization.
- RAT checking preserves satisfiability when its witness-driven check succeeds, allowing the required clause to be added to the CNF.The main RAT theorem states that satisfiability of the current CNF implies satisfiability after adding the pivot-prefixed clause.
- The extension adds RAT actions to the oracle and checker, with RAT_check_run iterating through candidate clauses and applying the supplied propagation witnesses.The RAT procedure examines clauses containing the negated pivot and uses witness lists to guide propagation or recursive checking.
- The full LRAT checker is correct by construction: a successful check guarantees that the input CNF is unsatisfiable, independently of oracle implementation errors.The universal quantification over the oracle protects correctness from errors in the oracle and its interface.
- Partial proof checking is expressed as a reduction: each verified proof segment transforms one CNF into another while preserving satisfiability.The checker returns both a Boolean result and the resulting CNF, enabling entailment checking between intermediate formulas.
- The certified Coq checker verified the Boolean Pythagorean Triples transformation proof in 8 minutes and 25 seconds, including approximately 15 seconds for entailment checking.The proof was the only SAT-related step from the original development that the earlier checker could not verify.
5 LRAT Checker in ACL2
The paper extends an ACL2-based DRAT checker to certified LRAT proof checking and verifies its correctness in ACL2. On a 68,667-clause transformation proof, the checker validates every clause addition in under 9 seconds, nearly matching non-certified checking and DRAT-to-LRAT conversion.
- Checker construction: The ACL2 extension is certified and checks the validity of UNSAT proofs in the LRAT format using the ACL2 theorem-proving system.The extension builds on an existing ACL2-based DRAT checker.
- Correctness: The correctness theorem states that a valid formula and refutation proof imply that the formula is unsatisfiable.ACL2 establishes this theorem through its defthm command.
- Implementation: The checker represents formulas with applicative hash tables and verifies each proof step as a redundant extension of the current formula.RAT checks are among the functions invoked by the proof recognizer.
- Definitions: The ACL2 formalization defines satisfiability as the existence of an assignment that satisfies the formula.The implementation separates assignment validity from the existential satisfiability definition.
- Results: 68,667 clauses are checked in less than 9 seconds, with certified LRAT checking almost as fast as non-certified checking and DRAT-to-LRAT conversion.The entailment-checking component was not yet implemented in the ACL2 checker.
6 Conclusions
The paper introduces LRAT, a clausal proof format extending GRIT to support techniques used by state-of-the-art SAT solvers, and demonstrates certified checking in Coq and ACL2. The ACL2 checker is nearly as fast as, and sometimes faster than, non-certified DRAT-trim checking, while the Coq checker also verifies a previously unresolved transformation proof.
- Contributions: LRAT extends GRIT to support all techniques used in state-of-the-art SAT solvers and enables efficient certified UNSAT proof checkers in Coq and ACL2.The format is presented as a novel approach to clausal proof checking.
- Performance: The ACL2 LRAT checker is almost as fast as, and sometimes faster than, non-certified DRAT-trim checking of the corresponding DRAT proof.The comparison supports the claim that certified checking can have reasonable overhead.
- Applications: The Coq checker verifies the transformation proof from the Boolean Pythagorean Triples problem, addressing the only SAT-related step previously left unchecked.Its entailment-checking capability enables verification of transformation proofs.