“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:
@inproceedings{ONP+19,
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.)