Abstract
The logic of equality with uninterpreted functions (EUF) and its extensions have been widely applied to processor verification, by means of a large variety of progressively more sophisticated (lazy or eager) translations into propositional SAT. Here we propose a new approach, namely a general DPLL(X) engine, whose parameter X can be instantiated with a specialized solver Solver T for a given theory T, thus producing a system DPLL(T). We describe this DPLL(T) scheme, the interface between DPLL(X) and Solver T , the architecture of DPLL(X), and our solver for EUF, which includes incremental and backtrackable congruence closure algorithms for dealing with the built-in equality and the integer successor and predecessor symbols. Experiments with a first implementation indicate that our technique already outperforms the previous methods on most benchmarks, and scales up very well.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Audemard, G., Bertoli, P., Cimatti, A., Kornilowicz, A., Sebastiani, R.: A SAT based approach for solving formulas over boolean and linear mathematical propositions. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 195–210. Springer, Heidelberg (2002)
Armando, A., Castellini, C., Giunchiglia, E.: SAT-based procedures for temporal reasoning. In: Biundo, S., Fox, M. (eds.) ECP 1999. LNCS, vol. 1809, pp. 97–108. Springer, Heidelberg (2000)
Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 68–80. Springer, Heidelberg (1994)
Barrett, C., Dill, D.L., Levitt, J.: Validity checking for combinations of theories with equality. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 187–201. Springer, Heidelberg (1996)
Barrett, C., Dill, D., Stump, A.: Checking satisfiability of first-order formulas by incremental translation into sat. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 236. Springer, Heidelberg (2002)
Bryant, R.E., German, S., Velev, M.N.: Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic. ACM Trans. Computational Logic 2(1), 93–134 (2001)
Bryant, R.E., Lahiri, S., Seshia, S.: Deciding CLU logic formulas via boolean and pseudo-boolean en codings. In: Procs. 1st Int. Workshop on Constraints in Formal Verification (2002)
Bryant, R.E., Lahiri, S., Seshia, S.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 78. Springer, Heidelberg (2002)
Bachmair, L., Tiwari, A.: Abstract congruence closure and specializations. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 64–78. Springer, Heidelberg (2000)
Bryant, R.E., Velev, M.N.: Boolean satisfiability with transitivity constraints. ACM Trans. Computational Logic 3(4), 604–627 (2002)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. CACM 5(7), 394–397 (1962)
de Moura, L., Rueß, H.: Lemmas on demand for satisfiability solvers. In: Procs. 5th Int. Symp. on the Theory and Applications of Satisfiability Testing, SAT 2002, pp. 244–251 (2002)
Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM 7, 201–215 (1960)
Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpressions problem. J. ACM 27(4), 758–771 (1980)
Flanagan, C., Joshi, R., Ou, X., Saxe, J.B.: Theorem proving using lazy proof explanation. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 355–367. Springer, Heidelberg (2003)
Goldberg, E., Novikov, Y.: BerkMin: A fast and robust SAT-solver. In: Design, Automation, and Test in Europe (DATE 2002), pp. 142–149 (2002)
Kapur, D.: Shostak’s congruence closure as completion. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, Springer, Heidelberg (1997)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proc. 38th Design Automation Conference, DAC 2001 (2001)
Nelson, G., Oppen, D.C.: Fast decision procedures bases on congruence closure. J. ACM 27(2), 356–364 (1980)
Nieuwenhuis, R., Oliveras, A.: Congruence closure with integer offsets. In: Y. Vardi, M., Voronkov, A. (eds.) LPAR 2003. LNCS, vol. 2850, pp. 78–90. Springer, Heidelberg (2003)
Pnueli, A., Rodeh, Y., Shtrichman, O., Siegel, M.D.: Deciding equality formulas by small domains instantiations. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 455–469. Springer, Heidelberg (1999)
Seshia, S., Lahiri, S., Bryant, R.: A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. In: Procs. 40th Design Automation Conference (DAC), pp. 425–430 (2003)
Strichman, O., Seshia, S.A., Bryant, R.E.: Deciding separation formulas with SAT. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 209–222. Springer, Heidelberg (2002)
Tinelli, C.: A DPLL-based calculus for ground satisfiability modulo theories. In: Flesca, S., Greco, S., Leone, N., Ianni, G. (eds.) JELIA 2002. LNCS (LNAI), vol. 2424, pp. 308–319. Springer, Heidelberg (2002)
Tiwari, A., Vigneron, L.: Implementation of Abstract Congruence Closure (2001), At http://www.csl.sri.com/users/tiwari
Velev, M.N., Bryant, R.E.: Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. Journal of Symbolic Computation 35(2), 73–106 (2003)
Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient conflict driven learning in a Boolean satisfiability solver. In: Int. Conf. on Computer-Aided Design (ICCAD 2001), pp. 279–285 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C. (2004). DPLL(T): Fast Decision Procedures. In: Alur, R., Peled, D.A. (eds) Computer Aided Verification. CAV 2004. Lecture Notes in Computer Science, vol 3114. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27813-9_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-27813-9_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22342-9
Online ISBN: 978-3-540-27813-9
eBook Packages: Springer Book Archive