Continuous First-Order Constraint Satisfaction

  • Stefan Ratschan
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2385)


This paper shows how to use constraint programming techniques for solving first-order constraints over the reals (i.e., formulas in the first-order predicate language over the structure of the real numbers). More specifically, based on a narrowing operator that implements an arbitrary notion of consistency for atomic constraints over the reals (e.g., box-consistency), the paper provides a narrowing operator for first-order constraints that implements a corresponding notion of first-order consistency, and a solver based on such a narrowing operator. As a consequence, this solver can take over various favorable properties from the field of constraint programming.


Constraint Programming Reasoning 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    S. Basu, R. Pollack, and M.-F. Roy. On the combinatorial and algebraic complexity of quantifier elimination. In S. Goldwasser, editor, Proceedings fo the 35th Annual Symposium on Foundations of Computer Science, pages 632–641, Los Alamitos, CA, USA, 1994. IEEE Computer Society Press.Google Scholar
  2. 2.
    F. Benhamou. Interval constraint logic programming. InPodelski [21].Google Scholar
  3. 3.
    F. Benhamou and F. Goualard. Universally quantified interval constraints. In Proc. of the Sixth Intl. Conf. on Principles and Practice of Constraint Programming (CP’2000), number 1894 in LNCS, Singapore, 2000. Springer Verlag.Google Scholar
  4. 4.
    F. Benhamou, F. Goualard, L. Granvilliers, and J. F. Puget. Revising hull and box consistency. In Int. Conf. on Logic Programming, pages 230–244, 1999.Google Scholar
  5. 5.
    F. Benhamou, D. McAllester, and P. V. Hentenryck. CLP (Intervals) Revisited. In International Symposium on Logic Programming, pages 124–138, Ithaca, NY, USA, 1994. MIT Press.Google Scholar
  6. 6.
    F. Benhamou and W. J. Older. Applying interval arithmetic to real, integer and Boolean constraints. Journal of Logic Programming, 32(1):1–24, 1997.zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    B. F. Caviness and J. R. Johnson, editors. Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer, 1998.Google Scholar
  8. 8.
    G. E. Collins. Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition. In Second GI Conf. Automata Theory and Formal Languages, volume 33 of LNCS, pages 134–183. Springer Verlag, 1975. Also in [7].Google Scholar
  9. 9.
    G. E. Collins and H. Hong. Partial cylindrical algebraic decomposition for quantifier elimination. Journal of Symbolic Computation, 12:299–328, 1991. Also in [7].zbMATHMathSciNetCrossRefGoogle Scholar
  10. 10.
    J. H. Davenport and J. Heintz. Real quantifier elimination is doubly exponential. Journal of Symbolic Computation, 5:29–35, 1988.zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    L. Granvilliers. A symbolic-numerical branch and prune algorithm for solving nonlinear polynomial systems. Journal of Universal Computer Science, 4(2):125–146, 1998.zbMATHMathSciNetGoogle Scholar
  12. 12.
    P. V. Hentenryck, D. McAllester, and D. Kapur. Solving polynomial systems using a branch and prune approach. SI0AM Journal on Numerical Analysis, 34(2), 1997.Google Scholar
  13. 13.
    P. V. Hentenryck, V. Saraswat, and Y. Deville. The design, implementation, and evaluation of the constraint language cc(FD). In Podelski [21].Google Scholar
  14. 14.
    H. Hong and V. Stahl. Safe starting regions by fixed points and tightening. Computing, 53:323–335, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    L. Jaulin and É. Walter. Guaranteed tuning, with application to robust control and motion planning. Automatica, 32(8):1217–1221, 1996.zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    J. Jourdan and T. Sola. The versatility of handling disjunctions as constraints. In M. Bruynooghe and J. Penjam, editors, Proc. of the 5th Intl. Symp. on Programming Language Implementation and Logic Programming, PLILP’93, number 714 in LNCS, pages 60–74. Springer Verlag, 1993.Google Scholar
  17. 17.
    A. Macintyre and A. Wilkie. On the decidability of the real exponential field. In P. Odifreddi, editor, Kreiseliana—About and Around Georg Kreisel, pages 441–467. A K Peters, 1996.Google Scholar
  18. 18.
    S. Malan, M. Milanese, and M. Taragna. Robust analysis and design of control systems using interval arithmetic. Automatica, 33(7):1363–1372, 1997.zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    K. Marriott, P. Moulder, P. J. Stuckey, and A. Borning. Solving disjunctive constraints for interactive graphical applications. In Seventh Intl. Conf. on Principles and Practice of Constraint Programming-CP2001, number 2239 in LNCS, pages 361–376. Springer, 2001.CrossRefGoogle Scholar
  20. 20.
    A. Neumaier. Interval Methods for Systems of Equations. Cambridge Univ. Press, Cambridge, 1990.zbMATHGoogle Scholar
  21. 21.
    A. Podelski, editor. Constraint Programming: Basics and Trends, volume 910 of LNCS. Springer Verlag, 1995.zbMATHGoogle Scholar
  22. 22.
    S. Ratschan. Approximate quantified constraint solving (AQCS)., 2000. Software package.
  23. 23.
    S. Ratschan. Applications of real first-order constraint solving —bibliography., 2001.
  24. 24.
    S. Ratschan. Real first-order constraints are stable with probability one., 2001. Draft.
  25. 25.
    S. Ratschan. Approximate quantified constraint solving by cylindrical box decomposition. Reliable Computing, 8(1):21–42, 2002.zbMATHCrossRefMathSciNetGoogle Scholar
  26. 26.
    S. Ratschan. Quantified constraints under perturbations. Journal of Symbolic Computation, 33(4):493–505, 2002.zbMATHCrossRefMathSciNetGoogle Scholar
  27. 27.
    J. Renegar. On the computational complexity and geometry of the first-order theory of the reals. Journal of Symbolic Computation, 13(3):255–352, March 1992.Google Scholar
  28. 28.
    D. Richardson. Some undecidable problems involving elementary functions of a real variable. Journal of Symbolic Logic, 33:514–520, 1968.zbMATHCrossRefMathSciNetGoogle Scholar
  29. 29.
    D. Sam-Haroud and B. Faltings. Consistency techniques for continuous constraints. Constraints, 1(1/2):85–118, September 1996.Google Scholar
  30. 30.
    S. P. Shary. Outer estimation of generalized solution sets to interval linear systems. Reliable Computing, 5:323–335, 1999.zbMATHCrossRefMathSciNetGoogle Scholar
  31. 31.
    A. Tarski. A Decision Method for Elementary Algebra and Geometry. Univ. of California Press, Berkeley, 1951. Also in [7].zbMATHGoogle Scholar
  32. 32.
    L. van den Dries. Alfred Tarski’s elimination theory for real closed fields. Journal of Symbolic Logic, 53(1):7–19, 1988.zbMATHCrossRefMathSciNetGoogle Scholar
  33. 33.
    V. Weispfenning. The complexity of linear problems in fields. Journal of Symbolic Computation, 5(1–2):3–27, 1988.zbMATHMathSciNetCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Stefan Ratschan
    • 1
  1. 1.Institut d’Informatica i AplicacionsUniversitat de GironaSpain

Personalised recommendations