×

New techniques for linear arithmetic: cubes and equalities. (English) Zbl 1377.68128

Summary: We present several new techniques for linear arithmetic constraint solving. They are all based on the linear cube transformation, a method presented here, which allows us to efficiently determine whether a system of linear arithmetic constraints contains a hypercube of a given edge length. Our first findings based on this transformation are two sound tests that find integer solutions for linear arithmetic constraints. While many complete methods search along the problem surface for a solution, these tests use cubes to explore the interior of the problems. The tests are especially efficient for constraints with a large number of integer solutions, e.g., those with infinite lattice width. Inside the SMT-LIB benchmarks, we have found almost one thousand problem instances with infinite lattice width. Experimental results confirm that our tests are superior on these instances compared to several state-of-the-art SMT solvers. We also discovered that the linear cube transformation can be used to investigate the equalities implied by a system of linear arithmetic constraints. For this purpose, we developed a method that computes a basis for all implied equalities, i.e., a finite representation of all equalities implied by the linear arithmetic constraints. The equality basis has several applications. For instance, it allows us to verify whether a system of linear arithmetic constraints implies a given equality. This is valuable in the context of Nelson-Oppen style combinations of theories.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

Software:

z3; Yices; MathSAT5; CVC4

References:

[1] Barrett C, Conway C, Deters M, Hadarean L, Jovanović D, King T, Reynolds A, Tinelli C (2011) CVC4. In: CAV, LNCS, vol 6806, pp 171-177 · Zbl 0176.49902
[2] Beale EML (1954) An alternative method for linear programming, vol 50, issue 4, pp 513-523 · Zbl 0056.13705
[3] Bjørner N (1999) Integrating decision procedures for temporal verification. Ph.D. thesis, Stanford, CA, USA · Zbl 0787.03021
[4] Bobot F, Conchon S, Contejean E, Iguernelala M, Mahboubi A, Mebsout A, Melquiond G (2012) A simplex-based extension of Fourier-Motzkin for solving linear integer arithmetic. In: IJCAR 2012, LNCS, vol 7364, pp 67-81 · Zbl 1358.68249
[5] Boyd S, Vandenberghe L (2004) Convex optimization. Cambridge University Press, Cambridge · Zbl 1058.90049 · doi:10.1017/CBO9780511804441
[6] Bromberger M, Sturm T, Weidenbach C (2015) Linear integer arithmetic revisited. In: CADE-25, LNCS, vol 9195, pp 623-637 · Zbl 1432.68596
[7] Bromberger M, Weidenbach C (2016) Computing a complete basis for equalities implied by a system of LRA constraints. In: SMT 2016, pp 15-30 · Zbl 0468.68050
[8] Bromberger M, Weidenbach C (2016) Fast cube tests for lia constraint solving. In: IJCAR 2016, LNCS, vol 9706 · Zbl 1475.68337
[9] Bruttomesso R, Cimatti A, Franzen A, Griggio A, Sebastiani R (2009) Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis. AMAI 55(1):63-99 · Zbl 1192.68627
[10] Cimatti A, Griggio A, Schaafsma B, Sebastiani R (2013) The MathSAT5 SMT Solver. In: TACAS, LNCS, vol 7795 · Zbl 1381.68153
[11] Dillig I, Dillig T, Aiken A (2009) Cuts from proofs: a complete and practical technique for solving linear inequalities over integers. In: CAV, LNCS, vol 5643, pp 233-247 · Zbl 1242.65116
[12] Dolzmann A, Sturm T, Weispfenning V (1999) Real quantifier elimination in practice. In: Algorithmic algebra and number theory. Springer, pp 221-247 · Zbl 0934.68130
[13] Dutertre B (2014) Yices 2.2. In: CAV 2014, LNCS, vol 8559
[14] Dutertre B, de Moura, L (2006) A fast linear-arithmetic solver for DPLL(T). In: CAV, LNCS, vol. 4144, pp. 81-94 (2006). Extended version: Integrating simplex with DPLL(T). Technical report, CSL, SRI International
[15] Faure G, Nieuwenhuis R, Oliveras A, Rodríguez-Carbonell E (2008) Sat modulo the theory of linear arithmetic: exact, inexact and commercial solvers. In: SAT 2008, LNCS, vol 4996, pp 77-90 · Zbl 1138.68537
[16] Griggio A (2012) A practical approach to satisfiability modulo linear integer arithmetic. JSAT 8(1/2):1-27 · Zbl 1331.68207
[17] Hillier FS (1969) Efficient heuristic procedures for integer linear programming with an interior. Oper Res 17(4):600-637 · Zbl 0176.49902 · doi:10.1287/opre.17.4.600
[18] Jovanović D, de Moura L (2013) Cutting to the chase. JAR 51(1):79-108 · Zbl 1314.90053 · doi:10.1007/s10817-013-9281-x
[19] Jünger M, Liebling TM, Naddef D, Nemhauser GL, Pulleyblank WR, Reinelt G, Rinaldi G, Wolsey LA (eds) (2010) 50 years of integer programming 1958-2008 · Zbl 1331.68207
[20] Kannan R, Lovász L (1986) Covering minima and lattice point free convex bodies. FSTTCS, LNCS, vol 241, pp 193-213 · Zbl 0621.10021
[21] Karmarkar N (1984) A new polynomial-time algorithm for linear programming. Combinatorica 4(4):373-396 · Zbl 0557.90065 · doi:10.1007/BF02579150
[22] Lemke CE (1954) The dual method of solving the linear programming problem. Nav Res Logist Quart 1(1):36-47 · Zbl 0128.39605 · doi:10.1002/nav.3800010107
[23] Loos R, Weispfenning V (1993) Applying linear quantifier elimination. Comput J 36(5):450-462 · Zbl 0787.03021 · doi:10.1093/comjnl/36.5.450
[24] de Moura L, Bjørner N (2008) Z3: an efficient SMT solver. In: Tools and algorithms for the construction and analysis of systems, LNCS, vol 4963, pp 337-340 · Zbl 0527.90066
[25] Papadimitriou CH (1981) On the complexity of integer programming. J ACM 28(4):765-768 · Zbl 0468.68050 · doi:10.1145/322276.322287
[26] Pugh W (1991) The omega test: a fast and practical integer programming algorithm for dependence analysis. In: Supercomputing 1991, Supercomputing ’91. ACM, pp 4-13 · Zbl 1034.68508
[27] Refalo P (1998) Approaches to the incremental detection of implicit equalities with the revised simplex method. In: PLILP 1998, LNCS, vol 1490, pp 481-496 · Zbl 1034.68508
[28] Rueß H, Shankar N (2004) Solving linear arithmetic constraints. Technical report, SRI International, Computer Science Laboratory
[29] Schrijver A (1986) Theory of linear and integer programming. Wiley, New York · Zbl 0665.90063
[30] Sturm T (1996) Real quadratic quantifier elimination in risa/asir. Technical report, ISIS-RM-5E, Fujitsu Laboratories Ltd · Zbl 0557.90065
[31] Telgen J (1983) Identifying redundant constraints and implicit equalities in systems of linear constraints. Manag Sci 29(10):1209-1222 · Zbl 0527.90066 · doi:10.1287/mnsc.29.10.1209
[32] Van Hentenryck P, Graf T (1992) Standard forms for rational linear arithmetic in constraint logic programming. AMAI 5(2):303-319 · Zbl 1034.68508
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.