Advertisement

Satisfiability of Non-linear (Ir)rational Arithmetic

  • Harald Zankl
  • Aart Middeldorp
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6355)

Abstract

We present a novel way for reasoning about (possibly ir)rational quantifier-free non-linear arithmetic by a reduction to SAT/SMT. The approach is incomplete and dedicated to satisfiable instances only but is able to produce models for satisfiable problems quickly. These characteristics suffice for applications such as termination analysis of rewrite systems. Our prototype implementation, called MiniSmt, is made freely available. Extensive experiments show that it outperforms current SMT solvers especially on rational and irrational domains.

Keywords

non-linear arithmetic SMT solving term rewriting termination matrix interpretations 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Alarcón, B., Lucas, S., Navarro-Marset, R.: Proving termination with matrix interpretations over the reals. In: WST 2009, pp. 12–15 (2009)Google Scholar
  2. 2.
    Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. TCS 236(1-2), 133–178 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Ashlock, D.: Evolutionary Computation for Modeling and Optimization. Springer, Heidelberg (2006)zbMATHGoogle Scholar
  4. 4.
    Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)CrossRefzbMATHGoogle Scholar
  5. 5.
    Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 298–302. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  6. 6.
    Borralleras, C., Lucas, S., Navarro-Marset, R., Rodriguez-Carbonell, E., Rubio, A.: Solving non-linear polynomial arithmetic via SAT modulo linear arithmetic. In: Schmidt, R.A. (ed.) Automated Deduction – CADE-22. Lecture Notes in Computer Science(LNAI), vol. 5663, pp. 294–305. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  7. 7.
    Codish, M., Lagoon, V., Stuckey, P.: Solving partial order constraints for LPO termination. JSAT 5, 193–215 (2008)MathSciNetzbMATHGoogle Scholar
  8. 8.
    Collins, G.E.: Quantifier elimination for 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
  9. 9.
    Courtieu, P., Gbedo, G., Pons, O.: Improved matrix interpretation. In: SOFSEM 2010. LNCS, vol. 5901, pp. 283–295. Springer, Heidelberg (2010)Google Scholar
  10. 10.
    Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  11. 11.
    Eén, N., Sörensson, N.: An extensible SAT-solver. In: SAT 2004. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)Google Scholar
  12. 12.
    Endrullis, J.: (Jambox), http://joerg.endrullis.de
  13. 13.
    Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. JAR 40(2-3), 195–220 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: SAT solving for termination analysis with polynomial interpretations. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 340–354. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  15. 15.
    Fuhs, C., Navarro-Marset, R., Otto, C., Giesl, J., Lucas, S., Schneider-Kamp, P.: Search techniques for rational polynomial orders. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) AISC 2008, Calculemus 2008, and MKM 2008. LNCS (LNAI), vol. 5144, pp. 109–124. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  16. 16.
    Gebhardt, A., Hofbauer, D., Waldmann, J.: Matrix evolutions. In: WST 2007, pp. 4–8 (2007)Google Scholar
  17. 17.
    Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. JAR 37(3), 155–203 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Gulwani, S., Tiwari, A.: Constraint-based approach for analysis of hybrid systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 190–203. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  19. 19.
    Hirokawa, N., Middeldorp, A.: Automating the dependency pair method. I&C 199(1-2), 172–199 (2005)MathSciNetzbMATHGoogle Scholar
  20. 20.
    Hofbauer, D., Waldmann, J.: Termination of string rewriting with matrix interpretations. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 328–342. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  21. 21.
    Hofbauer, D.: Termination proofs by context-dependent interpretations. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol. 2051, pp. 108–121. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  22. 22.
    Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean Termination Tool 2. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 295–304. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  23. 23.
    Kroening, D., Strichman, O.: Decision Procedures. Springer, Heidelberg (2008)zbMATHGoogle Scholar
  24. 24.
    Lucas, S.: Polynomials over the reals in proofs of termination: From theory to practice. TIA 39(3), 547–586 (2005)MathSciNetzbMATHGoogle Scholar
  25. 25.
    Lucas, S.: On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting. AAECC 17(1), 49–73 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    Lucas, S.: Practical use of polynomials over the reals in proofs of termination. In: PPDP 2007, pp. 39–50 (2007)Google Scholar
  27. 27.
    Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937–977 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  28. 28.
    Plaisted, D., Greenbaum, S.: A structure-preserving clause form translation. JSC 2(3), 293–304 (1986)MathSciNetzbMATHGoogle Scholar
  29. 29.
    Tarski, A.: A Decision Method for Elementary Algebra and Geometry, 2nd edn. University of California Press, Berkeley (1957)zbMATHGoogle Scholar
  30. 30.
    Zankl, H.: Lazy Termination Analysis. PhD thesis, University of Innsbruck (2009)Google Scholar
  31. 31.
    Zankl, H., Hirokawa, N., Middeldorp, A.: KBO orientability. JAR 43(2), 173–201 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  32. 32.
    Zantema, H.: Termination. In: TeReSe (ed.) Term Rewriting Systems, pp. 181–259. Cambridge University Press, Cambridge (2003)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Harald Zankl
    • 1
  • Aart Middeldorp
    • 1
  1. 1.Institute of Computer ScienceUniversity of InnsbruckAustria

Personalised recommendations