Advertisement

A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions

  • Gilles Audemard
  • Piergiorgio Bertoli
  • Alessandro Cimatti
  • Artur Korniłowicz
  • Roberto Sebastiani
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2392)

Abstract

The availability of decision procedures for combinations of boolean and linear mathematical propositions opens the ability to solve problems arising from real-world domains such as verification of timed systems and planning with resources. In this paper we present a general and efficient approach to the problem, based on two main ingredients. The first is a DPLL-based SAT procedure, for dealing efficiently with the propositional component of the problem. The second is a tight integration, within the DPLL architecture, of a set of mathematical deciders for theories of increasing expressive power. A preliminary experimental evaluation shows the potential of the approach.

Keywords

Model Check Decision Procedure Truth Assignment Temporal Reasoning Symbolic Model Check 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    R. Alur. Timed Automata. In Proc. 11th International Computer Aided Verification Conference, pages 8–22, 1999.Google Scholar
  2. 2.
    A. Armando, C. Castellini, and E. Giunchiglia. SAT-based procedures for temporal reasoning. In Proc. European Conference on Planning, ECP-99, 1999.Google Scholar
  3. 3.
    G. Audemard, A. Cimatti, A. Korni!lowicz, and R. Sebastiani. Bounded Model Checking for Timed Systems. Technical Report 0201-05, ITC-IRST, Trento, Italy, January 2002. Submitted for publication.Google Scholar
  4. 4.
    R. J. Bayardo, Jr. and R. C. Schrag. Using CSP Look-Back Techniques to Solve Real-World SAT instances. In Proc AAAI’97, pages 203–208. AAAI Press, 1997.Google Scholar
  5. 5.
    Michel Berkelaar. The solver lpsolve for Linear Programming and Mixed-Integer Problems. Available at http://elib.zib.de/pub/Packages/mathprog/linprog/lp-solve/.
  6. 6.
    A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. CAV’99, 1999.Google Scholar
  7. 7.
    M. Buro and H. Buning. Report on a SAT competition. Technical Report 110, University of Paderborn, Germany, November 1992.Google Scholar
  8. 8.
    Boris V. Cherkassky and Andrew V. Goldberg. Negative-cycle detection algorithms. Mathematical Programming, 85(2):277–311, 1999.zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    A. Cimatti, M. Pistore, M. Roveri, and R. Sebastiani. Improving the Encoding of LTL Model Checking into SAT. In Proc. 3rd International Workshop on Verification, Model Checking, and Abstract Interpretation, volume 2294 of LNCS Springer, 2002.Google Scholar
  10. 10.
    E. Giunchiglia, A. Massarotto, and R. Sebastiani. Act, and the Rest Will Follow: Exploiting Determinism in Planning as Satisfiability. In Proc. AAAI’98, pages 948–953, 1998.Google Scholar
  11. 11.
    E. Giunchiglia, M. Narizzano, A. Tacchella, and M. Vardi. Towards an Efficient Library for SAT: a Manifesto. In Proc. SAT 2001, Electronics Notes in Discrete Mathematics. Elsevier Science., 2001.Google Scholar
  12. 12.
    F. Giunchiglia and R. Sebastiani. Building decision procedures for modal logics from propositional decision procedures-the case study of modal K. In Proc. CADE13, LNAI. Springer Verlag, August 1996.Google Scholar
  13. 13.
    F. Giunchiglia and R. Sebastiani. Building decision procedures for modal logics from propositional decision procedures-the case study of modal K(m). Information and Computation, 162(1/2), October/November 2000.Google Scholar
  14. 14.
    I. Horrocks and P. F. Patel-Schneider. FaCT and DLP. In Proc. of Tableaux’98, number 1397 in LNAI, pages 27–30. Springer-Verlag, 1998.Google Scholar
  15. 15.
    J. Moeller, J. Lichtenberg, H. Andersen, and H. Hulgaard. Fully Symbolic Model Checking of Timed Systems using Difference Decision Diagrams. In Electronic Notes in Theoretical Computer Science, volume 23. Elsevier Science, 2001.Google Scholar
  16. 16.
    R. Sebastiani. Integrating SAT Solvers with Math Reasoners: Foundations and Basic Algorithms. Technical Report 0111-22, ITC-IRST, November 2001.Google Scholar
  17. 17.
    Ofer Shtrichmann. Tuning SAT Checkers for Bounded Model Checking. In Proc. CAV’2000, volume 1855 of LNCS. Springer, 2000.Google Scholar
  18. 18.
    K. Stergiou and M. Koubarakis. Backtracking algorithms for disjunctions of temporal constraints. In Proc. AAAI, pages 248–253, 1998.Google Scholar
  19. 19.
    S. Wolfman and D. Weld. The LPSAT Engine & its Application to Resource Planning. In Proc. IJCAI, 1999.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Gilles Audemard
    • 1
    • 2
  • Piergiorgio Bertoli
    • 1
  • Alessandro Cimatti
    • 1
  • Artur Korniłowicz
    • 1
    • 3
  • Roberto Sebastiani
    • 1
    • 4
  1. 1.ITC-IRSTPovo, TrentoItaly
  2. 2.LSISUniversity of ProvenceMarseilleFrance
  3. 3.Institute of Computer ScienceUniversity of BiałystokPoland
  4. 4.DITUniversità di TrentoPovo, TrentoItaly

Personalised recommendations