Abstract
In the past few years, general-purpose propositional satisfiability (SAT) solvers have improved dramatically in performance and have been used to tackle many new problems. It has also been shown that certain simple fragments of first-order logic can be decided efficiently by first translating the problem into an equivalent SAT problem and then using a fast SAT solver. In this paper, we describe an alternative but similar approach to using SAT in conjunction with a more expressive fragment of first-order logic. However, rather than translating the entire formula up front, the formula is incrementally translated during a search for the solution. As a result, only that portion of the translation that is actually relevant to the solution is obtained. We describe a number of obstacles that had to be overcome before developing an approach which was ultimately very effective, and give results on verification benchmarks using CVC (Cooperating Validity Checker), which includes the Chaff SAT solver. The results show a performance gain of several orders of magnitude over CVC without Chaff and indicate that the method is more robust than the heuristics found in CVC’s predecessor, SVC.
Chapter PDF
Similar content being viewed by others
References
C. Barrett, D. Dill, and J. Levitt. Validity Checking for Combinations of Theories with Equality. In Mandayam Srivas and Albert Camilleri, editors, Formal Methods In Computer-Aided Design, pages 187–201, 1996.
Clark W. Barrett. Checking Validity of Quantifier-Free Formulas in Combinations of First-Order Theories. PhD thesis, Stanford University, 2002.
R. Bryant, S. German, and M. Velev. Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions. In 11th International Conference on Computer-Aided Verification, pages 470–482, 1999.
Leonardo de Moura, Harald Ruess, and Maria Sorea. Lazy Theorem Proving for Bounded Model Checking over Infinite Domains. In 18th International Conference on Automated Deduction, 2002.
L. e Silva, L. Silveira, and J. Marques-Silva. Algorithms for Solving Boolean Satisfiability in Combinational Circuits. In Proceedings of the IEEE/ACM Design, Automation and Test in Europe Conference (DATE), March 1999.
C. Flanagan. Private Communication, 2000.
Cormac Flanagan, Rajeev Joshi, and James B. Saxe. The Design of An Efficient Theorem Prover using Explicated Clauses. 2002. In Preparation.
Tracy Larrabee. Test pattern generation using Boolean satisfiability. IEEE Transactions on Computer-Aided Design, 11(1):4–15, January 1992.
Jeremy R. Levitt. Formal Verification Techniques for Digital Systems. PhD thesis, Stanford University, 1999.
M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an Efficient SAT Solver. In Proceedings of the 39th Design Automation Conference, 2001.
G. Nelson and D. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):245–57, 1979.
A. Pnueli, Y. Rodeh, O. Shtrichman, and M. Siegel. Deciding Equality Formulas by Small-Domain Instantiations. In 11th International Conference on Computer-Aided Verification, pages 455–469, 1999.
H. Ruess and N. Shankar. Deconstructing Shostak. In 16th Annual IEEE Symposium on Logic in Computer Science, pages 19–28, June 2001.
Laurent Simon. The Sat-Ex Site. http://www.lri.fr/~simon/satex/satex.php3.
A. Stump, C. Barrett, and D. Dill. CVC: a Cooperating Validity Checker. In 14th International Conference on Computer-Aided Verification, 2002.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Barrett, C.W., Dill, D.L., Stump, A. (2002). Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. In: Brinksma, E., Larsen, K.G. (eds) Computer Aided Verification. CAV 2002. Lecture Notes in Computer Science, vol 2404. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45657-0_18
Download citation
DOI: https://doi.org/10.1007/3-540-45657-0_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43997-4
Online ISBN: 978-3-540-45657-5
eBook Packages: Springer Book Archive