“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.)