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.
This work is 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. We thank Andrew Goldberg, Stefano Pallottino and Romeo Rizzi for invaluable suggestions about the problems of solving linear (in)equalities.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
R. Alur. Timed Automata. In Proc. 11th International Computer Aided Verification Conference, pages 8–22, 1999.
A. Armando, C. Castellini, and E. Giunchiglia. SAT-based procedures for temporal reasoning. In Proc. European Conference on Planning, ECP-99, 1999.
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.
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.
Michel Berkelaar. The solver lpsolve for Linear Programming and Mixed-Integer Problems. Available at http://elib.zib.de/pub/Packages/mathprog/linprog/lp-solve/.
A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. CAV’99, 1999.
M. Buro and H. Buning. Report on a SAT competition. Technical Report 110, University of Paderborn, Germany, November 1992.
Boris V. Cherkassky and Andrew V. Goldberg. Negative-cycle detection algorithms. Mathematical Programming, 85(2):277–311, 1999.
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.
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.
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.
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.
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.
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.
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.
R. Sebastiani. Integrating SAT Solvers with Math Reasoners: Foundations and Basic Algorithms. Technical Report 0111-22, ITC-IRST, November 2001.
Ofer Shtrichmann. Tuning SAT Checkers for Bounded Model Checking. In Proc. CAV’2000, volume 1855 of LNCS. Springer, 2000.
K. Stergiou and M. Koubarakis. Backtracking algorithms for disjunctions of temporal constraints. In Proc. AAAI, pages 248–253, 1998.
S. Wolfman and D. Weld. The LPSAT Engine & its Application to Resource Planning. In Proc. IJCAI, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Audemard, G., Bertoli, P., Cimatti, A., Korniłowicz, A., Sebastiani, R. (2002). A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions. In: Voronkov, A. (eds) Automated Deduction—CADE-18. CADE 2002. Lecture Notes in Computer Science(), vol 2392. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45620-1_17
Download citation
DOI: https://doi.org/10.1007/3-540-45620-1_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43931-8
Online ISBN: 978-3-540-45620-9
eBook Packages: Springer Book Archive