skip to main content
article

Efficient solving of quantified inequality constraints over the real numbers

Published: 01 October 2006 Publication History

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]
Apt, K. R. 1999. The essence of constraint propagation. Theoret. Comput. Sci. 221, 1--2.]]
[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]
Benhamou, F. 1995. Interval constraint logic programming. In Constant Programming: Basic and Trends. Lecture Notes in Computer Science, vol. 910, Springer-Verlag, New York.]]
[6]
Benhamou, F., and Goualard, F. 2000. Universally quantified interval constraints. In Proceedings of the 6th International Conference on Principles and Practice of Constraint Programming (CP'2000). (Singapore). Lecture Notes in Computer Science, vol. 1894, Springer-Verlag, New York,]]
[7]
Benhamou, F., Goualard, F., Granvilliers, L., and Puget, J. F. 1999. Revising hull and box consistency. In Proceedings of the International Conference on Logic Programming. MIT Press, Cambridge, MA, 230--244.]]
[8]
Benhamou, F., McAllester, D., and Van Hentenryck, P. 1994. CLP(Intervals) revisited. In International Symposium on Logic Programming. (Ithaca, NY), MIT Press, Cambridge, MA, 124--138.]]
[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]
Bordeaux, L. and Monfroy, E. 2002. Beyond NP: Arc-consistency for quantified constraints. In Proceedings of the Principles and Practice of Constraint Programming (CP 2002). P. Van Hentenryck, Ed. Lecture Notes in Computer Science, vol. 2470, Springer-Verlag, New York.]]
[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]
Collavizza, H., Delobel, F., and Rueher, M. 1999. Extending consistent domains of numeric CSP. In IJCAI-99. (Stockholm, Sweden).]]
[14]
Collins, G. E. 1975. Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition. In 2nd GI Conference on Automata Theory and Formal Languages. Lecture Notes in Computer Science, vol. 33. Springer-Verlag, New York, 134--183. (Also in Caviness, B. F. and Johnson, J. R., Eds. 1998). Springer, Wien, Austria. 134--183.]]
[15]
Collins, G. E. and Hong, H. 1991. Partial cylindrical algebraic decomposition for quantifier elimination. J. Symb. Comput. 12, 299--328. Also in Caviness and Johnson 1998.]]
[16]
Cousot, P. and Cousot, R. 1977. Automatic synthesis of optimal invariant assertions: Mathematical foundations. In Proceedings of the 1977 Symposium on Artificial Intelligence and Programming Languages. 1--12.]]
[17]
Csendes, T. and Ratz, D. 1997. Subdivision direction selection in interval methods for global optimization. SIAM J. Numer. Anal. 34, 3, 922--938.]]
[18]
Davenport, J. H. and Heintz, J. 1988. Real quantifier elimination is doubly exponential. J. Symb. Comput. 5, 29--35.]]
[19]
Dorato, P. 2000. Quantified multivariate polynomial inequalities. IEEE Cont. Syst. Mag. 20, 5 (Oct.), 48--58.]]
[20]
Dorato, P., Yang, W., and Abdallah, C. 1997. Robust multi-objective feedback design by quantifier elimination. J. Symb. Comput. 24, 153--159.]]
[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]
Jaulin, L. and Walter, É. 1996. Guaranteed tuning, with application to robust control and motion planning. Automatica 32, 8, 1217--1221.]]
[29]
Jourdan, J. and Sola, T. 1993. The versatility of handling disjunctions as constraints. In Proceedings of the 5th International Symposium on Programming Language Implementation and Logic Programming, PLILP'93, M. Bruynooghe and J. Penjam, Eds. Lecture Notes in Computer Science, vol. 714, Springer-Verlag, New York, 60--74.]]
[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]
Malan, S., Milanese, M., and Taragna, M. 1997. Robust analysis and design of control systems using interval arithmetic. Automatica 33, 7, 1363--1372.]]
[34]
Marriott, K., Moulder, P., Stuckey, P. J., and Borning, A. 2001. Solving disjunctive constraints for interactive graphical applications. In Proceedings of the 7th International Conference on Principles and Practice of Constraint Programming (CP2001). Lecture Notes in Computer Science, vol. 2239, Springer-Verlag, New York, 361--376.]]
[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]
Podelski, A., Ed. 1995. Constraint Programming: Basics and Trends. Lecture Notes in Computer Science, vol. 910. Springer-Verlag, New York.]]
[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]
Ratschan, S. 2002b. Continuous first-order constraint satisfaction. In Artificial Intelligence, Automated Reasoning, and Symbolic Computation, J. Calmet, B. Benhamou, O. Caprotti, L. Henocque, and V. Sorge, Eds. Lecture Notes in Computer Science, vol. 2385, Springer-Verlag, New York, 181--195.]]
[43]
Ratschan, S. 2002c. Continuous first-order constraint satisfaction with equality and disequality constraints. In Proceedings of the 8th International Conference on Principles and Practice of Constraint Programming, P. van Hentenryck, Ed. Lecture Notes in Computer Science, vol. 2470, Springer-Verlag, New York, 680--685.]]
[44]
Ratschan, S. 2002d. Quantified constraints under perturbations. J. Symb. Comput. 33, 4, 493--505.]]
[45]
Ratschan, S. 2002e. Search heuristics for box decomposition methods. J. Glob. Optimiz. 24, 1, 51--60.]]
[46]
Renegar, J. 1992. On the computational complexity and geometry of the first-order theory of the reals. J. Symb. Comput. 13, 3 (Mar.), 255--352.]]
[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]
Van Hentenryck, P., McAllester, D., and Kapur, D. 1997a. Solving polynomial systems using a branch and prune approach. SIAM J. Numer. Anal. 34, 2, 797--827.]]
[56]
Van Hentenryck, P., Michel, L., and Deville, Y. 1997b. Numerica: A Modeling Language for Global Optimization. The MIT Press, Cambridge, MA.]]
[57]
Van Hentenryck, P., Saraswat, V., and Deville, Y. 1995. The design, implementation, and evaluation of the constraint language cc(FD). In Constraint Programming: Basics and Trends, A. Podelski, Ed. Lecture Notes in Computer Science, vol. 910, Springer-Verlag, New York.]]
[58]
Walsh, T. 2002. Stochastic constraint programming. In Proceedings of ECAI.]]
[59]
Weispfenning, V. 1988. The complexity of linear problems in fields. J. Symb. Comput. 5, 1--2, 3--27.]]

