zbMATH — the first resource for mathematics

Cutting to the chase. Solving linear integer arithmetic. (English) Zbl 1314.90053
Summary: 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.

90C10 Integer programming
90C05 Linear programming
Full Text: DOI
[1] Achterberg, T.: SCIP: Solving constraint integer programs. PhD thesis, TU Berlin (2007) · Zbl 1171.90476
[2] Achterberg, T; Koch, T; Martin, A; MIPLIB, Miplib 2003, Oper. Res. Lett., 34, 361-372, (2003) · Zbl 1133.90300
[3] Barth, P.: A Davis-Putnam Based Enumeration Algorithm for Linear Pseudo-Boolean Optimization. Research Report MPI-I-95-2-003, Saarbrücken (1995) · Zbl 0212.34203
[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) · Zbl 1031.68584
[5] Berre, D; Parrain, A, The sat4j library, release 2.2 system description, JSAT, 7, 59-64, (2010)
[6] Chai, D; Kuehlmann, A, A fast pseudo-Boolean constraint solver, IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst., 24, 305-317, (2005)
[7] Chvátal, V, Edmonds polytopes and a hierarchy of combinatorial problems, Discrete Math., 4, 305-337, (1973) · Zbl 0253.05131
[8] Cooper, DC, Heorem proving in arithmetic without multiplication, Mach. intell., 7, 300, (1972)
[9] Cotton, S.: Natural domain SMT: a preliminary assessment. In: FORMATS (2010) · Zbl 1290.68112
[10] Davis, M; Logemann, G; Loveland, D, A machine program for theorem-proving, Commun. ACM, 5, 397, (1962) · Zbl 0217.54002
[11] Davis, M; Putnam, H, A computing procedure for quantification theory, J. ACM (JACM), 7, 201-215, (1960) · Zbl 0212.34203
[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] 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) · Zbl 1426.68251
[14] Dillig, I., Dillig, T., Aiken, A.: Cuts from proofs: a complete and practical technique for solving linear inequalities over integers. In: CAV (2009) · Zbl 1242.65116
[15] Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: CAV, LNCS, pp. 81-94 (2006)
[16] Gomory, RE, Outline of an algorithm for integer solutions to linear programs, Bull. Am. Math. Soc., 64, 275-278, (1958) · Zbl 0085.35807
[17] Griggio, A.: A practical approach to SMT(LA(Z)). In: SMT Workshop (2010)
[18] Korovin, K., Tsiskaridze, N., Voronkov, A.: Conflict resolution. In: Principles and Practice of Constraint Programming (2009) · Zbl 1336.68236
[19] McMillan, K.L., Kuehlmann, A., Sagiv, M.: Generalizing DPLL to richer logics. In: CAV (2009) · Zbl 1242.68282
[20] Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: DAC (2001) · Zbl 1133.90300
[21] Nieuwenhuis, R; Oliveras, A; Tinelli, C, Solving SAT and SAT modulo theories: from an abstract DPLL procedure to DPLL(T), J. ACM, 53, 937-977, (2006) · Zbl 1326.68164
[22] Papadimitriou, CH, On the complexity of integer programming, J. ACM, 28, 765-768, (1981) · Zbl 0468.68050
[23] Pugh, W.: The omega test: a fast and practical integer programming algorithm for dependence analysis. In: ACM/IEEE Conference on Supercomputing (1991)
[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) · Zbl 1125.03010
[25] Silva, J.P.M., Sakallah, K.A.: GRASP—a new search algorithm for satisfiability. In: ICCAD (1997) · Zbl 1392.68388
[26] Wolsey, L.A., Nemhauser, G.L.: Integer and Combinatorial Optimization. Wiley, New York (1999) · Zbl 0944.90001
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.