DRAT-trim: efficient checking and trimming using expressive clausal proofs. (English) Zbl 1423.68475

Wetzler, Nathan; Heule, Marijn J. H.; Hunt, Warren A. jun.

Sinz, Carsten (ed.) et al., Theory and applications of satisfiability testing – SAT 2014. 17th international conference, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14–17, 2014. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8561, 422-429 (2014).

Summary: 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.
For the entire collection see [Zbl 1293.68033].

MSC:

68T20	Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68T15	Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

DRAT-trim; Plingeling; Treengeling