DRAT-trim
DRAT-trim: efficient checking and trimming using expressive clausal proofs. The DRAT-trim tool is a satisfiability proof checker based on the new DRAT proof format. Unlike its predecessor, DRUP-trim, all presently known SAT solving and preprocessing techniques can be validated using DRAT-trim. Checking time of a proof is comparable to the running time of the proof-producing solver. Memory usage is also similar to solving memory consumption, which overcomes a major hurdle of resolution-based proof checkers. The DRAT-trim tool can emit trimmed formulas, optimized proofs, and new TraceCheck$^{ + }$ dependency graphs. We describe the output that is produced, what optimizations have been made to check RAT clauses, and potential applications of the tool.
Keywords for this software
References in zbMATH (referenced in 10 articles , 1 standard article )
Showing results 1 to 10 of 10.
Sorted by year (- Cheung, Kevin K.H.; Gleixner, Ambros; Steffy, Daniel E.: Verifying integer programming results (2017)
- Heule, Marijn J.H.; Seidl, Martina; Biere, Armin: Solution validation and extraction for QBF preprocessing (2017)
- Miller, Dale: Proof checking and logic programming (2017)
- Zulkoski, Edward; Bright, Curtis; Heinle, Albert; Kotsireas, Ilias; Czarnecki, Krzysztof; Ganesh, Vijay: Combining SAT solvers with computer algebra systems to verify combinatorial conjectures (2017)
- Codish, Michael; Frank, Michael; Itzhakov, Avraham; Miller, Alice: Computing the Ramsey number $R(4,3,3)$ using abstraction and symmetry breaking (2016)
- Kevin K. H. Cheung, Ambros Gleixner, Daniel E. Steffy: Verifying Integer Programming Results (2016) arXiv
- Davis, Jared; Myreen, Magnus O.: The reflective Milawa theorem prover is sound (down to the machine code that runs it) (2015)
- Heule, Marijn J.H.; Hunt, Warren A.jun.; Wetzler, Nathan: Expressing symmetry breaking in DRAT proofs (2015)
- Miller, Dale: Proof checking and logic programming (2015)
- Wetzler, Nathan; Heule, Marijn J. H.; Hunt, Warren A. jun.: DRAT-trim: efficient checking and trimming using expressive clausal proofs (2014)