The DRAT format and DRAT-trim checker

2016/10/19 by Marijn J. H. Heule, Heule, Marijn J. H. · 2 citations
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Natural Language Processing Techniques

paper · pdf · doi:10.48550/arxiv.1610.06229

openalex publication_date 2016/10/19 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

This document describes the DRAT format for clausal proofs and the DRAT-trim proof checker.

Cited by

• Monochromatic 4-AP avoidance in 2-colorings of Z/pZ for primes p >= 5 and a computation of W_c(4,2)
• Short proofs without interference

Related

• Axioms vs. rewrite rules: from completeness to cut elimination
• Resolution structure in HornSAT and CNFSAT
• Fast Verifying Proofs of Propositional Unsatisfiability via Window Shifting
• Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA\n (Full Paper)
• Towards the shortest DRAT proof of the Pigeonhole Principle