Adrian Rebola Pardo, Armin Biere,
"Two flavors of DRAT"
: Proc. 9th Work. on Pragmatics of SAT (POS'18), Serie EasyChair Preprint, Nummer 457, 8-2018
Original Titel:
Two flavors of DRAT
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 9th Work. on Pragmatics of SAT (POS'18)
Original Kurzfassung:
DRAT proofs have become the de facto standard for certifying SAT solvers? results. State-of-the-art DRAT checkers are able to e?ciently establish the unsatis?ability of a formula. However, DRAT checking requires unit propagation, and so it is computationally non-trivial. Due to design decisions in the development of early DRAT checkers, the class of proofs accepted by state-of-the-art DRAT checkers di?ers from the class of proofs accepted by the original de?nition. In this paper, we formalize the operational de?nition of DRAT proofs, and discuss practical implications of this di?erence for generating as well as checking DRAT proofs. We also show that these theoretical di?erences have the potential to a?ect whether some proofs generated in practice by SAT solvers are correct or not.