Integrating Boolean and Mathematical Solving: Foundations, Basic Algorithms, and Requirements

  • 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 2385)


In the last years we have witnessed an impressive advance in the efficiency of boolean solving techniques, which has brought large previously intractable problems at the reach of state-of-the-art solvers. Unfortunately, simple boolean expressions are not expressive enough for representing many real-world problems, which require handling also integer or real values and operators. On the other hand, mathematical solvers, like computer-algebra systems or constraint solvers, cannot handle efficiently problems involving heavy boolean search, or do not handle them at all. In this paper we present the foundations and the basic algorithms for a new class of procedures for solving boolean combinations of mathematical propositions, which combine boolean and mathematical solvers, and we highlight the main requirements that boolean and mathematical solvers must fulfill in order to achieve the maximum benefits from their integration. Finally we show how existing systems are captured by our framework.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [ABC+02]_G. Audemard, P. Bertoli, A. Cimatti, A. Korniłowicz, and R. Sebastiani. A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions. In Proc. CADE’2002., 2002. To appear. Available at
  2. [ACG99]
    A. Armando, C. Castellini, and E. Giunchiglia. SAT-based procedures for temporal reasoning. In Proc. European Conference on Planning, CP-99, 1999.Google Scholar
  3. [ACKS02]
    G. Audemard, A. Cimatti, A. Korniłowicz, and R. Sebastiani. SAT-Based Bounded Model Checking for Timed Systems. 2002. Available at
  4. [BCCZ99]
    A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. CAV’99, 1999.Google Scholar
  5. [Bry86]
    R. E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, C-35(8):677–691, August 1986.Google Scholar
  6. [CABN97]
    W. Chan, R. J. Anderson, P. Beame, and D. Notkin. Combining constraint solving and symbolic model checking for a class of systems with non-linear constraints. In Proc. CAV’97, volume 1254 of LNCS, pages 316–327, Haifa, Israel, June 1997. Springer-Verlag.Google Scholar
  7. [DLL62]
    M. Davis, G. Longemann, and D. Loveland. A machine program for theorem proving. Journal of the ACM, 5(7), 1962.Google Scholar
  8. [GS96]
    F. Giunchiglia and R. Sebastiani. Building decision procedures for modal logics from propositional decision procedures-the case study of modal K. In Proc. of the 13th Conference on Automated Deduction, LNAI, New Brunswick, NJ, USA, August 1996. Springer Verlag.Google Scholar
  9. [GS00]
    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
  10. [HPS98]
    I. Horrocks and P. F. Patel-Schneider. FaCT and DLP. In Procs. Tableaux’98, number 1397 in LNAI, pages 27–30. Springer-Verlag, 1998.Google Scholar
  11. [KMS96]
    H. Kautz, D. McAllester, and Bart Selman. Encoding Plans in Propositional Logic. In Proc. KR’96, 1996.Google Scholar
  12. [MLAH01]
    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
  13. [Pug92]
    W. Pugh. The Omega Test: a fast and practical integer programming algoprithm for dependence analysis. Communication of the ACM, August 1992.Google Scholar
  14. [RV01]
    A. Robinson and A. Voronkov, editors. Handbook of Automated Reasoning. Elsevier Science Publishers, 2001.Google Scholar
  15. [Seb01]
    R. Sebastiani. Integrating SAT Solvers with Math Reasoners: Foundations and Basic Algorithms. Technical Report 0111-22, ITC-IRST, November 2001. Available at
  16. [Smu68]
    R. M. Smullyan. First-Order Logic. Springer-Verlag, NY, 1968.zbMATHGoogle Scholar
  17. [WW99]
    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