Abstract
We propose a novel, sound, and complete Simplex-based algorithm for solving linear inequalities over integers. Our algorithm, which can be viewed as a semantic generalization of the branch-and-bound technique, systematically discovers and excludes entire subspaces of the solution space containing no integer points. Our main insight is that by focusing on the defining constraints of a vertex, we can compute a proof of unsatisfiability for the intersection of the defining constraints and use this proof to systematically exclude subspaces of the feasible region with no integer points. We show experimentally that our technique significantly outperforms the top four competitors in the QF-LIA category of the SMT-COMP ’08 when solving linear inequalities over integers.
This work was supported by grants from NSF and DARPA (CCF-0430378, CNS-0716695).
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program, pp. 84–97. ACM Press, New York (1978)
Pugh, W.: The omega test: A fast and practical integer programming algorithm for dependence analysis. Communications of the ACM (1992)
Brinkmann, R., Drechsler, R.: RTL-datapath verification using integer linear programming. In: VLSI Design, pp. 741–746 (2002)
Amon, T., Borriello, G., Hu, T., Liu, J.: Symbolic timing verification of timing diagrams using presburger formulas. In: DAC 1997: Proceedings of the 34th annual conference on Design automation, pp. 226–231. ACM, New York (1997)
Dutertre, B., De Moura, L.: The yices SMT solver. Technical report, SRI International (2006)
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)
Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 298–302. Springer, Heidelberg (2007)
Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R.: The mathsat 4 SMT solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 299–303. Springer, Heidelberg (2008)
Bofill, M., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: The barcelogic SMT solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 294–298. Springer, Heidelberg (2008)
Dantzig, G.: Linear Programming and Extensions. Princeton University Press, Princeton (1963)
Ganesh, V., Berezin, S., Dill, D.: Deciding presburger arithmetic by model checking and comparisons with other methods. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 171–186. Springer, Heidelberg (2002)
Schrijver, A.: Theory of Linear and Integer Programming. J. Wiley & Sons, Chichester (1986)
Nemhauser, G.L., Wolsey, L.: Integer and Combinatorial Optimization. John Wiley & Sons, Chichester (1988)
Storjohann, A., Labahn, G.: Asymptotically fast computation of hermite normal forms of integer matrices. In: Proc. Int’l. Symp. on Symbolic and Algebraic Computation: ISSAC 1996, pp. 259–266. ACM Press, New York (1996)
http://gmplib.org/: Gnu mp bignum library
Cohen, H.: A Course in Computational Algebraic Number Theory. Graduate Texts in Mathematics. Springer, Heidelberg (1993)
Domich, P., Kannan, R., Trotter, J.L.: Hermite normal form computation using modulo determinant arithmetic. Mathematics of Operations Research 12(1), 50–59 (1987)
http://www.smtcomp.org : Smt-comp 2008
http://www.gnu.org/software/glpk/: Glpk (gnu linear programming kit)
http://lpsolve.sourceforge.net/5.5/: lp_solve reference guide
Jain, H., Clarke, E., Grumberg, O.: Efficient craig interpolation for linear diophantine (dis)equations and linear modular equations. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 254–267. Springer, Heidelberg (2008)
Golub, G.H., Van Loan, C.F.: Matrix Computations. JHU Press (1996)
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
Dillig, I., Dillig, T., Aiken, A. (2009). Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers. 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_20
Download citation
DOI: https://doi.org/10.1007/978-3-642-02658-4_20
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)