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 31 articles , 1 standard article )

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

1 2 next

  1. Bright, Curtis; Cheung, Kevin; Stevens, Brett; Roy, Dominique; Kotsireas, Ilias; Ganesh, Vijay: A nonexistence certificate for projective planes of order ten with weight 15 codewords (2020)
  2. Heule, Marijn J. H.; Kiesl, Benjamin; Biere, Armin: Strong extension-free proof systems (2020)
  3. Kiesl, Benjamin; Rebola-Pardo, Adrián; Heule, Marijn J. H.; Biere, Armin: Simulating strong practical proof systems with extended resolution (2020)
  4. Lammich, Peter: Efficient verified (UN)SAT certificate checking (2020)
  5. Alviano, Mario; Dodaro, Carmine; Fichte, Johannes K.; Hecher, Markus; Philipp, Tobias; Rath, Jakob: Inconsistency proofs for ASP: the ASP-DRUPE format (2019)
  6. Kiesl, Benjamin; Heule, Marijn J. H.; Biere, Armin: Truth assignments as conditional autarkies (2019)
  7. Marić, Filip: Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points (2019)
  8. Tonello, Elisa; Farcot, Etienne; Chaouiya, Claudine: Local negative circuits and cyclic attractors in Boolean networks with at most five components (2019)
  9. Huang, Pei; Ma, Feifei; Ge, Cunjing; Zhang, Jian; Zhang, Hantao: Investigating the existence of large sets of idempotent quasigroups via satisfiability testing (2018)
  10. Kiesl, Benjamin; Rebola-Pardo, Adrián; Heule, Marijn J. H.: Extended resolution simulates (\mathsfDRAT) (2018)
  11. Kiesl, Benjamin; Seidl, Martina; Tompits, Hans; Biere, Armin: Local redundancy in SAT: generalizations of blocked clauses (2018)
  12. Lonsing, Florian; Egly, Uwe: (\textsfQRAT^+): generalizing QRAT by a more powerful QBF redundancy property (2018)
  13. Slaney, John; Woltzenlogel Paleo, Bruno: Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (2018)
  14. Cheung, Kevin K. H.; Gleixner, Ambros; Steffy, Daniel E.: Verifying integer programming results (2017)
  15. Chihani, Zakaria; Miller, Dale; Renaud, Fabien: A semantic framework for proof evidence (2017)
  16. Cruz-Filipe, Luís; Heule, Marijn J. H.; Hunt Jr., Warren A.; Kaufmann, Matt; Schneider-Kamp, Peter: Efficient certified RAT verification (2017)
  17. Heule, Marijn; Hunt, Warren jun.; Kaufmann, Matt; Wetzler, Nathan: Efficient, verified checking of propositional proofs (2017)
  18. Heule, Marijn J. H.; Seidl, Martina; Biere, Armin: Solution validation and extraction for QBF preprocessing (2017)
  19. Kiesl, Benjamin; Heule, Marijn J. H.; Seidl, Martina: A little blocked literal goes a long way (2017)
  20. Lammich, Peter: The GRAT tool chain -- efficient (UN)SAT certificate checking with formal correctness guarantees (2017)

1 2 next