Anzeige
Erschienen in:
2014 | OriginalPaper | Buchkapitel
DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
verfasst von : Nathan Wetzler, Marijn J. H. Heule, Warren A. Hunt Jr.
Erschienen in: Theory and Applications of Satisfiability Testing – SAT 2014
Verlag: Springer International Publishing
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.