Journal of Automated Reasoning

, Volume 51, Issue 1, pp 79–108

Cutting to the Chase

Solving Linear Integer Arithmetic
Article

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.

Keywords

Linear arithmetic SMT SAT DPLL Linear programming Integer arithmetic 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Achterberg, T.: SCIP: Solving constraint integer programs. PhD thesis, TU Berlin (2007)Google Scholar
  2. 2.
    Achterberg, T., Koch, T., Martin, A.: MIPLIB 2003. Oper. Res. Lett. 34(4), 361–372 (2006)CrossRefGoogle 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)Google Scholar
  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)Google Scholar
  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)CrossRefGoogle Scholar
  7. 7.
    Chvátal, V. Edmonds polytopes and a hierarchy of combinatorial problems. Discrete Math. 4(4), 305–337 (1973)MathSciNetMATHCrossRefGoogle 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)Google Scholar
  10. 10.
    Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 397 (1962)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM (JACM) 7(3), 201–215 (1960)MathSciNetMATHCrossRefGoogle 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)Google Scholar
  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)Google Scholar
  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)Google Scholar
  15. 15.
    Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: CAV, LNCS, pp. 81–94 (2006)Google Scholar
  16. 16.
    Gomory, R.E.: Outline of an algorithm for integer solutions to linear programs. Bull. Am. Math. Soc. 64(5), 275–278 (1958)MathSciNetMATHCrossRefGoogle Scholar
  17. 17.
    Griggio, A.: A practical approach to SMT(LA(Z)). In: SMT Workshop (2010)Google Scholar
  18. 18.
    Korovin, K., Tsiskaridze, N., Voronkov, A.: Conflict resolution. In: Principles and Practice of Constraint Programming (2009)Google Scholar
  19. 19.
    McMillan, K.L., Kuehlmann, A., Sagiv, M.: Generalizing DPLL to richer logics. In: CAV (2009)Google Scholar
  20. 20.
    Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: DAC (2001)Google Scholar
  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)MathSciNetCrossRefGoogle Scholar
  22. 22.
    Papadimitriou, C.H.: On the complexity of integer programming. J. ACM 28(4), 765–768 (1981)MathSciNetMATHCrossRefGoogle 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)Google Scholar
  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)Google Scholar
  25. 25.
    Silva, J.P.M., Sakallah, K.A.: GRASP—a new search algorithm for satisfiability. In: ICCAD (1997)Google Scholar
  26. 26.
    Wolsey, L.A., Nemhauser, G.L.: Integer and Combinatorial Optimization. Wiley, New York (1999)MATHGoogle Scholar

Copyright information

© Springer Science+Business Media Dordrecht 2013

Authors and Affiliations

  1. 1.New York UniversityNew YorkUSA
  2. 2.Microsoft ResearchRedmondUSA

Personalised recommendations