Abstract
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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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.
F. Benhamou. Interval constraint logic programming. InPodelski [21].
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.
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.
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.
F. Benhamou and W. J. Older. Applying interval arithmetic to real, integer and Boolean constraints. Journal of Logic Programming, 32(1):1–24, 1997.
B. F. Caviness and J. R. Johnson, editors. Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer, 1998.
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].
G. E. Collins and H. Hong. Partial cylindrical algebraic decomposition for quantifier elimination. Journal of Symbolic Computation, 12:299–328, 1991. Also in [7].
J. H. Davenport and J. Heintz. Real quantifier elimination is doubly exponential. Journal of Symbolic Computation, 5:29–35, 1988.
L. Granvilliers. A symbolic-numerical branch and prune algorithm for solving nonlinear polynomial systems. Journal of Universal Computer Science, 4(2):125–146, 1998.
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.
P. V. Hentenryck, V. Saraswat, and Y. Deville. The design, implementation, and evaluation of the constraint language cc(FD). In Podelski [21].
H. Hong and V. Stahl. Safe starting regions by fixed points and tightening. Computing, 53:323–335, 1994.
L. Jaulin and É. Walter. Guaranteed tuning, with application to robust control and motion planning. Automatica, 32(8):1217–1221, 1996.
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.
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.
S. Malan, M. Milanese, and M. Taragna. Robust analysis and design of control systems using interval arithmetic. Automatica, 33(7):1363–1372, 1997.
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.
A. Neumaier. Interval Methods for Systems of Equations. Cambridge Univ. Press, Cambridge, 1990.
A. Podelski, editor. Constraint Programming: Basics and Trends, volume 910 of LNCS. Springer Verlag, 1995.
S. Ratschan. Approximate quantified constraint solving (AQCS). http://www.risc.uni-linz.ac.at/research/software/AQCS, 2000. Software package.
S. Ratschan. Applications of real first-order constraint solving —bibliography. http://www.risc.uni-linz.ac.at/people/sratscha/appFOC.html, 2001.
S. Ratschan. Real first-order constraints are stable with probability one. http://www.risc.uni-linz.ac.at/people/sratscha, 2001. Draft.
S. Ratschan. Approximate quantified constraint solving by cylindrical box decomposition. Reliable Computing, 8(1):21–42, 2002.
S. Ratschan. Quantified constraints under perturbations. Journal of Symbolic Computation, 33(4):493–505, 2002.
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.
D. Richardson. Some undecidable problems involving elementary functions of a real variable. Journal of Symbolic Logic, 33:514–520, 1968.
D. Sam-Haroud and B. Faltings. Consistency techniques for continuous constraints. Constraints, 1(1/2):85–118, September 1996.
S. P. Shary. Outer estimation of generalized solution sets to interval linear systems. Reliable Computing, 5:323–335, 1999.
A. Tarski. A Decision Method for Elementary Algebra and Geometry. Univ. of California Press, Berkeley, 1951. Also in [7].
L. van den Dries. Alfred Tarski’s elimination theory for real closed fields. Journal of Symbolic Logic, 53(1):7–19, 1988.
V. Weispfenning. The complexity of linear problems in fields. Journal of Symbolic Computation, 5(1–2):3–27, 1988.
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
Ratschan, S. (2002). Continuous First-Order Constraint Satisfaction. In: Calmet, J., Benhamou, B., Caprotti, O., Henocque, L., Sorge, V. (eds) Artificial Intelligence, Automated Reasoning, and Symbolic Computation. AISC Calculemus 2002 2002. Lecture Notes in Computer Science(), vol 2385. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45470-5_18
Download citation
DOI: https://doi.org/10.1007/3-540-45470-5_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43865-6
Online ISBN: 978-3-540-45470-0
eBook Packages: Springer Book Archive