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.
This work was partially funded by the ANR ARPEGE project “ASOPT”.
Chapter PDF
Similar content being viewed by others
References
Applegate, D., Cook, W., Dash, S., Espinoza, D.: Exact solutions to linear programming problems. Oper. Res. Lett. 35(6), 693–699 (2007)
Dantzig, G.: Linear Programming and Extensions. Princeton University Press, Princeton (1998)
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)
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)
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)
Dutertre, B., de Moura, L.: Integrating simplex with DPLL(T). Technical Report SRI-CSL-06-01, SRI International (May 2006)
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)
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)
Free Software Foundation. GNU Linear Programming Kit Reference Manual, version 4.34 (December 2008)
Free Software Foundation. GNU MP The GNU Multiple Precision Arithmetic Library, 4.2.4 edition (September 2008)
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)
Hales, T.C.: Some algorithms arising in the proof of the Kepler conjecture, arXiv:math/0205209v1
Hales, T.C.: A proof of the Kepler conjecture. Ann. Math. 162, 1065–1185 (2005)
Koch, T.: The final NETLIB-LP results. Op. Res. Letters 32(2), 138–142 (2004)
Schrijver, A.: Theory of Linear and Integer Programming. Wiley, Chichester (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Monniaux, D. (2009). On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure. In: Bouajjani, A., Maler, O. (eds) Computer Aided Verification. CAV 2009. Lecture Notes in Computer Science, vol 5643. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02658-4_42
Download citation
DOI: https://doi.org/10.1007/978-3-642-02658-4_42
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02657-7
Online ISBN: 978-3-642-02658-4
eBook Packages: Computer ScienceComputer Science (R0)