Efficient solving of quantified inequality constraints over the real numbers

ABSTRACT

Let a quantified inequality constraint over the reals be a formula in the first-order predicate language over the structure of the real numbers, where the allowed predicate symbols are ≤ and <. Solving such constraints is an undecidable problem when allowing function symbols such sin or cos. In this article, we give an algorithm that terminates with a solution for all, except for very special, pathological inputs. We ensure the practical efficiency of this algorithm by employing constraint programming techniques.

REFERENCES

• 1: Abdallah, C., Dorato, P., Yang, W., Liska, R., and Steinberg, S. 1996. Applications of quantifier elimination theory to control system design. In Proceedings of the 4th IEEE Mediterranean Symposium on Control and Automation, (Crete, Greece), IEEE Computer Society Press, Los Alamitos, CA.
• 2: Anderson, B. D. O., Bose, N. K., and Jury, E. I. 1975. Output feedback stabilization and related problems---solution via decision methods. IEEE Trans. Automatic Control AC-20, 53--66.
• 3: Krzysztof R. Apt, The essence of constraint propagation, Theoretical Computer Science, v.221 n.1-2, p.179-210, June 28, 1999 [doi>10.1016/S0304-3975(99)00032-8 ]
• 4: Basu, S., Pollack, R., and Roy, M.-F. 1994. On the combinatorial and algebraic complexity of quantifier elimination. In Proceedings of the 35th Annual Symposium on Foundations of Computer Science, S. Goldwasser, Ed. IEEE Computer Society Press, Los Alamitos, CA, 632--641.
• 5: Frédéric Benhamou, Interval Constraint Logic Programming, Selected Papers from Constraint Programming: Basics and Trends, p.1-21, May 16-20, 1994
• 6: Frédéric Benhamou , Frédéric Goualard, Universally Quantified Interval Constraints, Proceedings of the 6th International Conference on Principles and Practice of Constraint Programming, p.67-82, September 18-21, 2000
• 7: Frédéric Benhamou , Frédéric Goualard , Laurent Granvilliers , Jean-François Puget, Revising hull and box consistency, Proceedings of the 1999 international conference on Logic programming, p.230-244, November 1999, Las Cruces, New Mexico, United States
• 8: F. Benhamou , D. McAllester , P. van Hentenryck, CLP(intervals) revisited, Proceedings of the 1994 International Symposium on Logic programming, p.124-138, November 1994, Symposia, Melbourne
• 9: Benhamou, F. and Older, W. J. 1997. Applying interval arithmetic to real, integer and Boolean constraints. J. Logic Prog. 32, 1, 1--24.
• 10: Lucas Bordeaux , Eric Monfroy, Beyond NP: Arc-Consistency for Quantified Constraints, Proceedings of the 8th International Conference on Principles and Practice of Constraint Programming, p.371-386, September 09-13, 2002
• 11: Caviness, B. F. and Johnson, J. R., Eds. 1998. Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer, Wien, Austria.
• 12: Cleary, J. G. 1987. Logical arithmetic. Future Comput. Syst. 2, 2, 125--149.
• 13: Hélène Collavizza , François Delobel , Michel Rueher, Extending Consistent Domains of Numeric CSP, Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence, p.406-413, July 31-August 06, 1999
• 14: George E. Collins, Hauptvortrag: Quantifier elimination for real closed fields by cylindrical algebraic decomposition, Proceedings of the 2nd GI Conference on Automata Theory and Formal Languages, p.134-183, May 20-23, 1975
• 15: George E. Collins , Hoon Hong, Partial cylindrical algebraic decomposition for quantifier elimination, Journal of Symbolic Computation, v.12 n.3, p.299-328, Sept. 1991
• 16: Patrick Cousot , Radhia Cousot, Automatic synthesis of optimal invariant assertions: Mathematical foundations, Proceedings of the 1977 symposium on Artificial intelligence and programming languages, p.1-12, August 15-17, 1977
• 17: T. Csendes , D. Ratz, Subdivision Direction Selection in Interval Methods for Global Optimization, SIAM Journal on Numerical Analysis, v.34 n.3, p.922-938, June 1997 [doi>10.1137/S0036142995281528]
• 18: James H. Davenport , Joos Heintz, Real quantifier elimination is doubly exponential, Journal of Symbolic Computation, v.5 n.1-2, p.29-35, February/April 1988 [doi>10.1016/S0747-7171(88)80004-X]
• 19: Dorato, P. 2000. Quantified multivariate polynomial inequalities. IEEE Cont. Syst. Mag. 20, 5 (Oct.), 48--58.
• 20: Peter Dorato , Wei Yang , Chaouki Abdallah, Robust multi-objective feedback design by quantifier elimination, Journal of Symbolic Computation, v.24 n.2, p.153-159, August 1997 [doi>10.1006/jsco.1997.0120 ]
• 21: Fargier, H., Lang, J., and Schiex, T. 1996. Mixed constraint satisfaction: A framework for decision problems under incomplete knowledge. In Proceedings of AAAI'96.
• 22: Fiorio, G., Malan, S., Milanese, M., and Taragna, M. 1993. Robust performance design of fixed structure controllers with uncertain parameters. In Proceedings of the 32nd IEEE Conference Decision and Control. IEEE Computer Society Press, Los Alamitos, CA, 3029--3031.
• 23: Garloff, J. and Graf, B. 1999. Solving strict polynomial inequalities by Bernstein expansion. In The Use of Symbolic Methods in Control System Analysis and Design, N. Munro, Ed. The Institution of Electrical Engineering (IEE), 339--352.
• 24: Granvilliers, L. 1998. A symbolic-numerical branch and prune algorithm for solving non-linear polynomial systems. J. Univ. Comput. Sci. 4, 2, 125--146.
• 25: Hong, H. and Stahl, V. 1994. Safe starting regions by fixed points and tightening. Computing 53, 323--335.
• 26: Jaulin, L., Braems, I., and Walter, É. 2002. Interval methods for nonlinear identification and robust control. In Proceedings of the 41st IEEE Conference on Decision and Control. IEEE Computer Society Press, Los Alamitos, CA.
• 27: Jaulin, L., Kieffer, M., Didrit, O., and Walter, É. 2001. Applied Interval Analysis, with Examples in Parameter and State Estimation, Robust Control and Robotics. Springer, Berlin, Germany.
• 28: Luc Jaulin , Éric Walter, Guaranteed tuning, with application to robust control and motion planning, Automatica (Journal of IFAC), v.32 n.9, p.1217-1221, Aug. 1996
• 29: Jean Jourdan , Thierry Sola, The Versatility of Handling Disjunctions as Constraints, Proceedings of the 5th International Symposium on Programming Language Implementation and Logic Programming, p.60-74, August 25-27, 1993
• 30: Kreinovich, V. and Csendes, T. 2001. Theoretical justification of a heuristic subbox selection criterion for interval global optimization. Central European J. Oper. Res. 9, 255--265.
• 31: Loos, R. and Weispfenning, V. 1993. Applying linear quantifier elimination. Comput. J. 36, 5, 450--462.
• 32: Macintyre, A. and Wilkie, A. 1996. On the decidability of the real exponential field. In Kreiseliana---About and Around Georg Kreisel, P. Odifreddi, Ed. A. K. Peters, 441--467.
• 33: S. Malan , M. Milanese , M. Taragna, Robust analysis and design of control systems using interval arithmetic, Automatica (Journal of IFAC), v.33 n.7, p.1363-1372, July 1997 [doi>10.1016/S0005-1098(97)00028-9 ]
• 34: Kim Marriott , Peter Moulder , Peter J. Stuckey , Alan Borning, Solving Disjunctive Constraints for Interactive Graphical Applications, Proceedings of the 7th International Conference on Principles and Practice of Constraint Programming, p.361-376, November 26-December 01, 2001
• 35: McCallum, S. 1993. Solving polynomial strict inequalities using cylindrical algebraic decomposition. Comput. J. 36, 5, 432--438.
• 36: Moore, R. E. 1966. Interval Analysis. Prentice Hall, Englewood Cliffs, NJ.
• 37: Neumaier, A. 1990. Interval Methods for Systems of Equations. Cambridge University Press, Cambridge, UK.
• 38: Andreas Podelski, Constraint Programming: Basics and Trends: 1994 Chatillon Spring School, Chantillon-Sur-Seine, France, May 16-20, 1994: Selected Papers, Springer-Verlag New York, Inc., Secaucus, NJ, 1995
• 39: Ratschan, S. 2001a. Applications of quantified constraint solving over the reals---bibliography. http://www.mpi-sb.mpg.de/~ratschan/appqcs.html.
• 40: Ratschan, S. 2001b. Real first-order constraints are stable with probability one. http://www.mpi-sb.mpg.de/~ratschan/preprints.html.Draft.
• 41: Ratschan, S. 2002a. Approximate quantified constraint solving by cylindrical box decomposition. Rel. Comput. 8, 1, 21--42.
• 42: Stefan Ratschan, Continuous First-Order Constraint Satisfaction, Proceedings of the Joint International Conferences on Artificial Intelligence, Automated Reasoning, and Symbolic Computation, p.181-195, July 01-05, 2002
• 43: Stefan Ratschan, Continuous First-Order Constraint Satisfactionwith Equality and Disequality Constraints, Proceedings of the 8th International Conference on Principles and Practice of Constraint Programming, p.680-685, September 09-13, 2002
• 44: Stefan Ratschan, Quantified constraints under perturbation, Journal of Symbolic Computation, v.33 n.4, p.493-505, April 2002 [doi>10.1006/jsco.2001.0519 ]
• 45: Stefan Ratschan, Search Heuristics for Box Decomposition Methods, Journal of Global Optimization, v.24 n.1, p.35-49, September 2002 [doi>10.1023/A:1016246616462 ]
• 46: James Renegar, On the computational complexity and geometry of the first-order theory of the reals. Par I: Introduction. Preliminaries. The geometry of semi-algebraic sets. The decision problem for the existential theory of the reals, Journal of Symbolic Computation, v.13 n.3, p.255-299, March 1992
• 47: Revol, N. and Rouillier, F. 2005. Motivations for an arbitrary precision interval arithmetic and the MPFI library. Reli. Comput. 11, 4, 275--290.
• 48: Richardson, D. 1968. Some undecidable problems involving elementary functions of a real variable. J. Symb. Logic 33, 514--520.
• 49: Sam-Haroud, D. and Faltings, B. 1996. Consistency techniques for continuous constraints. Constraints 1, 1/2 (Sept.), 85--118.
• 50: Shary, S. P. 1999. Outer estimation of generalized solution sets to interval linear systems. Reli. Comput. 5, 323--335.
• 51: Shary, S. P. 2002. A new technique in systems analysis under interval uncertainty and ambiguity. Reli. Comput. 8, 321--418.
• 52: Silaghi, M.-C., Sam-Haroud, D., and Faltings, B. 2001. Search techniques for non-linear constraints with inequalities. In Proceedings of the 14th Canadian Conference on AI.
• 53: Tarski, A. 1951. A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley, CA. (Also in Caviness and Johnson {1998}).
• 54: van den Dries, L. 1988. Alfred Tarski's elimination theory for real closed fields. J. Symb. Logic 53, 1, 7--19.
• 55: Pascal Van Hentenryck , David McAllester , Deepak Kapur, Solving Polynomial Systems Using a Branch and Prune Approach, SIAM Journal on Numerical Analysis, v.34 n.2, p.797-827, April. 1997 [doi>10.1137/S0036142995281504]
• 56: Van Hentenryck, P., Michel, L., and Deville, Y. 1997b. Numerica: A Modeling Language for Global Optimization. The MIT Press, Cambridge, MA.
• 57: Pascal Van Hentenryck , Vijay A. Saraswat , Yves Deville, Design, Implementation, and Evaluation of the Constraint Language cc(FD), Selected Papers from Constraint Programming: Basics and Trends, p.293-316, May 16-20, 1994
• 58: Walsh, T. 2002. Stochastic constraint programming. In Proceedings of ECAI.
• 59: Volker Weispfenning, The complexity of linear problems in fields, Journal of Symbolic Computation, v.5 n.1-2, p.3-27, February/April 1988 [doi>10.1016/S0747-7171(88)80003-8]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Logic and constraint programming

Additional Classification:
  G. Mathematics of Computing
  G.1 NUMERICAL ANALYSIS
      G.1.0 General
          Subjects: Stability (and instability); Interval arithmetic

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving

General Terms:
Algorithms, Theory, Verification

Keywords:
Constraint solving, decision procedures, numerical constraints