On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure
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.
- 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
- 6.Dutertre, B., de Moura, L.: Integrating simplex with DPLL(T). Technical Report SRI-CSL-06-01, SRI International (May 2006)Google Scholar
- 9.Free Software Foundation. GNU Linear Programming Kit Reference Manual, version 4.34 (December 2008)Google Scholar
- 10.Free Software Foundation. GNU MP The GNU Multiple Precision Arithmetic Library, 4.2.4 edition (September 2008)Google Scholar
- 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.Hales, T.C.: Some algorithms arising in the proof of the Kepler conjecture, arXiv:math/0205209v1Google Scholar