A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions
- 338 Downloads
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.
KeywordsModel Check Decision Procedure Truth Assignment Temporal Reasoning Symbolic Model Check
Unable to display preview. Download preview PDF.
- 1.R. Alur. Timed Automata. In Proc. 11th International Computer Aided Verification Conference, pages 8–22, 1999.Google Scholar
- 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.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.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.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.A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. CAV’99, 1999.Google Scholar
- 7.M. Buro and H. Buning. Report on a SAT competition. Technical Report 110, University of Paderborn, Germany, November 1992.Google Scholar
- 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.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.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.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.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.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.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.R. Sebastiani. Integrating SAT Solvers with Math Reasoners: Foundations and Basic Algorithms. Technical Report 0111-22, ITC-IRST, November 2001.Google Scholar
- 17.Ofer Shtrichmann. Tuning SAT Checkers for Bounded Model Checking. In Proc. CAV’2000, volume 1855 of LNCS. Springer, 2000.Google Scholar
- 18.K. Stergiou and M. Koubarakis. Backtracking algorithms for disjunctions of temporal constraints. In Proc. AAAI, pages 248–253, 1998.Google Scholar
- 19.S. Wolfman and D. Weld. The LPSAT Engine & its Application to Resource Planning. In Proc. IJCAI, 1999.Google Scholar