Advertisement

An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic

  • Marco Bozzano
  • Roberto Bruttomesso
  • Alessandro Cimatti
  • Tommi Junttila
  • Peter van Rossum
  • Stephan Schulz
  • Roberto Sebastiani
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3440)

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.

Keywords

Decision Procedure Conjunctive Normal Form Bound Model Check Linear Arithmetic Theory Solver 
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

  1. 1.
    Ackermann, W.: Solvable Cases of the Decision Problem. North Holland Pub. Co, Amsterdam (1954)zbMATHGoogle Scholar
  2. 2.
    Armando, A., Castellini, C., Giunchiglia, E.: SAT-based procedures for temporal reasoning. In: Proc. European Conference on Planning, CP 1999 (1999)Google Scholar
  3. 3.
    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)CrossRefGoogle Scholar
  4. 4.
    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)Google Scholar
  5. 5.
    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)CrossRefGoogle Scholar
  6. 6.
    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)Google Scholar
  7. 7.
    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)CrossRefGoogle Scholar
  8. 8.
    Badros, G.J., Borning, A.: The Cassowary linear arithmetic constraint solving algorithm: Interface and implementation. Technical Report UW-CSE-98-06-04 (Jun 1998)Google Scholar
  9. 9.
    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)Google Scholar
  10. 10.
    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)CrossRefGoogle Scholar
  11. 11.
    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)Google Scholar
  12. 12.
    Bockmayr, A., Weispfenning, V.: Solving Numerical Constraints. In: Handbook of Automated Reasoning, pp. 751–842. MIT Press, Cambridge (2001)CrossRefGoogle Scholar
  13. 13.
    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)CrossRefGoogle Scholar
  14. 14.
    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)Google Scholar
  15. 15.
    Brinkmann, R., Drechsler, R.: RTL-datapath verification using integer linear programming. In: Proc. ASP-DAC 2002, pp. 741–746. IEEE, Los Alamitos (2002)Google Scholar
  16. 16.
    Cherkassky, B.V., Goldberg, A.V.: Negative-cycle detection algorithms. Mathematical Programming 85(2), 277–311 (1999)zbMATHCrossRefMathSciNetGoogle Scholar
  17. 17.
  18. 18.
    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)Google Scholar
  19. 19.
    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)CrossRefGoogle Scholar
  20. 20.
    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)CrossRefGoogle Scholar
  21. 21.
    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)CrossRefGoogle Scholar
  22. 22.
    Gomes, C., Selman, B., Kautz, H.: Boosting Combinatorial Search Through Randomization. In: Proceedings of the Fifteenth National Conference on Artificial Intelligence (1998)Google Scholar
  23. 23.
    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)CrossRefGoogle Scholar
  24. 24.
  25. 25.
    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)CrossRefGoogle Scholar
  26. 26.
  27. 27.
    Moskewicz, M.W., Madigan, C.F., Zhang, Y.Z.L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Design Automation Conference (2001)Google Scholar
  28. 28.
    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)CrossRefGoogle Scholar
  29. 29.
  30. 30.
    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)Google Scholar
  31. 31.
  32. 32.
    Schulz, S.: E – A Brainiac Theorem Prover. AI Communications 15(2/3), 111–126 (2002)zbMATHGoogle Scholar
  33. 33.
    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)Google Scholar
  34. 34.
    Silva, J.P.M., Sakallah, K.A.: GRASP - A new Search Algorithm for Satisfiability. In: Proc. ICCAD 1996 (1996)Google Scholar
  35. 35.
  36. 36.
  37. 37.
    Wolfman, S., Weld, D.: The LPSAT Engine & its Application to Resource Planning. In: Proc. IJCAI (1999)Google Scholar
  38. 38.
    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)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Marco Bozzano
    • 1
  • Roberto Bruttomesso
    • 1
  • Alessandro Cimatti
    • 1
  • Tommi Junttila
    • 2
  • Peter van Rossum
    • 1
  • Stephan Schulz
    • 3
  • Roberto Sebastiani
    • 4
  1. 1.ITC-IRSTPovo, TrentoItaly
  2. 2.Helsinki University of TechnologyFinland
  3. 3.University of VeronaVeronaItaly
  4. 4.Università di TrentoPovo, TrentoItaly

Personalised recommendations