Cited By

View all
  • (2023)A GPU-Based Parallel Region Classification Method for Continuous Constraint Satisfaction ProblemsJournal of Mechanical Design10.1115/1.4063158146:4Online publication date: 6-Dec-2023
  • (2023)Constraint-Guided Automatic Side Object Placement for Steering Control Testing in Virtual Environment2023 IEEE Conference on Software Testing, Verification and Validation (ICST)10.1109/ICST57152.2023.00015(60-70)Online publication date: Apr-2023
  • (2023)Reachability Based Uniform Controllability to Target Set with Evolution FunctionDependable Software Engineering. Theories, Tools, and Applications10.1007/978-981-99-8664-4_2(21-37)Online publication date: 27-Nov-2023
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Computational Logic
ACM Transactions on Computational Logic  Volume 7, Issue 4
October 2006
226 pages
ISSN:1529-3785
EISSN:1557-945X
DOI:10.1145/1183278
Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 October 2006
Published in TOCL Volume 7, Issue 4

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. Constraint solving
  2. decision procedures
  3. numerical constraints

Qualifiers

  • Article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)9
  • Downloads (Last 6 weeks)0
Reflects downloads up to 25 Oct 2024

Other Metrics

Citations

Cited By

View all
  • (2023)A GPU-Based Parallel Region Classification Method for Continuous Constraint Satisfaction ProblemsJournal of Mechanical Design10.1115/1.4063158146:4Online publication date: 6-Dec-2023
  • (2023)Constraint-Guided Automatic Side Object Placement for Steering Control Testing in Virtual Environment2023 IEEE Conference on Software Testing, Verification and Validation (ICST)10.1109/ICST57152.2023.00015(60-70)Online publication date: Apr-2023
  • (2023)Reachability Based Uniform Controllability to Target Set with Evolution FunctionDependable Software Engineering. Theories, Tools, and Applications10.1007/978-981-99-8664-4_2(21-37)Online publication date: 27-Nov-2023
  • (2023)What if There Are Too Many Outliers?Uncertainty, Constraints, and Decision Making10.1007/978-3-031-36394-8_58(363-370)Online publication date: 19-Sep-2023
  • (2022)Reach-Avoid Verification for Time-varying Systems with Uncertain Disturbances2022 20th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE)10.1109/MEMOCODE57689.2022.9954600(1-12)Online publication date: 13-Oct-2022
  • (2022)Computing Funnels Using Numerical Optimization Based Falsifiers*2022 International Conference on Robotics and Automation (ICRA)10.1109/ICRA46639.2022.9811730(4318-4324)Online publication date: 23-May-2022
  • (2021)Formal Synthesis of Stochastic Systems via Control Barrier CertificatesIEEE Transactions on Automatic Control10.1109/TAC.2020.301391666:7(3097-3110)Online publication date: Jul-2021
  • (2020)Synthesis of Stochastic Systems with Partial Information via Control Barrier FunctionsIFAC-PapersOnLine10.1016/j.ifacol.2020.12.18753:2(2441-2446)Online publication date: 2020
  • (2019)Test Specification and Generation for Connected and Autonomous Vehicle in Virtual EnvironmentsACM Transactions on Cyber-Physical Systems10.1145/33119544:1(1-26)Online publication date: 2-Nov-2019
  • (2019)IntroductionInterval Methods for Solving Nonlinear Constraint Satisfaction, Optimization and Similar Problems10.1007/978-3-030-13795-3_1(1-3)Online publication date: 9-Mar-2019
  • Show More Cited By

View Options

Get Access

Login options

Full Access

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media