Advertisement

On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure

  • David Monniaux
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5643)

Abstract

We consider the decision problem for quantifier-free formulas whose atoms are linear inequalities interpreted over the reals or rationals. This problem may be decided using satisfiability modulo theory (SMT), using a mixture of a SAT solver and a simplex-based decision procedure for conjunctions. State-of-the-art SMT solvers use simplex implementations over rational numbers, which perform well for typical problems arising from model-checking and program analysis (sparse inequalities, small coefficients) but are slow for other applications (denser problems, larger coefficients).

We propose a simple preprocessing phase that can be adapted to existing SMT solvers and that may be optionally triggered. Despite using floating-point computations, our method is sound and complete — it merely affects efficiency. We implemented the method and provide benchmarks showing that this change brings a naive and slow decision procedure (“textbook simplex” with rational numbers) up to the efficiency of recent SMT solvers, over test cases arising from model-checking, and makes it definitely faster than state-of-the-art SMT solvers on dense examples.

References

  1. 1.
    Applegate, D., Cook, W., Dash, S., Espinoza, D.: Exact solutions to linear programming problems. Oper. Res. Lett. 35(6), 693–699 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Dantzig, G.: Linear Programming and Extensions. Princeton University Press, Princeton (1998)zbMATHGoogle Scholar
  3. 3.
    de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  4. 4.
    Dhiflaoui, M., Funke, S., Kwappik, C., Mehlhorn, K., Seel, M., Schömer, E., Schulte, R., Weber, D.: Certifying and repairing solutions to large LPs: how good are LP-solvers? In: SODA 2003: Proceedings of the fourteenth annual ACM-SIAM symposium on Discrete algorithms, pp. 255–256. SIAM, Philadelphia (2003)Google Scholar
  5. 5.
    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
  6. 6.
    Dutertre, B., de Moura, L.: Integrating simplex with DPLL(T). Technical Report SRI-CSL-06-01, SRI International (May 2006)Google Scholar
  7. 7.
    Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  8. 8.
    Faure, G., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: SAT modulo the theory of linear arithmetic: Exact, inexact and commercial solvers. In: Kleine Büning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 77–90. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  9. 9.
    Free Software Foundation. GNU Linear Programming Kit Reference Manual, version 4.34 (December 2008)Google Scholar
  10. 10.
    Free Software Foundation. GNU MP The GNU Multiple Precision Arithmetic Library, 4.2.4 edition (September 2008)Google Scholar
  11. 11.
    Gärtner, B.: Exact arithmetic at low cost — a case study in linear programming. In: SODA 1998: Proceedings of the ninth annual ACM-SIAM symposium on Discrete algorithms, pp. 157–166. SIAM, Philadelphia (1998)Google Scholar
  12. 12.
    Hales, T.C.: Some algorithms arising in the proof of the Kepler conjecture, arXiv:math/0205209v1Google Scholar
  13. 13.
    Hales, T.C.: A proof of the Kepler conjecture. Ann. Math. 162, 1065–1185 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Koch, T.: The final NETLIB-LP results. Op. Res. Letters 32(2), 138–142 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Schrijver, A.: Theory of Linear and Integer Programming. Wiley, Chichester (1998)zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • David Monniaux
    • 1
  1. 1.VerimagFrance

Personalised recommendations