mlsanityData to 14 Oct 2026

Efficient Certified RAT Verification

arXiv 1612.02353 ↗First posted 7 Dec 2016cs.LOcited by 13

Not on the map. Why?

Abstract (arXiv)

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.

Key facts. Cited by 13 papers in the map (data through 14 Oct 2026). First posted on arXiv 7 Dec 2016.

Builds on

No reference list yet.

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2021: 1; 2022: 1; 2023: 0; 2024: 3; 2025: 4; 2026: 4.

13 papers.

Sort:

By area:

  1. 2024Leveraging the Context through Multi-Round Interactions for Jailbreaking Attackscited by 36
  2. 2022Certified Symmetry and Dominance Breaking for Combinatorial Optimisationcited by 13
  3. 2024Certified MaxSAT Preprocessingcited by 3
  4. 2025PICID: Proof-Driven Clause Learning in Neural Network Verificationcited by 3
  5. 2025Certifying Pareto-Optimality in Multi-Objective Maximum Satisfiabilitycited by 2
  6. 2021Proof Generation in CDSATcited by 0
  7. 2024How To Discover Short, Shorter, and the Shortest Proofs of Unsatisfiability: A Branch-and-Bound Approach for Resolution Proof Length Minimizationcited by 0
  8. 2025Pseudo-Boolean Proof Logging for Optimal Classical Planningcited by 0
  9. 2025Faster Certified Symmetry Breaking Using Orders With Auxiliary Variablescited by 0
  10. 2026Streaming LRAT Certificates into Lean Theoremscited by 0
  11. 2026Formally Verified Synthesizable Floating-Point Data Types in ARCH HDLcited by 0
  12. 2026LeanCSP: A Framework for Certifying Constraint Reformulation and Solving in Leancited by 0
1 more
  1. 2026Dependable AI-Assisted Engineering: A Formal Framework for AI Participation and Assurance in Safety-Critical Workflowscited by 0