Don’t care in SMT: building flexible yet efficient abstraction/refinement solvers
Tóm tắt
This paper describes a method for combining “off-the-shelf” SAT and constraint solvers for building an efficient Satisfiability Modulo Theories (SMT) solver for a wide range of theories. Our method follows the abstraction/refinement approach to simplify the implementation of custom SMT solvers. The expected performance penalty by not using an interweaved combination of SAT and theory solvers is reduced by generalising a Boolean solution of an SMT problem first via assigning don’t care to as many variables as possible. We then use the generalised solution to determine a thereby smaller constraint set to be handed over to the constraint solver for a background theory. We show that for many benchmarks and real-world problems, this optimisation results in considerably smaller and less complex constraint problems. The presented approach is particularly useful for assembling a practically viable SMT solver quickly, when neither a suitable SMT solver nor a corresponding incremental theory solver is available. We have implemented our approach in the ABsolver framework and applied the resulting solver successfully to an industrial case-study: the verification problems arising in verifying an electronic car steering control system impose non-linear arithmetic constraints, which do not fall into the domain of any other available solver.
Tài liệu tham khảo
Ball, T., Lahiri, S.K., Musuvathi, M.: Zap: Automated theorem proving for software analysis. In: Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), pp 2–22 (2005)
Barrett, C., Berezin, S.: CVC Lite: A new implementation of the cooperating validity checker. In: Computer Aided Verification (CAV), pp 515–518 (2004)
Bauer, A.: Simplifying diagnosis using LSAT: a propositional approach to reasoning from first principles. In: Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems (CP-AI-OR), pp 49–63 (2005)
Bauer, A., Leucker, M., Schallhart, C., Tautschnig, M.: Don’t care in SMT—building flexible yet efficient abstraction/refinement solvers. In: Proceedings of the 2007 ISoLA Workshop On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA’07), France, RNTI, Revue des Nouvelles Technologies de l’Information (2007a)
Bauer, A., Pister, M., Tautschnig, M.: Tool-support for the analysis of hybrid systems and models. In: Design, Automation and Test in Europe (DATE), pp 924–929 (2007b)
Belov, A., Stachniak, Z.: Substitutional definition of satisfiability in classical propositional logic. In: Theory and Applications of Satisfiability Testing (SAT), pp 31–45 (2005)
Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Schulz, S., Sebastiani, R.: An incremental and layered procedure for the satisfiability of linear arithmetic logic. In: Tools and Algorithms for Construction and Analysis of Systems (TACAS), pp 317–333 (2005)
Delgrande J.P., Gupta A.: The complexity of minimum partial truth assignments and implication in negation-free formulae. Ann. Math. Artif. Intell. 18(1), 51–67 (1996)
DIMACS: Satisfiability: Suggested format. Tech. rep. (1993)
Dutertre, B., de Moura, L.M.: A fast linear-arithmetic solver for DPLL(T). In: Computer Aided Verification (CAV), pp 81–94 (2006)
Een, N., Sörensson, N.: An extensible sat-solver. In: Theory and Application of Satisfiability Testing (SAT), pp 502–518 (2003)
Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast decision procedures. In: Computer Aided Verification (CAV), pp 175–188 (2004)
Halbwachs N., Caspi P., Raymond P., Pilaud D.: The synchronous dataflow programming language. Lustre 79(9), 1305–1320 (1991)
Jones, R.B., Dill, D.L.: Automatic verification of pipelined microprocessors control. In: Computer Aided Verification (CAV), pp 68–80 (1994)
Kirousis L.M., Kolaitis P.G.: The complexity of minimal satisfiability problems. Inf. Comput. 187(1), 20–39 (2003)
Lahiri, S.K., Nieuwenhuis, R., Oliveras, A.: SMT techniques for fast predicate abstraction. In: Computer Aided Verification (CAV), pp 424–437 (2006)
Lougee-Heimer R.: The common optimization interface for operations research: promoting open-source software in the operations research community. IBM. J. Res. Dev. 47(1), 57–66 (2003)
Lynce, I., Ouaknine, J.: Sudoku as a SAT problem. In: Proceedings of the Ninth International Symposium on Artificial Intelligence and Mathematics (2006)
Marques-Silva, J.P., Sakallah, K.A.: GRASP—a new search algorithm for satisfiability. In: International Conference on Computer-Aided Design (ICCAD), pp 220–227 (1996)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Design Automation Conference (DAC), pp 530–535 (2001)
Prasad M.R., Biere A., Gupta A.: A survey of recent advances in sat-based formal verification. Softw. Tools Technol. Transf. 7(2), 156–173 (2005)
Ranise, S., Tinelli, C.: The SMT-LIB Standard: Version 1.2. Techical report, Department of Computer Science, University of Iowa, http://www.SMT-LIB.org (2006)
Rodeh Y., Strichman O.: Building small equality graphs for deciding equailty logic with uninterpreted functions. Inf. Comput. 204(1), 26–59 (2006)
Roorda, J.W., Claessen, K.: SAT-based assistance in abstraction refinement for symbolic trajectory evaluation. In: Computer Aided Verification (CAV), pp 175–189 (2006)
Rushby, J: Harnessing disruptive innovation in formal verification. In: Softw. Eng. Formal Methods, pp 21–30 (2006a)
Rushby, J.: Tutorial: automated formal methods with PVS, SAL, and Yices. In: Software Engineering and Formal Methods (SEFM), p 262 (2006b)
Sheini, H., Sakallah, K.: From propositional satisfiability to satisfiability modulo theories. In: Theory and Applications of Satisfiability Testing (SAT), pp 1–9 (2006)
Sheini, H.M., Sakallah, K.A.: A scalable method for solving satisfiability of integer linear arithmetic logic. In: Theory and Application of Satisfiability Testing (SAT), pp 241–256 (2005)
Shostak R.: Deciding linear inequalities by computing loop residues. J. ACM 28(4), 769–779 (1981)
Wächter A., Biegler L.T.: Line search filter methods for nonlinear programming: motivation and global convergence. SIAM J. Optim. 16(1), 1–31 (2005)
Weber, T.: A SAT-based Sudoku solver. In: Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), Short Paper Proceedings, pp 11–15 (2005)
Zantema, H., Groote, J.F.: Transforming equality logic to propositional logic. Electr. Notes. Theor. Comput. Sci. 86(1) (2003)