Computing a Complete Basis for Equalities Implied by a System of LRA Constraints Martin Bromberger1,2 and Christoph Weidenbach1 1 Max Planck Institute for Informatics, Saarbrücken, Germany {mbromber,weidenb}@mpi-inf.mpg.de 2 Graduate School of Computer Science, Saarbrücken, Germany Abstract We present three new methods that investigate the equalities implied by a system of linear arithmetic constraints. Implied equalities can be used to simplify linear arithmetic constraints and are valuable in the context of Nelson-Oppen style combinations of theories. The first method efficiently checks whether a system of linear arithmetic constraints implies an equality at all. In case the system does, the method also returns a valid equality as an explanation. The second method uses the first method to compute a basis for all implied equalities, i.e., a finite representation of all equalities implied by the linear arithmetic constraints. The third method uses the second method to check efficiently whether a system of linear arithmetic constraints implies a given equality. 1 Introduction Polyhedra and the systems of linear arithmetic constraints Ax ≤ b defining them have a vast number of theoretical and real-world applications [2, 9]. It is, therefore, no surprise that the theory of linear arithmetic is also one of the most popular and best investigated theories for satisfiability modulo theories (SMT) solving [5, 6, 7]. Equalities are a special instance of linear arithmetic constraints. They are useful in simplifying systems of arithmetic constraints [7], and they are essential for the Nelson-Oppen style combinations of theories [4]. However, they are also an obstacle for our fast cube tests [3], which find integer solutions by exploring the interior of a polyhedron with cubes. If a system of linear arithmetic constraints Ax ≤ b implies an equality, then it has only a surface and no interior; so our cube tests cannot explore an interior and will certainly fail. In order to expand the applicability of our cube tests, we are interested in methods that find, isolate, and eliminate implied equalities from systems of linear arithmetic constraints. We mentioned such methods already in [3], but we will fully present three methods here for the first time. In Section 3, we present the first method, which efficiently checks whether a system of linear arithmetic constraints Ax ≤ b implies an equality at all. We can detect the existence of an implied equality by searching for a cube contained in Ax ≤ b. If the maximal edge length of such a cube is 0, there exists an implied equality (Lemma 6). This test can be further simplified. By turning all inequalities in Ax ≤ b into strict inequalities Ax < b, the interior of the original polyhedron remains while the surface disappears. If Ax < b is unsatisfiable, then Ax ≤ b has no interior and implies an equality (Lemma 7). Based on an explanation of unsatisfiability for Ax < b, the method generates an implied equality as an explanation (Lemma 8). The second method, introduced in Section 4, consists of the algorithm EqualityBasis(Ax ≤ b) that computes a basis for all implied equalities, i.e., a finite representation of all equalities implied by the satisfiable linear arithmetic constraints Ax ≤ b. For this purpose, the algorithm iteratively applies the first method to find, collect, and eliminate equalities from Ax ≤ b. When Ax ≤ b contains no more equalities, then the collected equalities represent an equality basis Dx = c, i.e., any implied equality can be obtained by a linear combination from Dx = c. The equality basis has many applications. In combination with the algorithm Subst(Dx = c, Ax ≤ b), Figure 3, it eliminates all equalities implied by Dx = c from Ax ≤ b, which results in a system of inequalities with an interior and, therefore, improves the applicability of our cube tests. Together with a diophantine equation handler [7], the equality basis is useful for simplifying linear integer constraint systems. Note that simplifying Ax ≤ b with the equality basis is only useful if Ax ≤ b is satisfiable and if we want to perform subsequent computations on Ax ≤ b, e.g., maximizing/minimizing multiple cost functions for Ax ≤ b or as an intermediate step towards determining an integer solution for Ax ≤ b. Finally, in Section 4 we introduce an efficient method testing whether a system of linear arithmetic constraints implies a given equality. The method relies on an equality basis Dx = c of Ax ≤ b where the Subst algorithm efficiently explores implication of a given equality. For the Nelson-Oppen style combination of theories inside an SMT solver [4], each theory solver has to return all valid equations between variables in its theory. Linear arithmetic theory solvers sometimes guess these equations based on one satisfiable assignment. Then the equations are transferred according to the Nelson-Oppen method without verification. This leads to a backtrack of the combination procedure in case the guess was wrong and eventually led to a conflict. With the availability of our algorithm Subst, the guesses can be verified directly and efficiently, even before suggestion. Therefore, the method helps the theory solver in avoiding any conflicts due to wrong guesses together with the overhead of the entailed backtracking. This comes at the price of computing once and for all an equality basis, where an already found satisfying assignment has further potential for simplification, see Appendix B. 2 Preliminaries While the difference between matrices, vectors, and their components is always clear in context, we generally use upper case letters for matrices (e.g., A), lower case letters for vectors (e.g., x), and lower case letters with an index i or j (e.g., bi , xj ) as components of the associated vector at position i or j, respectively. The only exceptions are the row vectors aTi = (ai1 , . . . , ain ) of a matrix A = (a1 , . . . , am )T , which already contain an index i that indicates the row’s position inside A. In order to save space, we write vectors only implicitly as columns via the transpose ( )T operator, which turns all rows (b1 , . . . , bm ) into columns (b1 , . . . , bm )T and vice versa. We will also abbreviate (0, . . . , 0)T as 0. Likewise, we will abbreviate (1, . . . , 1)T as 1. In the context of SMT theory solvers, we have to deal with inequalities aTi x ≤ bi and strict inequalities aTi x < bi , where ai ∈ Qn and bi ∈ Q. We will model strict inequalities as non-strict inequalities by generalizing the field Q for our inequality bounds bi to Qδ . Lemma 1 ([5]). Let ai ∈ Qn and bi ∈ Q. Then, a set of linear arithmetic constraints S containing strict inequalities S 0 = {aT1 x < b1 , . . . , aTm x < bm } is satisfiable iff there exists a rational number δ > 0 such that for all δ 0 with 0 < δ 0 ≤ δ, Sδ0 = (S ∪ Sδ0 0 ) \ S 0 is satisfiable, where Sδ0 0 = {aT1 x ≤ b1 − δ 0 , . . . , aTm x ≤ bm − δ 0 }. As a result of this observation, δ is expressed symbolically as an infinitesimal parameter [5]. This leads to the ordered vector field Qδ that has pairs of rationals as elements (p, q) ∈ Q × Q, representing p + qδ, with the following operations: (p1 , q1 ) + (p2 , q2 ) ≡ (p1 + p2 , q1 + q2 ) a · (p, q) ≡ (a · p, a · q) (p1 , q1 ) ≤ (p2 , q2 ) ≡ (p1 < p2 ) ∨ (p1 = p2 ∧ q1 ≤ q2 ) (p1 , q1 ) < (p2 , q2 ) ≡ (p1 < p2 ) ∨ (p1 = p2 ∧ q1 < q2 ) , where a ∈ Q [5]. Now we can represent aTi x < bi by aTi x ≤ bi − δ, where ai ∈ Qn and bi ∈ Q. Note, however, that aTi x < bi cannot be represented by aTi x ≤ bi − δ if ai ∈ Qn and bi ∈ Qδ . To do so, we would have to introduce a second infinitesimal and extend Qδ to Q × Q × Q. For the remainder of the paper, we will also abbreviate with bδi that we have turned the bound bi = (pi , qi ) ∈ Qδ into a strict bound bδi = (pi , −1) ∈ Qδ . In this paper, we treat polyhedra and their definitions through a system of inequalities Ax ≤ b as interchangeable. For such a system of inequalities, the row coefficients are given by A = (a1 , . . . , am )T ∈ Qm×n , the variables are given by x = (x1 , . . . , xn )T , and the inequality bounds are given by b = (b1 , . . . , bm )T ∈ Qm δ . To avoid misuse of the δ infinitesimal, we also require that the δ-coefficient qi in bi = pi + qi δ is either 0 or −1. Moreover, we assume that any constant rows ai = 0 have been eliminated from our system as a preprocessing step. This is a trivial task and eliminates some unnecessarily complicated corner cases. Note that the system of inequalities Ax ≤ b is just an abbreviation for the set of inequalities {aT1 x ≤ b1 , . . . , aTm x ≤ bm }. Since Ax ≤ b and A0 x ≤ b0 are just sets, we can write their combination as (Ax ≤ b)∪(A0 x ≤ b0 ). A special system of inequalities is a system of equations Dx = c, which is equivalent to the combined system of inequalities (Dx ≤ c) ∪ (−Dx ≤ −c). For such a system of equalities, the row coefficients are given by D = (d1 , . . . , dm )T ∈ Qm×n , the variables are given by x = (x1 , . . . , xn )T , and the equality bounds are given by c = (c1 , . . . , cm )T ∈ Qm . We denote by P A b = {x ∈ Q n : Ax ≤ b} the set of rational solutions to the system of inequalities Ax ≤ b and, therefore, the points inside the polyhedron. Similarly, we de- note by Cen (z) = x ∈ Qn : ∀j ∈ 1, . . . , n. |xj − zj | ≤ 2e the set of points contained in the n-dimensional hypercube that is parallel to the coordinate axes, has edge length e ∈ Q≥0 , and has center z ∈ Qn . For the remainder of this paper, we will consider only hypercubes that are parallel to the coordinate axes. For simplicity, we call these restricted hypercubes cubes. We say that a cube Cen (z) fits into a polyhedron defined by Ax ≤ b if all points inside the cube Cen (z) are solutions of Ax ≤ b, or formally: Cen (z) ⊆ P A b . In order to compute this, we transform the polyhedron Ax ≤ b into another polyhedron Ax ≤ b0 . For this new polyhedron, we merely have to test whether the cube’s center point z is a solution (z ∈ P A b0 ) in order to also determine whether the cube Cen (z) fits into the original polyhedron (Cen (z) ⊆ P A b ). This is a simple test that requires only evaluation. We presented this entire transformation in [3] as the linear cube transformation. To abbreviate the representation of this transformation, we will use the 1-norm [8], which is defined as kxk1 = |x1 | + . . . + |xn |. Lemma 2 ([3]). Let Cen (z) be a cube and Ax ≤ b be a polyhedron. Cen (z) ⊆ P A b if and only if Az ≤ b0 , where b0i = bi − 2e kai k1 . We say that a polyhedron implies an equality hT x = g, where h ∈ Qn , h 6= 0, and g ∈ Q, if hT x = g holds for all x ∈ P A b . An equality implied by Ax ≤ b is explicit if the inequalities hT x ≤ g and −hT x ≤ −g appear in Ax ≤ b. Otherwise, the equality is implicit. Polyhedra implying equalities have only surface points and, therefore, neither an interior nor a center. Thus, all cubes that fit into a polyhedron implying an equality dT x ≤ c with d 6= 0 have edge length zero. For the development of our first method deciding on implied equalities, we will use two formulations of Farkas’ Lemma: Lemma 3 ([2]). Ax ≤ b is satisfiable if and only if every y ∈ Qm with y ≥ 0 and y T A = 0 satisfies y T b ≥ 0, i.e., every non-negative linear combination of inequalities in Ax ≤ b does not result in a trivially unsatisfiable inequality, e.g., 0 ≤ −1. Lemma 4 ([2]). Ax ≤ b is unsatisfiable if and only if there exists a y ∈ Qm with y ≥ 0 and y T A = 0 so that y T b < 0, i.e., there exists a non-negative linear combination of inequalities in Ax ≤ b that results in the trivially unsatisfiable inequality y T Ax ≤ y T b. We call an unsatisfiable set C of inequalities minimal if every proper subset C 0 ⊂ C is satisfiable. Whenever a polyhedron Ax ≤ b is unsatisfiable, there exists a minimal set C of unsatisfiable inequalities so that every inequality in C appears also in Ax ≤ b [5]. We call such a minimal set C an explanation for Ax ≤ b’s unsatisfiability. In case we are investigating a minimal set of unsatisfiable inequalities, we can refine the second version of Farkas’ Lemma: T Lemma 5. Let C = {a0 i x ≤ b0i : 1 ≤ i ≤ m0 } be a minimal set of unsatisfiable constraints. 0 Let A0 = (a0 1 , . . . , a0 m0 )T and b0 = (b01 , . . . , b0m0 )T . Then, it holds for every y ∈ Qm with y ≥ 0, y T A0 = 0, and y T b0 < 0 that yi > 0 for all i ∈ {1, . . . , m0 }. Proof. Suppose to the contrary that there exists a y ≥ 0 with y T A0 = 0 and y T b0 < 0 such that one component of y is zero. Without loss of generality we assume that ym0 = 0. Let T C 0 = {a0 i x ≤ b0i : 1 ≤ i ≤ m0 − 1}, A00 = (a0 1 , . . . , a0 m0 −1 )T , b00 = (b01 , . . . , b0m0 −1 )T , and T T y 0 = (y1 , . . . , ym0 −1 )T . Then, y 0 ≥ 0, y 0 A00 = 0, and y 0 b00 < 0. However, by Lemma 4, this implies that A00 x ≤ b00 is unsatisfiable and, therefore, C 0 ⊂ C is also unsatisfiable. Thus, C is not minimal, which contradicts our initial assumptions. 3 Detecting Implied Equalities In this section, we present a method that detects whether a polyhedron Ax ≤ b implies an equality at all and then returns one valid equality as explanation. Polyhedra implying equalities have only surface points and, therefore, no interior. Thus, all cubes that fit into a polyhedron implying an equality hT x = g with h 6= 0 have edge length zero. Lemma 6 ([3]). Let Ax ≤ b be a polyhedron. Then, exactly one of the following statements is true: (1) Ax ≤ b implies an equality hT x = g with h 6= 0, or (2) Ax ≤ b contains a cube with edge length e > 0. Lemma 6 states that a polyhedron contains either a cube with a positive edge length e > 0, or an equality. Since e is arbitrarily small, the factor 2e kai k1 is also arbitrarily small. We can even choose our edge length so small that we can ignore the different multiples kai k1 and any infinitesimals introduced by strict inequalities. We just have to turn all of our inequalities into strict inequalities. Lemma 7. Let Ax ≤ b be a polyhedron, where ai 6= 0, bi = (pi , qi ), qi ∈ {−1, 0}, and bδi = (pi , −1) be the strict versions of the bounds bi for all i ∈ {1, . . . , m}. Then, the following statements are equivalent: (1) Ax ≤ b contains a cube with edge length e > 0, and (2) Ax ≤ bδ is satisfiable, where all bounds bi of Ax ≤ b have been replaced by strict bounds bδi . Proof. (1) ⇒ (2): If Ax ≤ b contains a cube of edge length e > 0, then Ax ≤ b − a0 is satisfiable, where a0i = 2e kai k1 . By Lemma 1, we know that there must exist a δ ∈ Q such that Ax ≤ p + qδ − a0 holds. Now, let δ 0 = min{a0i − qi δ : i = 1, . . . , m}. Since a0i − qi δ ≥ δ 0 , it holds that Ax ≤ p − δ 0 1. Since qi ∈ {−1, 0} and a0i = kai k1 > 0, it also holds that δ 0 > 0. By Lemma 1, we deduce that Ax < p and, therefore, Ax ≤ bδ holds. (2) ⇒ (1): If Ax ≤ bδ is satisfiable, then we know by Lemma 1 that there must exist a δ > 0 such that Ax ≤ p − δ1 holds. Let amax = max{kai k1 : i = 1, . . . , m}, δ 0 = 2δ , and e = amax δ . 0 e e Then, pi − δ = pi − δ − 2 amax ≤ bi − 2 kai k1 . Thus, Ax ≤ b contains a cube with edge length e > 0. In case Ax ≤ bδ is unsatisfiable, Ax ≤ b contains no cube with positive edge length and, therefore by Lemma 6, an equality. Dutertre and de Moura presented a dual simplex algorithm that can solve the systems Ax ≤ b and Ax ≤ bδ [5]. In case Ax ≤ bδ is unsatisfiable, the algorithm returns an explanation, i.e., a minimal set C of unsatisfiable constraints aTi x ≤ bδi from Ax ≤ bδ . If Ax ≤ b itself is satisfiable, then we can extract equalities from this explanation: for every aTi x ≤ bδi ∈ C, Ax ≤ b implies the equality aTi x = bi . Lemma 8. Let Ax ≤ b be a satisfiable polyhedron, where ai 6= 0, bi = (pi , qi ), qi ∈ {−1, 0}, and bδi = (pi , −1) be the strict versions of the bounds bi for all i ∈ {1, . . . , m}. Let Ax ≤ bδ be unsatisfiable. Let C be a minimal set of unsatisfiable constraints aTi x ≤ bδi from Ax ≤ bδ . Then, it holds for every aTi x ≤ bδi ∈ C that aTi x = bi is an equality implied by Ax ≤ b. Proof. Because of transitivity of the subset and implies relationships, we can assume that Ax ≤ b and Ax ≤ bδ contain only the inequalities associated with the explanation C. Therefore, C = {aT1 x ≤ bδ1 , . . . , aTm x ≤ bδm }. By Lemma 4 and Ax ≤ bδ being unsatisfiable, we know that there exists a y ∈ Qm with y ≥ 0, y T A = 0, and y T bδ < 0. By Lemma 3 and Ax ≤ b being satisfiable, we know that y T b ≥ 0 is also true. By Lemma 5, we know that yk > 0 for every k ∈ {1, . . . , m}. Now, we will use y T bδ < 0, y T b ≥ 0, and the definitions of < and ≤ for Qδ to prove that y b = 0 and b = p. Since y T bδ < 0, we get that y T p ≤ 0. Since y T b ≥ 0, we get that y T p ≥ 0. T If we combine y T p ≤ 0 and y T p ≥ 0, we get that y T p = 0. From y T p = 0 and y T b ≥ 0, we get y T q ≥ 0. Since y > 0 and qi ∈ {−1, 0}, we get that y T q = 0 and qi = 0. Since qi = 0, b = p. Next, we multiply y T A = 0 with an x ∈ P A T b to get y Ax = 0. Since yk > 0 for every  Pm k ∈ {1, . . . , m}, we can solve y T Ax = 0 for every aTk x and get: aTk x = − i=1,i6=k yyki aTi x . Pm   Likewise, we will solve y T b = 0 for every bk to get: bk = − i=1,i6=k yyki bi . Since x ∈ P A T b satisfies all ai x ≤ bi , wecan deduce  bk as the lower  bound  of aTk x: m m aTk x = − i=1,i6=k yyki aTi x ≥ − i=1,i6=k yyki bi = bk , P P which proves that Ax ≤ b implies aTk x = bk . Lemma 8 justifies simplifications on Ax ≤ bδ . We can eliminate all inequalities in Ax ≤ bδ that cannot appear in the explanation of unsatisfiability, i.e., all inequalities aTi x ≤ bδi that cannot form an equality aTi x = bi that is implied by Ax ≤ b. For example, if we have an assignment v ∈ Qn such that Av ≤ b is true, then we can eliminate every inequality aTi x ≤ bδi for which aTi v = bi is false. According to this argument, we can also eliminate all inequalities aTi x ≤ bδi that were already strict inequalities in Ax ≤ b. 4 Computing an Equality Basis An equality basis for a satisfiable system of inequalities Ax ≤ b is a system of equalities D0 x = c0 such that all (explicit and implicit equalities) implied by Ax ≤ b are linear combinations of equalities from D0 x = c0 . Based on Gaussian elimination, we will represent D0 x = c0 as an equivalent system of equalities y − Dz = c such that y = (y1 , . . . , yny )T and z = (z1 , . . . , znz )T are a partition of the variables in x, D ∈ Qny ×nz , and c ∈ Qny . This form represents a distinct substitution that replaces variable yi with ci + dTi z. With the substitution we can directly check whether an equality hT x = g is a linear combination of y − Dz = c and, therefore, implied by both Ax ≤ b and y − Dz = c. We simply apply the substitution to hT x = g and see if it simplifies to 0 = 0. Since swapping the columns in A and xT does not influence the satisfiable assignments for x in Ax ≤ b, we assume without loss of generality that (x1 , . . . , xn ) = (y1 , . . . , yny , z1 , . . . , znz ). Algorithm 1: EqualityBasis(Ax ≤ b) Input : A satisfiable system of inequalities Ax ≤ b, where A ∈ Qm×n and b ∈ Qm δ Output: An equality basis Dx = c for Ax ≤ b T 1 z := (x1 , . . . , xn ) 0×0 2 D := () ∈ Q , c := () ∈ Q0 , y := () ∈ Q0 T 3 Remove all rows ai z ≤ b from Az ≤ b such that ai = 0 and bi = 0 δ 4 while Az ≤ b is unsatisfiable (i.e., Az ≤ b contains an equality) do 5 Let C be an explanation for Az ≤ bδ being unsatisfiable 6 Select (aTi z ≤ bδi ) ∈ C ; // by Lemma 8, aTi z = bi is implied by Az ≤ b /* Without loss of generality we can assume that ai1 6= 0. */ /* Otherwise, we would just swap the columns accordingly. */ 7 (y 0 , z 0 , A0 z 0 ≤ b0 , y 0 − D0 z 0 = c0 ) := Elim(y, z, Az ≤ b, y − Dz = c, aTi z = bi ) 8 (y, z, Az ≤ b, y − Dz = c) := (y 0 , z 0 , A0 z 0 ≤ b0 , y 0 − D0 z 0 = c0 ) 9 end 10 return y − Dz = c Figure 1: EqualityBasis computes an equality basis Algorithm 2: Elim(y, z, Az ≤ b, y − Dz = c, hT z = g) Input : Two variable vectors y and z, a system of inequalities Az ≤ b, a system of equalities y − Dz = c, and an equality hT z = g implied by Az ≤ b, where h1 6= 0 Output: The tuple (y 0 , z 0 , A0 z 0 ≤ b0 , y 0 − D0 z 0 = c0 ), where y 0 = (y1 , . . . , yny , z1 )T , z 0 = (z2 , . . . , znz )T , and the combined systems (Az ≤ b) ∪ (y − Dz = c) and (A0 z 0 ≤ b0 ) ∪ (y 0 − D0 z 0 = c0 ) have Pnz the same solutions 1 1 Replace z1 in Az ≤ b with z1 := h (g − j=2 hj zj ) 1 ai1 T ai1 /* by subtracting h1 h z = h1 g from every inequality aTi z ≤ bi */ 1 Pnz 2 Replace z1 in y − Dz = c with z1 := h (g − j=2 h j zj ) 1 /* by adding dhi11 hT z = dhi11 g to every equality yi − dTi z = ci */ Pnz −hj g 3 Add the row z1 − ( j=2 h1 j z ) = h1 to the end of y − Dz = c T 4 Remove all rows ai z ≤ bi from Az ≤ b such that ai = 0 and bi = 0 5 Remove the first column of Az ≤ b, which contains only zeros due to our substitutions T T 6 y := (y1 , . . . , yny , z1 ) , z := (z2 , . . . , znz ) 7 return (y, z, Az ≤ b, y − Dz = c) Figure 2: Elim removes an equality hT z = g from Az ≤ b The algorithm EqualityBasis(Ax ≤ b) (Figure 1) computes an equality basis y − Dz = c for the set of inequalities Ax ≤ b. To this end, EqualityBasis splits our system of inequalities into a system of inequalities Az ≤ b and a system of equalities y − Dz = c. While the variables z are completely defined by Az ≤ b, y − Dz = c is used to extend any assignment from the variables z to the variables y. Initially, z is just x, y − Dz = c is empty, and Az ≤ b is just Ax ≤ b. However, in every iteration of the while loop, EqualityBasis eliminates one equality aTi z = bi from Az ≤ b and adds it to y − Dz = c. EqualityBasis finds this equality based on Algorithm 3: Subst(y − Dz = c, Ax ≤ b) Input : A system of equalities y − Dz = c, and a system of inequalities Ax ≤ b such that (x1 , . . . , xn ) = (y1 , . . . , yny , z1 , . . . , znz ) Output: A0 z ≤ b0 , the system of inequalities that remains after we have eliminated the variables y from Ax ≤ b with the equations in y − Dz = c 0 0 0×0 0 T 1 z := (x1 , . . . , xn ) , D := () ∈ Q , c := () ∈ Q0 , y 0 := () ∈ Q0 2 for i = 1, . . . , ny do 3 (y 0 , z 0 , Az 0 ≤ b, y 0 − D0 z 0 = c0 ) := Elim(y 0 , z 0 , Az 0 ≤ b, y 0 − D0 z 0 = c0 , yi − dTi z = ci ) 4 end 5 return Az ≤ b Figure 3: Subst eliminates variables y from Ax ≤ b with the equations in y − Dz = c the techniques we presented in the Lemmas 7 & 8. Then, EqualityBasis uses the algorithm Elim from Figure 2 to eliminate aTi z = bi from Az ≤ b and to add it to y − Dz = c. Note that we assume for this algorithm that ai1 6= 0. Naturally, this is not always the case, but we could assure it by swapping columns. We refrain from doing so explicitly to simplify the algorithm. The results of applying Elim(y, z, Az ≤ b, y − Dz = c, hT z = g) are a new system of inequalities A0 z 0 ≤ b0 , a new system of equalities y 0 − D0 z 0 = c0 , and a new partition of our variables y 0 = (y1 , . . . , yny , z1 )T and z 0 = (z2 , . . . , znz )T . Due to the new partition, the variable yn0 y +1 := z1 is no longer defined by the inequalities A0 z 0 ≤ b0 , but it is defined by the equalities y 0 − D0 z 0 = c0 . However, Elim conserves the equivalence of the split systems, i.e., the combination of the input systems (Az ≤ b) ∪ (y − Dz = c) and the combination of the output systems (A0 z 0 ≤ b0 ) ∪ (y 0 − D0 z 0 = c0 ) are equivalent. Lemma 9. Let Az ≤ b be a system of inequalities. Let y −Dz = c be a system of equalities. Let hT z = g be an equality implied by Az ≤ b. Let (y 0 , z 0 , A0 z 0 ≤ b0 , y 0 −D0 z 0 = c0 ) := Elim(y, z, Az ≤ b, y − Dz = c, hT z = g), where y 0 = (y1 , . . . , yny , z1 )T , and z 0 = (z2 , . . . , znz )T . Let u ∈ Qny , v ∈ Qnz , u0 = (u1 , . . . , uny , v1 )T , and v 0 = (v2 , . . . , vnz )T Then, (Av ≤ b) ∪ (u − Dv = c) is true if and only if (A0 v 0 ≤ b0 ) ∪ (u0 − D0 v 0 = c0 ) is true. Proof. Assume that (Av ≤ b) ∪ (u − Dv = c) is true. Since Az ≤ b implies hT z = g, hT v = g is also true. We get (A0 v 0 ≤ b0 ) ∪ (u0 − D0 v 0 = c0 ) by subtracting multiples of hT v = g from (Av ≤ b) ∪ (u − Dv = c), which simplifies to subtracting 0 = 0 because hT v = g is true. Therefore, we have proven that (A0 v 0 ≤ b0 ) ∪ (u0 − D0 v 0 = c0 ) is true. Assume that (A0 v 0 ≤ b0 ) ∪ (u0 − D0 v 0 = c0 ) is true. Since the last row of y 0 − D0 z 0 = c0 is T just hh1z = hg1 (see line 3 in Fig. 2), hT v = g is true. We get (Av ≤ b) ∪ (u − Dv = c) by adding multiples of hT v = g to (A0 v 0 ≤ b0 ) ∪ (u0 − D0 v 0 = c0 ), which simplifies to adding 0 = 0 because hT v = g is true. Therefore, we have also proven that (Av ≤ b) ∪ (u − Dv = c) is true. After removing all equalities from Ax ≤ b the algorithm EqualityBasis(Ax ≤ b) terminates resulting in a system of inequalities A0 z ≤ b0 implying no equalities and a system of equalities y − Dz = c that is an equality basis of the original system Ax ≤ b. The algorithm is guaranteed to terminate because every call to Elim moves one variable from the vector z to the vector y. Note that EqualityBasis(Ax ≤ b) does not return the final system of inequalities A0 z ≤ b0 . However, we can obtain it with the help of a third algorithm Subst(y − Dz = c, Ax ≤ b) (Figure 3). The algorithm Subst(y −Dz = c, Ax ≤ b) eliminates the variables yi by substituting them with c + dTi z, which also eliminates the equalities y − Dz = c from Ax ≤ b the same way EqualityBasis(Ax ≤ b) did. Since Subst is based on Elim, Subst is also equivalence preserving. A fact that we will exploit to prove the correctness of EqualityBasis(Ax ≤ b). Lemma 10. Let y − Dz = c be a satisfiable system of equalities. Let Ax ≤ b and A∗ x ≤ b∗ be two systems of inequalities, both implying the equalities in y−Dz = c. Let A0 z ≤ b0 be the output of Subst(y − Dz = c, Ax ≤ b). Let A∗∗ z ≤ b∗∗ be the output of Subst(y − Dz = c, A∗ x ≤ b∗ ). Then, A0 z ≤ b0 is equivalent to A∗∗ z ≤ b∗∗ if Ax ≤ b is equivalent to A∗ x ≤ b∗ . Proof. Let Ax ≤ b be equivalent to A∗ x ≤ b∗ . Suppose to the contrary that A0 z ≤ b0 is not equivalent to A∗∗ z ≤ b∗∗ . This means that there exists a v ∈ Qnz such that either A0 v ≤ b0 is true and A∗∗ v ≤ b∗∗ is false, or A0 v ≤ b0 is false and A∗∗ v ≤ b∗∗ is true. Without loss of generality we select the first case that A0 v ≤ b0 is true and A∗∗ v ≤ b∗∗ is false. We now extend this solution by u ∈ Qny , where ui := ci + dTi v, so (A0 v ≤ b0 ) ∪ (u − Dv = c) is true. However, based on Lemma 9 and the transitivity of equivalence, the four systems of constraints Ax ≤ b, A∗ x ≤ b∗ , (A0 z ≤ b0 ) ∪ (y − Dz = c), and (A∗∗ z ≤ b∗∗ ) ∪ (y − Dz = c) are equivalent. Therefore, (A∗∗ v ≤ b∗∗ ) ∪ (u − Dv = c) is true, which means that A∗∗ v ≤ b∗∗ is also true. The latter contradicts our initial assumptions. We also use Subst to determine whether a system of equalities implies (implicitly or explic- itly) an equality hT x = g. Again this is based on the fact that Dx = c implies an equality if and only if the equality can be obtained by a linear combination from Dx = c. However, with Subst we turn Dx = c into a substitution and can directly check whether hT x = g is a linear combination from Dx = c. We simply apply the substitution to hT x = g and see if it simplifies to 0 = 0. In this case, line 4 of Elim eliminates the equality. Lemma 11. Let y − Dz = c be a satisfiable system of equalities. Let hT x = g be an equality. Then, hT x = g is implied by y − Dz = c if and only if Subst(y − Dz = c, hT x = g) = ∅. Proof. First of all, let us look at the case where hT x = g is an explicit equality yi − dTi z = ci in y−Dz = c. Then clearly, yi −dTi z = ci will be eliminated when we call Elim with yi −dTi z = ci in line 3 of Subst. Therefore, the empty set is the output of both Subst(y − Dz = c, yi − dTi z = ci ) and Subst(y − Dz = c, y − Dz = c). Now, let us look at the case where hT x = g is an implicit equality in y − Dz = c. Since both y − Dz = c and (y − Dz = c) ∪ (hT z = g) imply hT z = g and the equalities in y − Dz = c, the output of both Subst(y − Dz = c, y − Dz = c) and Subst(y − Dz = c, (y − Dz = c) ∪ (hT z = g)) must be equivalent (see Lemma 10). Therefore, the output of Subst(y − Dz = c, (y − Dz = c) ∪ (hT z = g)) can only be the empty set. Hence, the output of Subst(y − Dz = c, hT z = g) is also the empty set. Finally, let us look at the case where hT x = g is not an equality implied by y − Dz = c. Suppose to the contrary that the output of Subst(y − Dz = c, hT z = g) is the empty set. We know based on Lemma 9 and transitivity of equivalence that (y − Dz = c) ∪ (hT z = g) and (y − Dz = c) ∪ ∅ are equivalent. Therefore, hT z = g is implied by y − Dz = c, which contradicts our initial assumption. In case y − Dz = c is an equality basis of Ax ≤ b, we can use the above Lemma 11 to check whether Ax ≤ b implies hT z = g. Naturally, Ax ≤ b implies hT z = g if and only if Subst(y − Dz = c, hT z = g) = ∅. With the help of the Lemmas 10 & 11, we are also able to prove that EqualityBasis(Ax ≤ b) computes an actual equality basis. Lemma 12. Let Ax ≤ b be a satisfiable system of inequalities. Let y − Dz = c be the output of EqualityBasis(Ax ≤ b). Then y − Dz = c is an equality basis of Ax ≤ b. Proof. Let A0 z ≤ b0 be the output of Subst(y − Dz = c, Ax ≤ b). Since y − Dz = c is the output of EqualityBasis(Ax ≤ b), the condition in line 4 of EqualityBasis guarantees us that A0 z ≤ b0 implies no equalities. Now, suppose to the contrary of our initial assumptions that Ax ≤ b implies an equality hT x = g that y − Dz = c does not imply. Since hT x = g is not implied by y − Dz = c, the output of Subst(y − Dz = c, hT x = g) is an equality T T h0 z = g 0 , where h0 6= 0. This also implies that (A0 z ≤ b0 ) ∪ (h0 z = g 0 ) is the output of T Subst(y − Dz = c, (Ax ≤ b) ∪ (h x = g)). By Lemma 10, A z ≤ b and (A0 z ≤ b0 ) ∪ (h0 z = g 0 ) T 0 0 T are equivalent. Therefore, A0 z ≤ b0 implies the equality h0 z = g 0 , which contradicts the condition in line 4 of EqualityBasis and, therefore, our initial assumptions. 5 Conclusions Through Lemmas 7 & 8, we have presented a method that efficiently checks whether a system of linear arithmetic constraints implies an equality at all. We use this method in the algorithm EqualityBasis(Ax ≤ b) to compute an equality basis y − Dz = c. With the algorithm Subst(y − Dz = c, Ax ≤ b), we have also presented an algorithm that simplifies a system of linear arithmetic constraints Ax ≤ b by eliminating all equalities y − Dz = c from Ax ≤ b via substitution. Moreover, we explained how to use an equality basis y − Dz = c of Ax ≤ b and Subst(y − Dz = c, hT x = g) to check whether Ax ≤ b implies a given equality hT x = g. There already exist several methods that find, isolate, and eliminate implied equali- ties [1, 10, 11, 12]. Hentenryck and Graf [12] define unique normal forms for systems of linear constraints with non-negative variables. To compute a normal form, they first eliminate all implied equalities aTi x = bi from Ax ≤ b. To this end, they determine the lower bound for each inequality aTi x ≤ bi in Ax ≤ b by solving one optimization linear program for each inequality. Similarly, Refalo [10] describes several incremental methods that turn a satisfiable system of linear constraints in “revised solved form” into a system without any implied equalities. He also uses optimization to detect and to eliminate implied equalities. The method presented by Telgen [11] does not require optimization. He presents criteria to detect implied equalities based on the tableau used in the simplex algorithm. However, Telgen was not able to formulate an algorithm that efficiently computes these criteria. In the worst case, he has to pivot the simplex tableau until he has computed all possible tableaux for the given system of constraints. Another method that detects implied equalities was presented by Bjørner [1]. He uses Fourier Motzkin variable elimination to compute linear combinations that result in implied equalities. Our methods do not require optimization, which SMT solvers are usually not fine-tuned for. Furthermore, we have defined our methods for a rather general formulation of linear constraints, which makes it very easy to convert our results into other representations, e.g., the tableau-and- bound representation used in Dutertre and de Moura’s version of the simplex algorithm (see Appendix B). Finally, our method efficiently searches for implied equalities. We neither have to check each inequality independently nor do we have to blindly pivot the simplex tableau. Our methods can be implemented as an extension of Dutertre and de Moura’s simplex algorithm [5]. The input constraints for this algorithm are represented by a so-called tableau Ax = 0 and two bounds li ≤ xi ≤ ui for every variable xi in the tableau. The variables are also partitioned into two sets: the non-basic variables and the basic variables. We find a satisfiable assignment by updating an intermediate assignment β. These updates are typically accompanied by a pivot of the tableau, i.e., by performing substitutions in the tableau, a non- basic variable and a basic variable are swapped. It is also possible to transform our system of inequalities A0 x0 ≤ b0 into this tableau-and- bound representation with the help of slack variables. However, this transformation also means that other representations have to be adjusted accordingly. For example, an equality basis is no longer a system of equalities but a tableau Ax = 0 and a set of tightly bounded variables xi such that li = ui . This means that our goal shifts from finding equalities aTi x = bi to finding tightly bounded variables. It also means that turning the bounds li and ui of every variable xi into strict bounds is enough to apply Lemma 7. The tableau-and-bound representation also grants us several advantages for the implemen- tation of our methods. For example, we do not have to explicitly eliminate variables via substi- tution. As mentioned in Section 3, the specifics of the implementation will also contain justified simplifications for Lemma 7. For further details on the implementation, see the Appendix. For future research, we plan to investigate the above methods and their performance as a preprocessing step for our cube tests [3], and as a certifying algorithm for the equalities transferred as part of the Nelson-Oppen style combination of theories [4]. Acknowledgments The authors would like to thank the anonymous reviewers for their valuable comments, sugges- tions, and for directing us to related work. References [1] N. Bjørner. Integrating Decision Procedures for Temporal Verification. PhD thesis, Stanford, CA, USA, 1999. AAI9924398. [2] S. Boyd and L. Vandenberghe. Convex Optimization. Cambridge University Press, New York, NY, USA, 2004. [3] M. Bromberger and C. Weidenbach. Fast cube tests for lia constraint solving. In N. Olivetti and A. Tiwari, editors, IJCAR 2016, volume 9706 of LNCS. Springer, 2016. [4] R. Bruttomesso, A. Cimatti, A. Franzen, A. Griggio, and R. Sebastiani. Delayed theory combina- tion vs. nelson-oppen for satisfiability modulo theories: a comparative analysis. AMAI, 55(1):63– 99, 2009. [5] B. Dutertre and L. de Moura. A fast linear-arithmetic solver for dpll(t). In T. Ball and R. B. Jones, editors, CAV, volume 4144 of LNCS, pages 81–94. Springer, 2006. [6] G. Faure, R. Nieuwenhuis, A. Oliveras, and E. Rodrı́guez-Carbonell. Sat modulo the theory of linear arithmetic: Exact, inexact and commercial solvers. In H. Kleine Büning and X. Zhao, editors, SAT 2008, volume 4996 of LNCS, pages 77–90. Springer, 2008. [7] A. Griggio. A practical approach to satisfiability modulo linear integer arithmetic. JSAT, 8(1/2):1– 27, 2012. [8] R. A. Horn and C. R. Johnson. Norms for vectors and matrices. In Matrix Analysis, pages 313–386. Cambridge University Press, second edition, 2012. Cambridge Books Online. [9] M. Jünger, T. M. Liebling, D. Naddef, G. L. Nemhauser, W. R. Pulleyblank, G. Reinelt, G. Rinaldi, and L. A. Wolsey, editors. 50 Years of Integer Programming 1958-2008. Springer, 2010. [10] P. Refalo. Approaches to the incremental detection of implicit equalities with the revised simplex method. In C. Palamidessi, H. Glaser, and K. Meinke, editors, PLILP 1998, volume 1490 of LNCS, pages 481–496. Springer, 1998. [11] J. Telgen. Identifying redundant constraints and implicit equalities in systems of linear constraints. Management Science, 29(10):1209–1222, 1983. [12] P. Van Hentenryck and T. Graf. Standard forms for rational linear arithmetic in constraint logic programming. AMAI, 5(2):303–319, 1992. Appendix A The Dual Simplex Algorithm In the next section of the appendix, we present a guideline for an implementation of the above methods as an extension of the dual simplex algorithm by Dutertre and de Moura [5]. Whenever we will refer to the simplex algorithm in this appendix, we will refer to the specific version of the dual simplex algorithm presented by Dutertre and de Moura [5]. The simplex algorithm accepts only linear arithmetic systems that are defined by a system of equalities Ax = 0 and a set of bounds for the variables lj ≤ xj ≤ uj (for j = 1, . . . , n). If there is no lower bound lj ∈ Qδ for variable xj , then we simply set lj = −∞. Similarly, if there is no upper bound uj ∈ Qδ for variable xj , then we simply set uj = ∞. We can easily transform a system of inequalities Ax ≤ b into the above format if we introduce a so-called slack variable si for every inequality in our system. Our system is then defined by the equalities Ax − s = 0, and the bounds −∞ ≤ xj ≤ ∞ for every original variable xj and the bounds −∞ ≤ si ≤ bi for every slack variable introduced for the inequality aTi x ≤ bi . We can even reduce the number of slack variables if we transform rows of the form aij · xj ≤ cj directly into bounds for xj . Moreover, we can use the same slack variable for multiple inequalities as long as the left side of the inequality is similar enough. For example, the inequalities aTi x ≤ bi and −aTi x ≤ ci can be transformed into the equality aTi x−si = 0 and the bounds −ci ≤ si ≤ bi . For more details on these simplifications we refer to [5]. The simplex algorithm also partitions the variables into two sets: the set of non-basic variables N and the set of basic variables B. Initially, our original variables are the non-basic variables and the slack variables are the basic variables. The non-basic variables N define the basic variables over a tableau derived from our P system of equalities. Each row in this tableau represent one basic variable xi ∈ B: xi = xj ∈N aij xj . The simplex algorithm exchanges variables from xi ∈ B and xj ∈ N with the pivot algorithm (Figure 4). To do so, we also have to change the tableau via substitution. All tableaux constructed in this way are equivalent to the original system of equalities Ax = 0. The goal of the simplex algorithm is to find an assignment β that maps every variable xi to a value β(xi ) ∈ Qδ that satisfies our constraint system, i.e., A(β(x)) = 0 and li ≤ β(xi ) ≤ ui for every variable xi . The algorithm starts with an assignment β that fulfils A(β(x)) = 0 and lj ≤ β(xj ) ≤ uj for every non-basic variable xj ∈ N . Initially, we get such an assignment through our tableau. We simply choose a value lj ≤ β(xj ) ≤ uj for every non-basic P variable xj ∈ N and define the value of every basic variable xi ∈ B over the tableau: β(xi ) := xj ∈N aij β(xj ). As an invariant, the simplex algorithm will continue to fulfil A(β(x)) = 0 and lj ≤ β(xj ) ≤ uj for every non-basic variable xj ∈ N and every intermediate assignment β. The simplex algorithm finds a satisfiable assignment or an explanation of unsatisfiability through the Check() algorithm (Figure 4). Since all non-basic variables fulfil their bounds and the tableau guarantees that Ax = 0, Check() only looks for a basic variable that violates one of its bounds. If all basic variables xi satisfy their bounds, then β is already a satisfiable assignment and Check() can return true. If Check() finds a basic variable xi that violates one of its bounds, then it looks for a non-basic variable xj it can pivot with. We fulfil our invariant again after an update of our β assignment that sets β(xi ) to the previously violated bound value. However, not all non-basic variables can be used for pivoting. If every non-basic variable violates the conditions in lines 6 & 12 of Check(), then the row of xi and all non-basic variables xj with aij 6= 0 build an unresolvable conflict. Hence, Check() has found a row that explains the conflict and it can return unsatisfiable. Algorithm 4: pivot(xi , xj ) Input : A basic variable xi and a non-basic variable xj so that aij is non-zero Effect :PTransforms the tableau so xi becomes non-basic and xj basic 1 Let xi = k∈N aik xk be the row defining 1 P the basic aik variable xi 2 We rewrite this row as xj = a xi − k∈N \{xj } aij k so it defines xj instead x ij 3 foreach xk ∈ N \ {xj } do ajk := − aaik ij ; 4 aji := a1ij aik Then, we substitute xj in all other rows with a1ij xi − P 5 k∈N \{xj } aij xk 6 for xl ∈ B do 7 foreach xk ∈ N \ {xj } do alk := alk + alj ajk ; 8 ali := alj aji ; alj := 0 9 end 10 N = (N ∪ {xi }) \ {xj }; B = (B ∪ {xj }) \ {xi } Algorithm 5: update(xj , v) Input : A non-basic variable xj and a value v ∈ Qδ Effect : Sets the value β(xj ) of xj to v and updates the values of all basic variables 1 foreach xi ∈ B do β(xi ) := β(xi ) + aij (v − β(xj )); 2 β(xj ) := v Algorithm 6: pivotAndUpdate(xi , xj , v) Input : A basic variable xi , a non-basic variable xj , and a value v ∈ Qδ Effect : Pivots variables xi and xj and updates the value β(xi ) of xi to v v−β(xi ) 1 θ := aij 2 β(xi ) := v; β(xj ) := β(xj ) + θ 3 foreach xk ∈ B \ {xi } do β(xk ) := β(xk ) + akj θ; 4 pivot(xi , xj ) Algorithm 7: Check() Output : Returns true iff there exists a satisfiable assignment for the tableau and the bounds u and l; otherwise, it returns (false,xi ), where xi is the conflicting basic variable 1 while true do 2 select the smallest basic variable xi such that β(xi ) < li or β(xi ) > ui 3 if there is no such xi then return true; 4 if β(xi ) < li then 5 select the smallest non-basic variable xj such that 6 (aij > 0 and β(xj ) < uj ) or (aij < 0 and β(xj ) > lj ) 7 if there is no such xj then return (false,xi ); 8 pivotAndUpdate(xi , xj , li ) 9 end 10 if β(xi ) > ui then 11 select the smallest non-basic variable xj such that 12 (aij < 0 and β(xj ) < uj ) or (aij > 0 and β(xj ) > lj ) 13 if there is no such xj then return (false,xi ); 14 pivotAndUpdate(xi , xj , ui ) 15 end 16 end Figure 4: The functions of the dual simplex algorithm by Dutertre and de Moura [5] The algorithm is guaranteed to terminate due to a variable selection strategy called Bland’s rule. Bland’s rule is based on a predetermined variable order and always selects the smallest variables fulfilling the conditions for pivoting. B Specifics for an Implementation An equality basis for a satisfiable system of inequalities Ax ≤ b is a system of equalities Dx = c such that all (explicit and implicit equalities) implied by Ax ≤ b are linear combinations of equalities from Dx = c. In case of the tableau-and-bound representation of the simplex algorithm, an equality basis simplifies to a tableau and a set of tightly bounded variables, i.e., β(xj ) := lj or β(xj ) := uj for all satisfiable assignments β. Therefore, one way of determining an equality basis is to find all tightly bounded variables. To find all tightly bounded variables, we present a new extension of the simplex algorithm called FindTightBounds() (Figure 5). This extension uses our Lemmas 7 & 8 to iteratively find all bounds lj ≤ xj (xj ≤ uj ) that hold tightly for all satisfiable assignments β, and then turns them into explicit equalities by setting uj := lj (lj := uj ). But first of all, FindTightBounds() determines if our constraint system is actually satisfiable with a call of Check(). If the system is unsatisfiable, then it has no solutions and, therefore, implies all equalities. In this case, FindTightBounds() stops an returns false. Otherwise, we get a satisfiable assignment β from Check() and we use this assignment in Initialize() (Figure 5) to eliminate all bounds that do not hold tightly under β (i.e., β(xi ) > li or β(xi ) < ui ). We know that we can eliminate these bounds without losing any tightly bounded variables because we only need the bounds that can be part of an equality explanation, i.e., only bounds that hold tightly for all satisfiable assignments (see Lemma 8). For the same reason, Initialize() eliminates all originally strict bounds, i.e., bounds with a non-zero delta part. Next, Initialize() tries to turn as many variables xi with li = ui into non-basic variables. We do so because xi is guaranteed to stay a non-basic variable if li = ui (see lines 6 & 12 of Check). Pivoting like this essentially eliminates the tightly bounded non-basic variable xi and replaces it with the constant value li . There only exists one case when Initialize() cannot turn the variable xi with li = ui into a non-basic variable. This case occurs whenever all non- basic variables xj with non-zero P coefficient aij also have tight bounds lj = uj . However, in this case the complete row xi = xj ∈N aij xj simplifies to xi = li , so it will never produce a conflict and we can also ignore this row. As its last action, Initialize() turns the bounds of all variables xj with lj < uj into strict bounds. Since Initialize() transformed these bounds into strict bounds, the condition of the while loop in line 3 of FindTightBounds() checks whether the system contains another tightly bounded variable (see also Lemma 7). If Check returns (false, xi ), then the row xi represents an equality explanation and all variables xj with a non-zero coefficient in the row hold tightly (see Lemma 8). FindTightBounds() uses FixEqualities(xi ) (Figure 5) to turn these tightly bounded variables xj into explicit equalities. FixEqualities(xi ) simply sets lj = uj and, thereby, the variable xj is (essentially) replaced with the constant value lj . After FixEqualities(xi ) is done fixing the tightly bounded variables, we go back to the beginning of the loop in FindTightBounds() and do another call to Check. If Check returns true, then the original system of inequalities implies no further tightly bounded variables (Lemma 7). We exit the loop and revert the bounds of the remaining variables xj with lj < uj to their original values. As a result, we have also reverted to a linear system equivalent to our original constraint system. The only difference is that now all tightly bounded variables xi are explicit equalities, i.e., li = ui , and represent an equality basis for our Algorithm 8: Initialize() Effect : Removes all bounds lk and uk that cannot produce equalities; turns as many basic variables xi with li = ui into non-basic variables as is possible; the bounds for all variables xk are turned into strict bounds if lk < uk 1 for xk ∈ B ∪ N do 2 if β(xk ) > lk then lk := −∞; 3 if β(xk ) < uk then uk := +∞; 4 if β(xk ) = pk + qk δ such that qk 6= 0 then lk := −∞; uk := ∞; 5 end 6 for xi ∈ B do 7 if li = ui then 8 select the smallest non-basic variable xj such that aij is non-zero and lj < uj 9 if there is such an xj then pivot(xi , xj ); 10 end 11 end 12 for xk ∈ B ∪ N do 13 if lk < uk then 14 if lk 6= −∞ then lk := lk + δ; 15 if uk 6= +∞ then uk := uk − δ; 16 if lk 6= −∞ and xk ∈ N then update(xk , lk ); 17 if uk 6= +∞ and xk ∈ N then update(xk , uk ); 18 end 19 end Algorithm 9: FixEqualities(xi ) Input : A basic variable xi that explains the conflict Effect : Turns the bounds of all variables responsible for the conflict into equalities 1 for xj ∈ N do 2 if lj < uj then 3 if β(xi ) < li and aij > 0 then uj := uj + δ; lj := uj ; update(xj , uj ); 4 if β(xi ) < li and aij < 0 then lj := lj − δ; uj := lj ; update(xj , lj ); 5 if β(xi ) > ui and aij > 0 then lj := lj − δ; uj := lj ; update(xj , lj ); 6 if β(xi ) > ui and aij < 0 then uj := uj + δ; lj := uj ; update(xj , uj ); 7 end 8 end 9 if β(xi ) > ui then ui := ui + δ; li := ui ; 10 if β(xi ) < li then li := li − δ; ui := li ; Algorithm 10: FindTightBounds() Effect : Finds as many tightly bounded variables as possible Output : false iff the system of linear arithmetic constraints is unsatisfiable 1 if Check() returns (false,xi ) then return false; 2 Initialize() 3 while Check() returns (false,xi ) do 4 FixEqualities(xi ) 5 end 6 For all variables xi with li < ui recover their old bounds 7 return true Figure 5: The functions used to turn our original tableau into a basis of equalities Algorithm 11: IsImplied(hT x = g) Input : An equality hT x = g Output : Returns true iff hT x = g is implied by our system of constraints 1 if FindTightBounds() returns false then return true; 2 for i := 1, . . . , n do 3 if xi ∈ N and li = ui then g := g − hi · li ; hi := 0; 4 if xi ∈ B then 5 for xj ∈ N do 6 if lj = uj then g := g − aij · hi · lj ; 7 if lj 6= uj then hj := hj + aij · hi ; 8 end 9 end 10 end 11 return (h = 0 and g = 0) Figure 6: IsImplied checks whether hT x = g is implied by our system of inequalities original constraint system. Hence, we can continue with other computations on the tableau without losing our equality basis. The algorithm FindTightBounds() P terminates because every call to FixEqualities(xi ) simplifies the row xi = xj ∈N aij xj to xi = li . Hence, the row will never again be an equality explanation and the number of iterations we spent in the while loop of FindTightBounds() is bounded by the number of variables. Finally, we present IsImplied(hT x = g), an algorithm that uses the equality basis to detect whether our original system of constraints implies the equality hT x =Pg. The algorithm substitutes all basic variables xi in hT x = g with their row definition xj ∈N aij xj . The algorithm also replaces every tightly bounded non-basic variable xj with the constant bound value cj it is tightly bounded to. As a result of these substitutions, hT x = g simplifies to 0T x = 0 if and only if hT x = g is implied by our system of constraints. Note that the call to FindTightBounds() in line 1 of IsImplied is not necessary if we made the call once before.