×

zbMATH — the first resource for mathematics

A complete and terminating approach to linear integer solving. (English) Zbl 1432.68597
Summary: We consider feasibility of linear integer problems in the context of verification systems such as SMT solvers or theorem provers. Although satisfiability of linear integer problems is decidable, many state-of-the-art implementations neglect termination in favor of efficiency. We present the calculus CutSat++ that is sound, terminating, complete, and leaves enough space for model assumptions and simplification rules in order to be efficient in practice. CutSat++ combines model-driven reasoning and quantifier elimination to the feasibility of linear integer problems.
MSC:
68W30 Symbolic computation and algebraic computation
68Q60 Specification and verification (program logics, model checking, etc.)
68R07 Computational aspects of satisfiability
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
90C10 Integer programming
Software:
MathSAT5; CVC4; Chaff; Yices; z3
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Alagi, G.; Weidenbach, C., NRCL - a model building approach to the Bernays-Schönfinkel fragment, (FroCoS. FroCoS, Lecture Notes in Computer Science, vol. 9322 (2015), Springer), 69-84 · Zbl 06688808
[2] Bachmair, L.; Ganzinger, H., On restrictions of ordered paramodulation with simplification, (CADE. CADE, Lecture Notes in Computer Science, vol. 449 (1990), Springer), 427-441
[3] Bachmair, L.; Ganzinger, H.; Waldmann, U., Refutational theorem proving for hierarchic first-order theories, Appl. Algebra Eng. Commun. Comput., 5, 193-212 (1994) · Zbl 0797.03008
[4] Barrett, C.; Conway, C.; Deters, M.; Hadarean, L.; Jovanović, D.; King, T.; Reynolds, A.; Tinelli, C., CVC4, (CAV. CAV, Lecture Notes in Computer Science, vol. 6806 (2011), Springer), 171-177
[5] Barrett, C.; Nieuwenhuis, R.; Oliveras, A.; Tinelli, C., Splitting on demand in SAT modulo theories, (LPAR. LPAR, Lecture Notes in Computer Science, vol. 4246 (2006), Springer), 512-526 · Zbl 1165.68480
[6] Baumgartner, P.; Waldmann, U., Hierarchic superposition with weak abstraction, (CADE. CADE, Lecture Notes in Computer Science, vol. 7898 (2013), Springer), 39-57 · Zbl 1381.03017
[7] Bayardo, R. J.; Schrag, R., Using CSP look-back techniques to solve exceptionally hard SAT instances, (CP. CP, Lecture Notes in Computer Science, vol. 1118 (1996), Springer), 46-60
[8] Berman, L., Precise bounds for Presburger arithmetic and the reals with addition, (FOCS (1977), IEEE Computer Society), 95-99
[9] Berman, L., The complexity of logical theories, Theor. Comput. Sci., 11, 71-77 (1980) · Zbl 0475.03017
[10] (Biere, A.; Heule, M.; van Maaren, H.; Walsh, T., Handbook of Satisfiability. Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185 (2009), IOS Press) · Zbl 1183.68568
[11] Bromberger, M.; Sturm, T.; Weidenbach, C., Linear integer arithmetic revisited, (CADE. CADE, Lecture Notes in Computer Science, vol. 9195 (2015), Springer), 623-637 · Zbl 1432.68596
[12] Caferra, R.; Leitsch, A.; Peltier, N., Automated Model Building, Applied Logic Series, vol. 31 (2004), Springer · Zbl 1085.03009
[13] Cimatti, A.; Griggio, A.; Schaafsma, B.; Sebastiani, R., The MathSAT5 SMT solver, (TACAS. TACAS, Lecture Notes in Computer Science, vol. 7795 (2013), Springer), 93-107 · Zbl 1381.68153
[14] Cooper, D. C., Theorem proving in arithmetic without multiplication, Machine Intelligence, 7, 91-99 (1972) · Zbl 0258.68046
[15] Dillig, I.; Dillig, T.; Aiken, A., Cuts from proofs: a complete and practical technique for solving linear inequalities over integers, (CAV. CAV, Lecture Notes in Computer Science, vol. 5643 (2009), Springer), 233-247 · Zbl 1242.65116
[16] Dragan, I.; Korovin, K.; Kovács, L.; Voronkov, A., Bound propagation for arithmetic reasoning in Vampire, (SYNASC (2013), IEEE Computer Society), 169-176
[17] Dutertre, B., Yices 2.2, (CAV. CAV, Lecture Notes in Computer Science, vol. 8559 (2014), Springer), 737-744
[18] Dutertre, B.; de Moura, L. M., A fast linear-arithmetic solver for DPLL(T), (CAV. CAV, Lecture Notes in Computer Science, vol. 4144 (2006), Springer), 81-94
[19] Ferrante, J.; Rackoff, C. W., A decision procedure for the first order theory of real addition with order, SIAM J. Comput., 4, 69-76 (1975) · Zbl 0294.02022
[20] Ferrante, J.; Rackoff, C. W., The Computational Complexity of Logical Theories, LNM, vol. 718 (1979), Springer · Zbl 0404.03028
[21] Fietzke, A.; Weidenbach, C., Superposition as a decision procedure for timed automata, Math. Comput. Sci., 6, 409-425 (2012) · Zbl 1262.68159
[22] Fischer, M. J.; Rabin, M., Super-Exponential Complexity of Presburger Arithmetic, SIAM-AMS Proceedings, vol. 7, 27-41 (1974) · Zbl 0319.68024
[23] Fürer, M., The complexity of Presburger arithmetic with bounded quantifier alternation depth, Theor. Comput. Sci., 18, 105-111 (1982) · Zbl 0484.03003
[24] von zur Gathen, J.; Sieveking, M., A bound on solutions of linear integer equalities and inequalities, Proc. Am. Math. Soc., 72, 155-158 (1978) · Zbl 0397.90071
[25] Grädel, E., The Complexity of Subclasses of Logical Theories (1987), Universität Basel, Ph.D. thesis
[26] Griggio, A., A practical approach to satisfiability modulo linear integer arithmetic, JSAT, 8, 1-27 (2012) · Zbl 1331.68207
[27] Jovanović, D.; de Moura, L. M., Cutting to the chase solving linear integer arithmetic, (CADE. CADE, Lecture Notes in Computer Science, vol. 6803 (2011), Springer), 338-353 · Zbl 1314.90054
[28] Jovanović, D.; de Moura, L. M., Cutting to the chase, J. Autom. Reason., 51, 79-108 (2013) · Zbl 1314.90053
[29] (Jünger, M.; Liebling, T. M.; Naddef, D.; Nemhauser, G. L.; Pulleyblank, W. R.; Reinelt, G.; Rinaldi, G.; Wolsey, L. A., 50 Years of Integer Programming 1958-2008 (2010), Springer) · Zbl 1181.90003
[30] Lasaruk, A.; Sturm, T., Weak quantifier elimination for the full linear theory of the integers. A uniform generalization of Presburger arithmetic, Appl. Algebra Eng. Commun. Comput., 18, 545-574 (2007) · Zbl 1154.68112
[31] Moskewicz, M. W.; Madigan, C. F.; Zhao, Y.; Zhang, L.; Malik, S., Chaff: engineering an efficient SAT solver, (DAC (2001), ACM), 530-535
[32] de Moura, L.; Bjørner, N., Z3: an efficient SMT solver, (TACAS. TACAS, Lecture Notes in Computer Science, vol. 4963 (2008), Springer), 337-340
[33] Nieuwenhuis, R.; Oliveras, A.; Tinelli, C., Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T), J. ACM, 53, 937-977 (2006) · Zbl 1326.68164
[34] Oppen, D. C., A \(2^{2^{2^{p n}}}\) upper bound on the complexity of Presburger arithmetic, J. Comput. Syst. Sci., 16, 323-332 (1978) · Zbl 0381.03021
[35] Papadimitriou, C. H., On the complexity of integer programming, J. ACM, 28, 765-768 (1981) · Zbl 0468.68050
[36] Piskac, R.; de Moura, L. M.; Bjørner, N., Deciding effectively propositional logic using DPLL and substitution sets, J. Autom. Reason., 44, 401-424 (2010) · Zbl 1197.03011
[37] Presburger, M., Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt, (Comptes Rendus du premier congres de Mathematiciens des Pays Slaves. Comptes Rendus du premier congres de Mathematiciens des Pays Slaves, Warsaw, Poland (1929)), 92-101 · JFM 56.0825.04
[38] Silva, J. P.M.; Sakallah, K. A., Grasp - a new search algorithm for satisfiability, (ICCAD (1996), IEEE Computer Society Press), 220-227
[39] Weidenbach, C., Automated reasoning building blocks, (Correct System Design. Correct System Design, Lecture Notes in Computer Science, vol. 9360 (2015), Springer), 172-188 · Zbl 1444.68289
[40] Weispfenning, V., The complexity of almost linear diophantine problems, J. Symb. Comput., 10, 395-403 (1990) · Zbl 0716.68050
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.