Abstract
In this paper we present a new decision procedure for the satisfiability of Linear Arithmetic Logic (LAL), i.e. boolean combinations of propositional variables and linear constraints over numerical variables. Our approach is based on the well known integration of a propositional SAT procedure with theory deciders, enhanced in the following ways.
First, our procedure relies on an incremental solver for linear arithmetic, that is able to exploit the fact that it is repeatedly called to analyze sequences of increasingly large sets of constraints. Reasoning in the theory of LA interacts with the boolean top level by means of a stack-based interface, that enables the top level to add constraints, set points of backtracking, and backjump, without restarting the procedure from scratch at every call. Sets of inconsistent constraints are found and used to drive backjumping and learning at the boolean level, and theory atoms that are consequences of the current partial assignment are inferred.
Second, the solver is layered: a satisfying assignment is constructed by reasoning at different levels of abstractions (logic of equality, real values, and integer solutions). Cheaper, more abstract solvers are called first, and unsatisfiability at higher levels is used to prune the search. In addition, theory reasoning is partitioned in different clusters, and tightly integrated with boolean reasoning.
We demonstrate the effectiveness of our approach by means of a thorough experimental evaluation: our approach is competitive with and often superior to several state-of-the-art decision procedures.
This work has been sponsored by the CALCULEMUS! IHP-RTN EC project, contract code HPRN-CT-2000-00102, and has thus benefited of the financial contribution of the Commission through the IHP programme. It has also been partly supported by ESACS, an European sponsored project, contract no. G4RD-CT-2000-00361, by ORCHID, a project sponsored by Provincia Autonoma di Trento, and by a grant from Intel Corporation. The work of T. Junttila has also been supported by the Academy of Finland, project 53695. S. Schulz has also been supported by a grant of the Italian Ministero dell’Istruzione, dell’Universit e della Ricerca and the University of Verona. R. Sebastiani is also sponsored by a MIUR COFIN02 project, code 2002097822_003.
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
Ackermann, W.: Solvable Cases of the Decision Problem. North Holland Pub. Co, Amsterdam (1954)
Armando, A., Castellini, C., Giunchiglia, E.: SAT-based procedures for temporal reasoning. In: Proc. European Conference on Planning, CP 1999 (1999)
Armando, A., Castellini, C., Giunchiglia, E., Maratea, M.: A SAT-based Decision Procedure for the Boolean Combination of Difference Constraints. In: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 16–29. Springer, Heidelberg (2005)
Audemard, G., Bertoli, P., Cimatti, A., Korniłowicz, 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, p. 195. Springer, Heidelberg (2002)
Audemard, G., Bertoli, P., Cimatti, A., Korniłowicz, A., Sebastiani, R.: Integrating boolean and mathematical solving: Foundations, basic algorithms and requirements. In: Calmet, J., Benhamou, B., Caprotti, O., Hénocque, L., Sorge, V. (eds.) AISC 2002 and Calculemus 2002. LNCS (LNAI), vol. 2385, pp. 231–245. Springer, Heidelberg (2002)
Audemard, G., Bozzano, M., Cimatti, A., Sebastiani, R.: Verifying Industrial Hybrid Systems with MathSAT. In: Proc. of the 1st CADE-19 Workshop on Pragmatics of Decision Procedures in Automated Reasoning, PDPAR 2003 (2003)
Audemard, G., Cimatti, A., Korniłowicz, A., Sebastiani, R.: SAT-Based Bounded Model Checking for Timed Systems. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, Springer, Heidelberg (2002)
Badros, G.J., Borning, A.: The Cassowary linear arithmetic constraint solving algorithm: Interface and implementation. Technical Report UW-CSE-98-06-04 (Jun 1998)
Ball, T., Cook, B., Lahiri, S.K., Zhang, L.: Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement. In: Proc. CAV 2004, pp. 457–461. Springer, Heidelberg (2004)
Barrett, C., Berezin, S.: CVC Lite: A New Implementation of the Cooperating Validity Checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 515–518. Springer, Heidelberg (2004)
Bayardo Jr., R.J., Schrag, R.C.: Using CSP Look-Back Techniques to Solve Real-World SAT instances. In: Proc. AAAI/IAAI 1997, pp. 203–208. AAAI Press, Menlo Park (1997)
Bockmayr, A., Weispfenning, V.: Solving Numerical Constraints. In: Handbook of Automated Reasoning, pp. 751–842. MIT Press, Cambridge (2001)
Borning, A., Marriott, K., Stuckey, P., Xiao, Y.: Solving linear arithmetic constraints for user interface applications. In: Proc. UIST 1997, pp. 87–96. ACM, New York (1997)
Bozzano, M., Cimatti, A., Colombini, G., Kirov, V., Sebastiani, R.: The MathSat solver – a progress report. In: Proc. Workhop on Pragmatics of Decision Procedures in Automated Reasoning 2004, PDPAR 2004 (2004)
Brinkmann, R., Drechsler, R.: RTL-datapath verification using integer linear programming. In: Proc. ASP-DAC 2002, pp. 741–746. IEEE, Los Alamitos (2002)
Cherkassky, B.V., Goldberg, A.V.: Negative-cycle detection algorithms. Mathematical Programming 85(2), 277–311 (1999)
CVC, CVCLite and SVC, http://verify.stanford.edu/CVC,CVCL,SVC
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Filliâtre, J.-C., Owre, S., Ruess, H., Shankar, N.: ICS: Integrated Canonizer and Solver. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 246–249. Springer, Heidelberg (2001)
Flanagan, C., Joshi, R., Ou, X., Saxe, J.B.: Theorem Proving using Lazy Proof Explication. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 355–367. Springer, Heidelberg (2003)
Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175–188. Springer, Heidelberg (2004)
Gomes, C., Selman, B., Kautz, H.: Boosting Combinatorial Search Through Randomization. In: Proceedings of the Fifteenth National Conference on Artificial Intelligence (1998)
Horrocks, I., Patel-Schneider, P.F.: FaCT and DLP. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol. 1397, pp. 27–30. Springer, Heidelberg (1998)
Kroening, D., Ouaknine, J., Seshia, S., Strichman, O.: Abstraction-Based Satisfiability Solving of Presburger Arithmetic. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 308–320. Springer, Heidelberg (2004)
mathsat, http://mathsat.itc.it
Moskewicz, M.W., Madigan, C.F., Zhang, Y.Z.L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Design Automation Conference (2001)
Nieuwenhuis, R., Oliveras, A.: Congruence Closure with Integer Offsets. In: Y. Vardi, M., Voronkov, A. (eds.) LPAR 2003. LNCS (LNAI), vol. 2850, pp. 77–89. Springer, Heidelberg (2003)
Parthasarathy, G., Iyer, M.K., Cheng, K.-T.: An efficient finite-domain constraint solver for circuits. In: Proc. DAC 2004, pp. 212–217. IEEE, Los Alamitos (2004)
SAL Suite. http://www.csl.sri.com/users/demoura/gdp-benchmarks.html
Schulz, S.: E – A Brainiac Theorem Prover. AI Communications 15(2/3), 111–126 (2002)
Seshia, S.A., Lahiri, S.K., Bryant, R.E.: A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. In: Proc. DAC 2003, pp. 425–430. ACM, New York (2003)
Silva, J.P.M., Sakallah, K.A.: GRASP - A new Search Algorithm for Satisfiability. In: Proc. ICCAD 1996 (1996)
Wolfman, S., Weld, D.: The LPSAT Engine & its Application to Resource Planning. In: Proc. IJCAI (1999)
Zhang, L., Malik, S.: The quest for efficient boolean satisfiability solvers. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 17–36. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bozzano, M. et al. (2005). An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic. In: Halbwachs, N., Zuck, L.D. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2005. Lecture Notes in Computer Science, vol 3440. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31980-1_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-31980-1_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25333-4
Online ISBN: 978-3-540-31980-1
eBook Packages: Computer ScienceComputer Science (R0)