Continuous First-Order Constraint Satisfaction
- 243 Downloads
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.
KeywordsConstraint Programming Reasoning
Unable to display preview. Download preview PDF.
- 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.F. Benhamou. Interval constraint logic programming. InPodelski .Google Scholar
- 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.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.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
- 7.B. F. Caviness and J. R. Johnson, editors. Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer, 1998.Google Scholar
- 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 .Google Scholar
- 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.P. V. Hentenryck, V. Saraswat, and Y. Deville. The design, implementation, and evaluation of the constraint language cc(FD). In Podelski .Google Scholar
- 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.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
- 22.S. Ratschan. Approximate quantified constraint solving (AQCS). http://www.risc.uni-linz.ac.at/research/software/AQCS, 2000. Software package.
- 23.S. Ratschan. Applications of real first-order constraint solving —bibliography. http://www.risc.uni-linz.ac.at/people/sratscha/appFOC.html, 2001.
- 24.S. Ratschan. Real first-order constraints are stable with probability one. http://www.risc.uni-linz.ac.at/people/sratscha, 2001. Draft.
- 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
- 29.D. Sam-Haroud and B. Faltings. Consistency techniques for continuous constraints. Constraints, 1(1/2):85–118, September 1996.Google Scholar