DRAT-based Bit-Vector Proofs in CVC4

DRAT-based Bit-Vector Proofs in CVC4” by Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, and Clark Barrett. In Proceedings of the 22^nd International Conference on Theory and Applications of Satisfiability Testing (SAT '19), (Mikolá\u{s} Janota and Inês Lynce, eds.), July 2019, pp. 298-305. Lisbon, Portugal.


Many state-of-the-art Satisfiability Modulo Theories (SMT) solvers for the theory of fixed-size bit-vectors employ an approach called bit-blasting, where a given formula is translated into a Boolean satisfiability (SAT) problem and delegated to a SAT solver. Consequently, producing bit-vector proofs in an SMT solver requires incorporating SAT proofs into its proof infrastructure. In this paper, we describe three approaches for integrating DRAT proofs generated by an off-the-shelf SAT solver into the proof infrastructure of the SMT solver CVC4 and explore their strengths and weaknesses. We implemented all three approaches using CryptoMiniSat as the SAT back-end for its bit-blasting engine and evaluated performance in terms of proof-production and proof-checking.

BibTeX entry:

   author = {Alex Ozdemir and Aina Niemetz and Mathias Preiner and Yoni
	Zohar and Clark Barrett},
   editor = {Mikol{\'a}\u{s} Janota and In{\^e}s Lynce},
   title = {{DRAT}-based Bit-Vector Proofs in {CVC4}},
   booktitle = {Proceedings of the {\it 22^{nd}} International Conference
	on Theory and Applications of Satisfiability Testing (SAT '19)},
   series = {Lecture Notes in Computer Science},
   volume = {11628},
   pages = {298--305},
   publisher = {Springer},
   month = jul,
   year = {2019},
   isbn = {978-3-030-24257-2},
   doi = {10.1007/978-3-030-24258-9_21},
   note = {Lisbon, Portugal},
   url = {http://theory.stanford.edu/~barrett/pubs/ONP+19.pdf}

(This webpage was created with bibtex2web.)