An Algebraic Approach for the Unsatisfiability of Nonlinear Constraints

  • Ashish Tiwari
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3634)


We describe a simple algebraic semi-decision procedure for detecting unsatisfiability of a (quantifier-free) conjunction of nonlinear equalities and inequalities. The procedure consists of Gröbner basis computation plus extension rules that introduce new definitions, and hence it can be described as a critical-pair completion-based logical procedure. This procedure is shown to be sound and refutationally complete. When projected onto the linear case, our procedure reduces to the Simplex method for solving linear constraints. If only finitely many new definitions are introduced, then the procedure is also terminating. Such terminating, but potentially incomplete, procedures are used in “incompleteness-tolerant” applications.


Inference Rule Polynomial Ring Algebraic Approach Polynomial Ideal Slack Variable 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Audemard, G., Bertoli, P., Cimatti, A., Kornilowicz, A., Sebastiani, R.: A SAT based approach for solving formulas over boolean and linear mathematical propositions. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 195–210. Springer, Heidelberg (2002)Google Scholar
  2. 2.
    Bachmair, L., Ganzinger, H.: Buchberger’s algorithm: A constraint-based completion procedure. In: Jouannaud, J.-P. (ed.) CCL 1994. LNCS, vol. 845, Springer, Heidelberg (1994)CrossRefGoogle Scholar
  3. 3.
    Bachmair, L., Tiwari, A.: D-bases for polynomial ideals over commutative noetherian rings. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol. 1103, pp. 113–127. Springer, Heidelberg (1996)Google Scholar
  4. 4.
    Basu, S., Gonzalez-Vega, L. (eds.): Algorithmic and Quantitative Real Algebraic Geometry. DIMACS Series in DMTCS, vol. 60 (2003)Google Scholar
  5. 5.
    Basu, S., Pollack, R., Roy, M.-F.: On the combinatorial and algebraic complexity of quantifier elimination. J. of the ACM 43(6), 1002–1045 (1996)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Bochnak, J., Coste, M., Roy, M.-F.: Real Algebraic Geometry. Springer, Heidelberg (1998)zbMATHGoogle Scholar
  7. 7.
    Collins, G.E.: Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975)Google Scholar
  8. 8.
    Datta, R.S.: Using computer algebra to compute Nash equilibria. In: Intl. Symp. on Symbolic and Algebraic Computation, ISSAC 2003, pp. 74–79 (2003)Google Scholar
  9. 9.
    de Moura, L., Owre, S., Rueß, H., Rushby, J., Shankar, N.: The ICS decision procedures for embedded deduction. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 218–222. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  10. 10.
    Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Communications of the ACM 22(8), 465–476 (1979)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Einsiedler, M., Tuncel, H.: When does a polynomial ideal contain a positive polynomial? J. Pure Appl. Algebra 164(1-2), 149–152 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    Harrison, J.: Theorem proving with the real numbers. Springer, Heidelberg (1998)zbMATHGoogle Scholar
  13. 13.
    Hong, H.: Quantifier elimination in elementary algebra and geometry by partial cylindrical algebraic decomposition version 13 (1995),,
  14. 14.
    Krivine, J.L.: Anneaux preordonnes. J. Anal. Math. 12, 307–326 (1964)zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    Parrilo, P.A.: SOS methods for semi-algebraic games and optimization. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, p. 54. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  16. 16.
    Prajna, S., Papachristodoulou, A., Parrilo, P.A.: SOSTOOLS: Sum of Square Optimization Toolbox (2002),
  17. 17.
    Ratschan, S.: Applications of quantified constraint solving over the reals: Bibliography (2004),
  18. 18.
    Renegar, J.: On the computational complexity and geometry of the first order theory of the reals. J. of Symbolic Computation 13(3), 255–352 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    Roy, M.-F.: Degree bounds for Stengle’s Positivstellensatz. In: Network workshop on real algebra (2003),
  20. 20.
    Stengle, G.: A Nullstellensatz and a Positivstellensatz in semialgebraic geometry. Math. Ann. 207, 87–97 (1974)CrossRefMathSciNetGoogle Scholar
  21. 21.
    Stump, A., Barrett, C.W., Dill, D.L.: CVC: A cooperating validity checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 500–504. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  22. 22.
    Tarski, A.: A Decision Method for Elementary Algebra and Geometry, 2nd edn. University of California Press (1948)Google Scholar
  23. 23.
    Tiwari, A., Khanna, G.: Series of abstractions for hybrid automata. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol. 2289, pp. 465–478. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  24. 24.
    Weispfenning, V.: The complexity of linear problems in fields. J. of Symbolic Computation 5 (1988)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Ashish Tiwari
    • 1
  1. 1.SRI InternationalMenlo ParkUSA

Personalised recommendations