Advertisement

Formal Methods in System Design

, Volume 48, Issue 3, pp 257–273 | Cite as

A search-based procedure for nonlinear real arithmetic

  • Ashish Tiwari
  • Patrick Lincoln
Article
  • 190 Downloads

Abstract

We present a new procedure for testing satisfiability (over the reals) of a conjunction of polynomial equations. There are three possible return values for our procedure: it either returns a model for the input formula, or it says that the input is unsatisfiable, or it fails because the applicability condition for the procedure, called the eigen-condition, is violated. For the class of constraints where the eigen-condition holds, our procedure is a decision procedure. We describe satisfiability-preserving transformations that can potentially convert problems into a form where eigen-condition holds. We experimentally evaluate the procedure on constraints generated by template-based verification and synthesis procedures.

Keywords

Nonlinear arithmetic Theory of reals Polynomials  SAT solving Program verification 

Notes

Acknowledgments

This work was sponsored, in part, by Defense Advanced Research Projects Agency (DARPA) and Air Force Research Laboratory (AFRL), under contract FA8750-12-C-0284, and the National Science Foundation under Grant CNS-1423298. The views, opinions, and/or findings contained in this report are those of the authors and should not be interpreted as representing the official views or policies, either expressed or implied, of the funding agencies.

References

  1. 1.
    Akbarpour B, Paulson LC (2010) MetiTarski: An automatic theorem prover for real-valued special functions. J Autom Reason 44(3):175–205MathSciNetCrossRefMATHGoogle Scholar
  2. 2.
    Bachmair L, Ganzinger H (1994) Buchberger’s algorithm: a constraint-based completion procedure. In: Proceedings of 1st international conference constraints in computational logic, LNCS 845, Springer, pp 285–301Google Scholar
  3. 3.
    Basu S, Pollack R, Roy MF (1996) On the combinatorial and algebraic complexity of quantifier elimination. J ACM 43(6):1002–1045MathSciNetCrossRefMATHGoogle Scholar
  4. 4.
    Bochnak J, Coste M, Roy MF (1998) Real algebraic geometry. Springer, New YorkCrossRefMATHGoogle Scholar
  5. 5.
    Buchberger B (1983) A critical-pair completion algorithm for finitely generated ideals in rings. In: Proceedings of logic and machines: decision problems and complexity, LNCS, vol. 171, pp 137–161Google Scholar
  6. 6.
    Cheng CH, Ruess H, Shankar N (2013) JBernstein: a validity checker for generalized polynomial constraints. In: Proceedings of 25th international conference computer aided verification, CAV, vol. LNCS 8044, Springer, pp 656–661Google Scholar
  7. 7.
    Cheng CH, Shankar N, Ruess H, Bensalem S (2013) EFSMT: a logical framework for cyber-physical systems. CoRR abs/1306.3456 Google Scholar
  8. 8.
    Collins GE (1975) Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition. In: Proceedings of 2nd GI Conference on Automata Theory and Formal Languages, LNCS, Springer, vol. 33, pp 134–183Google Scholar
  9. 9.
    Collins GE, Hong H (1991) Partial cylindrical algebraic decomposition for quantifier elimination. J Symb Comput 12(3):299–328MathSciNetCrossRefMATHGoogle Scholar
  10. 10.
    Colon M, Sankaranarayanan S, Sipma H (2003) Linear invariant generation using non-linear constraint solving. In: Computer-Aided Verification (CAV), LNCS, Springer-Verlag, vol. 2725, pp 420–433Google Scholar
  11. 11.
    Davenport JH, Heintz J (1988) Real quantifier elimination is doubly exponential. J Symb Comput 5(1–2):29–35MathSciNetCrossRefMATHGoogle Scholar
  12. 12.
    Davis M, Logemann G, Loveland D (1962) A machine program for theorem-proving. CACM 5(7):394–397MathSciNetCrossRefMATHGoogle Scholar
  13. 13.
    Demmel J, Dumitriu I, Holtz O (2007) Fast linear algebra is stable. Numer Math 108:59–91MathSciNetCrossRefMATHGoogle Scholar
  14. 14.
    Fränzle M, Herde C, Teige T, Ratschan S, Schubert T (2007) Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. JSAT 1(3–4):209–236MATHGoogle Scholar
  15. 15.
    Ganzinger H, Hagen G, Nieuwenhuis R, Oliveras A, Tinelli C (2004) DPLL(T): fast decision procedures. In: Proceedings of 16th International Conference on Computer Aided Verification, CAV 2004, LNCS, Springer, vol 3114, pp 175–188Google Scholar
  16. 16.
    Gao S, Avigad J, Clarke EM (2012) \(\delta \)-complete decisionprocedures for satisfiability over the reals. In: Proceedings 6th International Conference Automated Reasoning, IJCAR, LNCS 7364, pp 286–300Google Scholar
  17. 17.
    Gao S, Kong S, Clarke EM (2013) dReal: An SMT solver for nonlinear theories over the reals. In: Proceedings of 24th International Conference on Automated Deduction, CADE, LNCS 7898, Springer, pp 208–214Google Scholar
  18. 18.
    Grigoriev D (1988) Complexity of deciding Tarski algebra. J Symb Comput 5(1–2):65–108MathSciNetCrossRefMATHGoogle Scholar
  19. 19.
    Gulwani S, Jha S, Tiwari A, Venkatesan R (2011) Synthesis of loop-free programs. In: Proceedings of ACM Conference on Prgramming Language Designing and Implementation of PLDI, pp 62–73Google Scholar
  20. 20.
    Gulwani S, Srivastava S, Venkatesan R (2008) Program analysis as constraint solving. In: Proceedings of ACM Conference on Prgramming Language Design and implementaion, PLDI, pp 281–292Google Scholar
  21. 21.
    Gulwani S, Tiwari A (2008) Constraint-based approach for analysis of hybrid systems. In: Proceedings of 20th International Conference on Computer Aided Verification, CAV 2008, LNCS, vol. 5123, pp 190–203. Springer. July 7–14, 2008, Princeton, NJGoogle Scholar
  22. 22.
    Hong H (1990) An improvement of the projection operator in cylindrical algebraic decomposition. In: Proceedings of ISAAC 90, pp 261–264Google Scholar
  23. 23.
    Hong H, Safey El Din M (2009) Variant real quantifier elimination: algorithm and application. In: ISSAC, pp 183–190. ACM. doi: 10.1145/1576702.1576729
  24. 24.
    Iwane H, Yanami H, Anai H (2011) An effective implementation of a symbolic-numeric cylindrical algebraic decomposition for optimization problems. In: Proceedings of International Workshop on Symbolic Numeric Computation, SNC, pp 168–177. ACMGoogle Scholar
  25. 25.
    Jovanovic D, de Moura LM (2012) Solving non-linear arithmetic. In: Proceedings of 6th International Conference Automated Reasoning, IJCAR, LNCS 7364, Springer, pp 339–354Google Scholar
  26. 26.
    Leike J (2014) Software and benchmarks for synthesis for polynomial lasso programs http://www.csl.sri.com/~tiwari/softwares/synthesis_for_polynomial_lasso_programs_source.zip
  27. 27.
    Leike J, Tiwari A (2014) Synthesis for polynomial lasso programs. In: Proceedings of VMCAI, LNCS 8318, pp 454–472Google Scholar
  28. 28.
    Loup U, Scheibler K, Corzilius F, Ábrahám E, Becker B (2013) A symbiosis of interval constraint propagation and cylindrical algebraic decomposition. In: Proceedings of 24th International Conference on Automated Deduction, CADE, LNCS 7898, Springer, pp 193–207Google Scholar
  29. 29.
    Matringe N, Moura AV, Rebiha R (2010) Generating invariants for non-linear hybrid systems by linear algebraic methods. In: Proceedings of 17th International Static Analysis Symposium, SAS, Springer, vol. LNCS 6337, pp 373–389Google Scholar
  30. 30.
    Microsoft Research: Z3: An efficient SMT solver. http://research.microsoft.com/projects/z3/
  31. 31.
    Parrilo PA (2003) Semidefinite programming relaxations for semialgebraic problems. Math Program Ser B 96(2):293–320MathSciNetCrossRefMATHGoogle Scholar
  32. 32.
    Rebiha R, Matringe N, Moura AV (2012) Transcendental inductive invariants generation for non-linear differential and hybrid systems. In: Proceedings of Hybrid System: Computation and Control, HSCC, pp 25–34. ACMGoogle Scholar
  33. 33.
    Renegar J (1992) On the computational complexity and geometry of the first-order theory of the reals. J Symb Comput 13(3):255–352MathSciNetCrossRefMATHGoogle Scholar
  34. 34.
    Sankaranarayanan S, Sipma H, Manna Z (2004) Constructing invariants for hybrid systems. In: R. Alur, G.J. Pappas (eds.) Hybrid systems: computation and control, HSCC 2004, Lecture Notes in Computer Science, vol. 2993, pp 539–554. SpringerGoogle Scholar
  35. 35.
    Sankaranarayanan S, Sipma HB, Manna Z (2008) Constructing invariants for hybrid systems. Formal Methods Syst Des 32(1):25–55CrossRefMATHGoogle Scholar
  36. 36.
    SRI International: Yices: An SMT solver. http://yices.csl.sri.com/
  37. 37.
    Srivastava S, Gulwani S, Foster JS (2013) Template-based program verification and program synthesis. STTT 15(5–6):497–518CrossRefGoogle Scholar
  38. 38.
    Stengle G (1974) A Nullstellensatz and a Positivstellensatz insemialgebraic geometry. Math Ann 207Google Scholar
  39. 39.
    Sturm T, Tiwari A (2011) Verification and synthesis using real quantifier elimination. In: Proceedings of International Symposium on Symbolic and Algebraic Computation , ISSAC, pp 329–336. ACMGoogle Scholar
  40. 40.
    Taly A, Gulwani S, Tiwari A (2009) Synthesizing switching logic using constraint solving. In: Proc. 10th Intl. Conf. on Verification, Model Checking and Abstract Interpretation, VMCAI, LNCS, Springer, vol. 5403, pp 305–319Google Scholar
  41. 41.
    Tarski A (1948) A decision method for elementary algebra and geometry, 2nd edn. University of California Press, BerkeleyMATHGoogle Scholar
  42. 42.
    Tiwari A (2005) An algebraic approach for the unsatisfiability of nonlinear constraints. In: Computer Science Logic, 14th Annual Conference, CSL 2005, LNCS, Springer, vol. 3634, pp 248–262Google Scholar
  43. 43.
    Tiwari A, Khanna G (2004) Nonlinear Systems: Approximating reach sets. In: Proceedings of 7th International Workshop on Hybrid Systems: Computation and Control, HSCC 2004, LNCS, Springer, vol. 2993, pp 600–614Google Scholar
  44. 44.
    Tiwari A, Lincoln P (2014) A nonlinear real arithmetic fragment. In: Proceedings on Computer Aided Verification CAV, LNCS, Springer, vol. 8559, pp 729–736Google Scholar

Copyright information

© Springer Science+Business Media New York 2016

Authors and Affiliations

  1. 1.SRI InternationalMenlo ParkUSA

Personalised recommendations