Skip to main content

Cutting to the Chase

Solving Linear Integer Arithmetic

Abstract

We describe a new algorithm for solving linear integer programming problems. The algorithm performs a DPLL style search for a feasible assignment, while using a novel cut procedure to guide the search away from the conflicting states.

This is a preview of subscription content, access via your institution.

References

  1. 1.

    Achterberg, T.: SCIP: Solving constraint integer programs. PhD thesis, TU Berlin (2007)

  2. 2.

    Achterberg, T., Koch, T., Martin, A.: MIPLIB 2003. Oper. Res. Lett. 34(4), 361–372 (2006)

    Article  Google Scholar 

  3. 3.

    Barth, P.: A Davis–Putnam Based Enumeration Algorithm for Linear Pseudo-Boolean Optimization. Research Report MPI-I-95-2-003, Saarbrücken (1995)

  4. 4.

    Berezin, S., Ganesh, V., Dill, D.L.: An online proof-producing decision procedure for mixed-integer linear arithmetic. In: Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 2619, pp. 521–536. Springer (2003)

  5. 5.

    Le Berre, D., Parrain, A.: The Sat4j library, release 2.2 system description. JSAT 7, 59–64 (2010)

    Google Scholar 

  6. 6.

    Chai, D., Kuehlmann, A.: A fast pseudo-boolean constraint solver. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 24(3), 305–317 (2005)

    Article  Google Scholar 

  7. 7.

    Chvátal, V. Edmonds polytopes and a hierarchy of combinatorial problems. Discrete Math. 4(4), 305–337 (1973)

    MathSciNet  MATH  Article  Google Scholar 

  8. 8.

    Cooper, D.C. Theorem proving in arithmetic without multiplication. Mach. intell. 7(91–99), 300 (1972)

    Google Scholar 

  9. 9.

    Cotton, S.: Natural domain SMT: a preliminary assessment. In: FORMATS (2010)

  10. 10.

    Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 397 (1962)

    MathSciNet  Article  Google Scholar 

  11. 11.

    Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM (JACM) 7(3), 201–215 (1960)

    MathSciNet  MATH  Article  Google Scholar 

  12. 12.

    de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: TACAS 2008, Budapest, Hungary. LNCS, vol. 4963, p. 337. Springer (2008)

  13. 13.

    de Moura, L., Jovanović, D.: A model-constructing satisfiability calculus. In: Verification, Model Checking, and Abstract Interpretation. LNCS, vol. 7737, pp. 1–12. Springer (2013)

  14. 14.

    Dillig, I., Dillig, T., Aiken, A.: Cuts from proofs: a complete and practical technique for solving linear inequalities over integers. In: CAV (2009)

  15. 15.

    Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: CAV, LNCS, pp. 81–94 (2006)

  16. 16.

    Gomory, R.E.: Outline of an algorithm for integer solutions to linear programs. Bull. Am. Math. Soc. 64(5), 275–278 (1958)

    MathSciNet  MATH  Article  Google Scholar 

  17. 17.

    Griggio, A.: A practical approach to SMT(LA(Z)). In: SMT Workshop (2010)

  18. 18.

    Korovin, K., Tsiskaridze, N., Voronkov, A.: Conflict resolution. In: Principles and Practice of Constraint Programming (2009)

  19. 19.

    McMillan, K.L., Kuehlmann, A., Sagiv, M.: Generalizing DPLL to richer logics. In: CAV (2009)

  20. 20.

    Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: DAC (2001)

  21. 21.

    Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract DPLL procedure to DPLL(T). J. ACM 53(6), 937–977 (2006)

    MathSciNet  Article  Google Scholar 

  22. 22.

    Papadimitriou, C.H.: On the complexity of integer programming. J. ACM 28(4), 765–768 (1981)

    MathSciNet  MATH  Article  Google Scholar 

  23. 23.

    Pugh, W.: The omega test: a fast and practical integer programming algorithm for dependence analysis. In: ACM/IEEE Conference on Supercomputing (1991)

  24. 24.

    Seshia, S.A., Bryant, R.E.: Deciding quantifier-free Presburger formulas using parameterized solution bounds. In: Logic in Computer Science, pp. 100–109. IEEE (2004)

  25. 25.

    Silva, J.P.M., Sakallah, K.A.: GRASP—a new search algorithm for satisfiability. In: ICCAD (1997)

  26. 26.

    Wolsey, L.A., Nemhauser, G.L.: Integer and Combinatorial Optimization. Wiley, New York (1999)

    MATH  Google Scholar 

Download references

Author information

Affiliations

Authors

Corresponding author

Correspondence to Dejan Jovanović.

Rights and permissions

Reprints and Permissions

About this article

Cite this article

Jovanović, D., de Moura, L. Cutting to the Chase. J Autom Reasoning 51, 79–108 (2013). https://doi.org/10.1007/s10817-013-9281-x

Download citation

Keywords

  • Linear arithmetic
  • SMT
  • SAT
  • DPLL
  • Linear programming
  • Integer arithmetic