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.

References in zbMATH (referenced in 17 articles , 1 standard article )

Showing results 1 to 17 of 17.
Sorted by year (citations)

  1. Slaney, John; Woltzenlogel Paleo, Bruno: Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (2018)
  2. Cheung, Kevin K.H.; Gleixner, Ambros; Steffy, Daniel E.: Verifying integer programming results (2017)
  3. Cruz-Filipe, Luís; Heule, Marijn J.H.; Hunt Jr., Warren A.; Kaufmann, Matt; Schneider-Kamp, Peter: Efficient certified RAT verification (2017)
  4. Heule, Marijn; Hunt, Warren jun.; Kaufmann, Matt; Wetzler, Nathan: Efficient, verified checking of propositional proofs (2017)
  5. Heule, Marijn J.H.; Seidl, Martina; Biere, Armin: Solution validation and extraction for QBF preprocessing (2017)
  6. Lammich, Peter: The GRAT tool chain -- efficient (UN)SAT certificate checking with formal correctness guarantees (2017)
  7. Miller, Dale: Proof checking and logic programming (2017)
  8. Zulkoski, Edward; Bright, Curtis; Heinle, Albert; Kotsireas, Ilias; Czarnecki, Krzysztof; Ganesh, Vijay: Combining SAT solvers with computer algebra systems to verify combinatorial conjectures (2017)
  9. Codish, Michael; Frank, Michael; Itzhakov, Avraham; Miller, Alice: Computing the Ramsey number $R(4,3,3)$ using abstraction and symmetry breaking (2016)
  10. Heule, Marijn J.H.; Kullmann, Oliver; Marek, Victor W.: Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer (2016)
  11. Kevin K. H. Cheung, Ambros Gleixner, Daniel E. Steffy: Verifying Integer Programming Results (2016) arXiv
  12. Philipp, Tobias; Rebola-Pardo, Adrián: DRAT proofs for XOR reasoning (2016)
  13. Davis, Jared; Myreen, Magnus O.: The reflective Milawa theorem prover is sound (down to the machine code that runs it) (2015)
  14. Heule, Marijn J.H.; Hunt, Warren A.jun.; Wetzler, Nathan: Expressing symmetry breaking in DRAT proofs (2015)
  15. Miller, Dale: Proof checking and logic programming (2015)
  16. Philipp, Tobias: An expressive model for instance decomposition based parallel SAT solvers (2015)
  17. Wetzler, Nathan; Heule, Marijn J. H.; Hunt, Warren A. jun.: DRAT-trim: efficient checking and trimming using expressive clausal proofs (2014)