Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers

  • Isil Dillig
  • Thomas Dillig
  • Alex Aiken
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5643)


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.


Linear Inequality Integer Solution Valid Inequality Integer Point Convex Polyhedron 
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.


  1. 1.
    Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program, pp. 84–97. ACM Press, New York (1978)Google Scholar
  2. 2.
    Pugh, W.: The omega test: A fast and practical integer programming algorithm for dependence analysis. Communications of the ACM (1992)Google Scholar
  3. 3.
    Brinkmann, R., Drechsler, R.: RTL-datapath verification using integer linear programming. In: VLSI Design, pp. 741–746 (2002)Google Scholar
  4. 4.
    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)Google Scholar
  5. 5.
    Dutertre, B., De Moura, L.: The yices SMT solver. Technical report, SRI International (2006)Google Scholar
  6. 6.
    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
  7. 7.
    Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 298–302. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  8. 8.
    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)CrossRefGoogle Scholar
  9. 9.
    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)CrossRefGoogle Scholar
  10. 10.
    Dantzig, G.: Linear Programming and Extensions. Princeton University Press, Princeton (1963)CrossRefzbMATHGoogle Scholar
  11. 11.
    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)CrossRefGoogle Scholar
  12. 12.
    Schrijver, A.: Theory of Linear and Integer Programming. J. Wiley & Sons, Chichester (1986)zbMATHGoogle Scholar
  13. 13.
    Nemhauser, G.L., Wolsey, L.: Integer and Combinatorial Optimization. John Wiley & Sons, Chichester (1988)CrossRefzbMATHGoogle Scholar
  14. 14.
    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)CrossRefGoogle Scholar
  15. 15. Gnu mp bignum library
  16. 16.
    Cohen, H.: A Course in Computational Algebraic Number Theory. Graduate Texts in Mathematics. Springer, Heidelberg (1993)CrossRefzbMATHGoogle Scholar
  17. 17.
    Domich, P., Kannan, R., Trotter, J.L.: Hermite normal form computation using modulo determinant arithmetic. Mathematics of Operations Research 12(1), 50–59 (1987)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18. Smt-comp 2008
  19. 19. Glpk (gnu linear programming kit)
  20. 20. lp_solve reference guide
  21. 21.
  22. 22.
    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)CrossRefGoogle Scholar
  23. 23.
    Golub, G.H., Van Loan, C.F.: Matrix Computations. JHU Press (1996)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Isil Dillig
    • 1
  • Thomas Dillig
    • 1
  • Alex Aiken
    • 1
  1. 1.Department of Computer ScienceStanford UniversityUSA

Personalised recommendations