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 rst method e ciently 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 rst method to compute a basis for all implied equalities, i.e., a nite representation of all equalities implied by the linear arithmetic constraints. The third method uses the second method to check e ciently whether a system of linear arithmetic constraints implies a given equality.
Polyhedra and the systems of linear arithmetic constraints Ax b de ning them have a vast
number of theoretical and real-world applications [
In Section 3, we present the rst method, which e ciently 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 simpli ed. 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 unsatis able, then Ax b has no interior and implies an equality (Lemma 7). Based on an explanation of unsatis ability 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 nite representation of all equalities implied by the satis able linear arithmetic constraints Ax b. For this purpose, the algorithm iteratively applies the rst method to nd, 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 [
Finally, in Section 4 we introduce an e cient 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 e ciently explores implication of a given equality. For
the Nelson-Oppen style combination of theories inside an SMT solver [
While the di erence 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 aiT = (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 aiT x bi and strict inequalities aiT x < bi, where ai 2 Qn and bi 2 Q. We will model strict inequalities as non-strict inequalities by generalizing the eld Q for our inequality bounds bi to Q .
Lemma 1 ([
As a result of this observation, is expressed symbolically as an in nitesimal parameter [
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 2 Q [
In this paper, we treat polyhedra and their de nitions through a system of inequalities Ax b as interchangeable. For such a system of inequalities, the row coe cients are given by A = (a1; : : : ; am)T 2 Qm n, the variables are given by x = (x1; : : : ; xn)T , and the inequality bounds are given by b = (b1; : : : ; bm)T 2 Qm. To avoid misuse of the in nitesimal, we also require that the -coe cient 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 fa1T x b1; : : : ; aTmx bmg. Since Ax b and A0x b0 are just sets, we can write their combination as (Ax b)[(A0x 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 coe cients are given by D = (d1; : : : ; dm)T 2 Qm n, the variables are given by x = (x1; : : : ; xn)T , and the equality bounds are given by c = (c1; : : : ; cm)T 2 Qm.
We denote by P bA = fx 2 Qn : Ax bg the set of rational solutions to the system of inequalities Ax b and, therefore, the points inside the polyhedron. Similarly, we denote by Cen(z) = x 2 Qn : 8j 2 1; : : : ; n: jxj zj j 2e the set of points contained in the n-dimensional hypercube that is parallel to the coordinate axes, has edge length e 2 Q 0, and has center z 2 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) ts into a polyhedron de ned by Ax b if all points inside the
cube Cen(z) are solutions of Ax b, or formally: Cen(z) P bA. 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 2 P bA0 ) in order to also
determine whether the cube Cen(z) ts into the original polyhedron (Cen(z) P bA). This is a
simple test that requires only evaluation. We presented this entire transformation in [
Az b0, where b0i = bi 2e kaik1. b be a polyhedron. Cen(z)
We say that a polyhedron implies an equality hT x = g, where h 2 Qn, h 6= 0, and g 2 Q, if hT x = g holds for all x 2 P bA. 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 t into a polyhedron implying an equality dT x c with d 6= 0 have edge length zero.
For the development of our rst method deciding on implied equalities, we will use two
formulations of Farkas' Lemma:
Lemma 3 ([
Lemma 4 ([
We call an unsatis able set C of inequalities minimal if every proper subset C0 C is
satis able. Whenever a polyhedron Ax b is unsatis able, there exists a minimal set C of
unsatis able inequalities so that every inequality in C appears also in Ax b [
Proof. Suppose to the contrary that there exists a y 0 with yT A0 = 0 and yT b0 < 0 such that one component of y is zero. Without loss of generality we assume that ym0 = 0. Let C0 = fa0iT x b0i : 1 i m0 1g, A00 = (a01; : : : ; a0m0 1)T , b00 = (b01; : : : ; b0m0 1)T , and y0 = (y1; : : : ; ym0 1)T . Then, y0 0, y0T A00 = 0, and y0T b00 < 0. However, by Lemma 4, this implies that A00x b00 is unsatis able and, therefore, C0 C is also unsatis able. Thus, C is not minimal, which contradicts our initial assumptions. 3
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 t into a polyhedron implying an equality hT x = g with h 6= 0 have edge length zero.
Lemma 6 ([
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 kaik1 is also arbitrarily small. We can even choose our edge length so small that we can ignore the di erent multiples kaik1 and any in nitesimals 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 2 f 1; 0g, and bi = (pi; 1) be the strict versions of the bounds bi for all i 2 f1; : : : ; mg. Then, the following statements are equivalent: (1) Ax b contains a cube with edge length e > 0, and (2) Ax b is satis able, where all bounds bi of Ax b have been replaced by strict bounds bi . Proof. (1) ) (2): If Ax b contains a cube of edge length e > 0, then Ax b a0 is satis able, where a0i = 2e kaik1. By Lemma 1, we know that there must exist a 2 Q such that Ax p + q a0 holds. Now, let 0 = minfa0i qi : i = 1; : : : ; mg. Since a0i qi 0 , it holds that Ax p 01. Since qi 2 f 1; 0g and a0i = kaik1 > 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 satis able, then we know by Lemma 1 that there must exist a > 0 such that Ax p 1 holds. Let amax = maxfkaik1 : i = 1; : : : ; mg, 0 = 2 , and e = amax . Then, pi = pi 0 2e amax bi 2e kaik1. Thus, Ax b contains a cube with edge length e > 0.
In case Ax b is unsatis able, 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 [
Lemma 8. Let Ax b be a satis able polyhedron, where ai 6= 0, bi = (pi; qi), qi 2 f 1; 0g, and bi = (pi; 1) be the strict versions of the bounds bi for all i 2 f1; : : : ; mg. Let Ax b be unsatis able. Let C be a minimal set of unsatis able constraints aiT x bi from Ax b . Then, it holds for every aiT x bi 2 C that aiT 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 = fa1T x b1; : : : ; aTmx bmg. By Lemma 4 and Ax b being unsatis able, we know that there exists a y 2 Qm with y 0, yT A = 0, and yT b < 0. By Lemma 3 and Ax b being satis able, we know that yT b 0 is also true. By Lemma 5, we know that yk > 0 for every k 2 f1; : : : ; mg.
Now, we will use yT b < 0, yT b 0, and the de nitions of < and for Q to prove that yT b = 0 and b = p. Since yT b < 0, we get that yT p 0. Since yT b 0, we get that yT p 0. If we combine yT p 0 and yT p 0, we get that yT p = 0. From yT p = 0 and yT b 0, we get yT q 0. Since y > 0 and qi 2 f 1; 0g, we get that yT q = 0 and qi = 0. Since qi = 0, b = p.
Next, we multiply yT A = 0 with an x 2 P bA to get yT Ax = 0. Since yk > 0 for every k 2 f1; : : : ; mg, we can solve yT Ax = 0 for every akT x and get: akT x = Pim=1;i6=k yyki aiT x . akT x =
Pm
i=1;i6=k b implies akT x = bk.
Likewise, we will solve yT b = 0 for every bk to get: bk = Since x 2 P bA satis es all aiT x
Pim=1;i6=k yyki bi . bi, we can deduce bk as the lower bound of akT x:
yyki aiT x Pim=1;i6=k yyki bi = bk ; which proves that Ax
Lemma 8 justi es simpli cations on Ax b . We can eliminate all inequalities in Ax b that cannot appear in the explanation of unsatis ability, i.e., all inequalities aiT x bi that cannot form an equality aiT x = bi that is implied by Ax b. For example, if we have an assignment v 2 Qn such that Av b is true, then we can eliminate every inequality aiT x bi for which aiT v = bi is false. According to this argument, we can also eliminate all inequalities aiT x bi that were already strict inequalities in Ax b. 4
An equality basis for a satis able system of inequalities Ax b is a system of equalities D0x = c0 such that all (explicit and implicit equalities) implied by Ax b are linear combinations of equalities from D0x = c0. Based on Gaussian elimination, we will represent D0x = 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 2 Qny nz , and c 2 Qny . This form represents a distinct substitution that replaces variable yi with ci + diT 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 simpli es to 0 = 0. Since swapping the columns in A and xT does not in uence the satis able assignments for x in Ax b, we assume without loss of generality that (x1; : : : ; xn) = (y1; : : : ; yny ; z1; : : : ; znz ).
7 8 9 end 10 return y 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 (y0; z0; A0z0 b0; y0 D0z0 = c0), where y0 = (y1; : : : ; yny ; z1)T , z0 = (z2; : : : ; znz )T , and the combined systems (Az b) [ (y Dz = c) and (A0z0 b0) [ (y0 D0z0 = c0) have the same solutions 1 Replace z1 in Az Pjn=z2 hjzj) /* by subtractingb wahi1i1thhTzz1 =:=ahih1111g(gfrom every inequality aiT z bi /* by adding dhi11 hT z = dhi11 g to every equality yi diT z = ci 3 Add the row z1 (Pjn=z2 hh1j zj) = hg1 to the end of y Dz = c 4 Remove all rows aiT z bi from Az b such that ai = 0 and bi = 0 5 Remove the rst column of Az b, which contains only zeros due to our substitutions 6 y := (y1; : : : ; yny ; z1)T , z := (z2; : : : ; znz )T 7 return (y; z; Az b; y Dz = c) 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 de ned 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 aiT z = bi from Az b and adds it to y Dz = c. EqualityBasis nds 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: A0z b0, the system of inequalities that remains after we have eliminated the variables y from Ax b with the equations in y Dz = c 1 z0 := (x1; : : : ; xn)T ; D0 := () 2 Q0 0; c0 := () 2 Q0; y0 := () 2 Q0 2 for i = 1; : : : ; ny do 3 (y0; z0; Az0 b; y0 D0z0 = c0) := Elim(y0; z0; Az0 b; y0 D0z0 = c0; yi diT z = ci) 4 end 5 return Az b the techniques we presented in the Lemmas 7 & 8. Then, EqualityBasis uses the algorithm Elim from Figure 2 to eliminate aiT 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 A0z0 b0, a new system of equalities y0 D0z0 = c0, and a new partition of our variables y0 = (y1; : : : ; yny ; z1)T and z0 = (z2; : : : ; znz )T . Due to the new partition, the variable yn0y+1 := z1 is no longer de ned by the inequalities A0z0 b0, but it is de ned by the equalities y0 D0z0 = 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 (A0z0 b0) [ (y0 D0z0 = 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 (y0; z0; A0z0 b0; y0 D0z0 = c0) := Elim(y; z; Az b; y Dz = c; hT z = g), where y0 = (y1; : : : ; yny ; z1)T , and z0 = (z2; : : : ; znz )T . Let u 2 Qny , v 2 Qnz , u0 = (u1; : : : ; uny ; v1)T , and v0 = (v2; : : : ; vnz )T Then, (Av b) [ (u Dv = c) is true if and only if (A0v0 b0) [ (u0 D0v0 = 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 (A0v0 b0) [ (u0 D0v0 = c0) by subtracting multiples of hT v = g from (Av b) [ (u Dv = c), which simpli es to subtracting 0 = 0 because hT v = g is true. Therefore, we have proven that (A0v0 b0) [ (u0 D0v0 = c0) is true.
Assume that (A0v0 b0) [ (u0 D0v0 = c0) is true. Since the last row of y0 D0z0 = c0 is just hhT1z = 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 (A0v0 b0) [ (u0 D0v0 = c0), which simpli es 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 A0z 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 nal system of inequalities A0z 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 + diT 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 satis able system of equalities. Let Ax b and A x b be two systems of inequalities, both implying the equalities in y Dz = c. Let A0z 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, A0z 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 A0z b0 is not equivalent to A z b . This means that there exists a v 2 Qnz such that either A0v b0 is true and A v b is false, or A0v b0 is false and A v b is true. Without loss of generality we select the rst case that A0v b0 is true and A v b is false. We now extend this solution by u 2 Qny , where ui := ci + diT v, so (A0v 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 , (A0z 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 explicitly) 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 simpli es to 0 = 0. In this case, line 4 of Elim eliminates the equality.
Lemma 11. Let y Dz = c be a satis able 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 diT z = ci in y Dz = c. Then clearly, yi diT z = ci will be eliminated when we call Elim with yi diT z = ci in line 3 of Subst. Therefore, the empty set is the output of both Subst(y Dz = c; yi diT 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.
of EqualityBasis(Ax b be a satis able system of inequalities. Let y b). Then y Dz = c is an equality basis of Ax Dz = c be the output b.
Proof. Let A0z 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 A0z 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 h0T z = g0, where h0 6= 0. This also implies that (A0z b0) [ (h0T z = g0) is the output of Subst(y Dz = c; (Ax b) [ (hT x = g)). By Lemma 10, A0z b0 and (A0z b0) [ (h0T z = g0) are equivalent. Therefore, A0z b0 implies the equality h0T z = g0, which contradicts the condition in line 4 of EqualityBasis and, therefore, our initial assumptions. 5
Through Lemmas 7 & 8, we have presented a method that e ciently 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 simpli es 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 nd, isolate, and eliminate implied
equalities [
Our methods do not require optimization, which SMT solvers are usually not ne-tuned for. Furthermore, we have de ned 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-andbound representation used in Dutertre and de Moura's version of the simplex algorithm (see Appendix B). Finally, our method e ciently 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 [
It is also possible to transform our system of inequalities A0x0 b0 into this tableau-andbound 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 nding equalities aiT x = bi to nding 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 implementation of our methods. For example, we do not have to explicitly eliminate variables via substitution. As mentioned in Section 3, the speci cs of the implementation will also contain justi ed simpli cations 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 [
The authors would like to thank the anonymous reviewers for their valuable comments, suggestions, and for directing us to related work. A
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 [
The simplex algorithm accepts only linear arithmetic systems that are de ned 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 2 Q for variable xj , then we simply set lj = 1. Similarly, if there is no upper bound uj 2 Q for variable xj , then we simply set uj = 1.
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 de ned by
the equalities Ax s = 0, and the bounds 1 xj 1 for every original variable xj and the
bounds 1 si bi for every slack variable introduced for the inequality aiT 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 aiT x bi
and aiT x ci can be transformed into the equality aiT x si = 0 and the bounds ci si bi.
For more details on these simpli cations we refer to [
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 de ne the basic variables over a tableau derived from our system of equalities. Each row in this tableau represent one basic variable xi 2 B: xi = Pxj2N aij xj . The simplex algorithm exchanges variables from xi 2 B and xj 2 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 nd an assignment that maps every variable xi to a value (xi) 2 Q that satis es our constraint system, i.e., A( (x)) = 0 and li (xi) ui for every variable xi. The algorithm starts with an assignment that ful ls A( (x)) = 0 and lj (xj ) uj for every non-basic variable xj 2 N . Initially, we get such an assignment through our tableau. We simply choose a value lj (xj ) uj for every non-basic variable xj 2 N and de ne the value of every basic variable xi 2 B over the tableau: (xi) := Pxj2N aij (xj ). As an invariant, the simplex algorithm will continue to ful l A( (x)) = 0 and lj (xj ) uj for every non-basic variable xj 2 N and every intermediate assignment .
The simplex algorithm nds a satis able assignment or an explanation of unsatis ability through the Check() algorithm (Figure 4). Since all non-basic variables ful l 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 satis able assignment and Check() can return true. If Check() nds a basic variable xi that violates one of its bounds, then it looks for a non-basic variable xj it can pivot with. We ful l 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 con ict. Hence, Check() has found a row that explains the con ict and it can return unsatis able.
Algorithm 4: pivot(xi; xj )
Input : A basic variable xi and a non-basic variable xj so that aij is non-zero
E ect : Transforms the tableau so xi becomes non-basic and xj basic 12 LWeet rxeiw=ritPekth2iNs aroikwxkasbxejt=he ar1iojwxide Pnikn2gNtnhfexjbgaasaiiickj xvkarsiaobiltedxei nes xj instead 3 foreach xk 2 N n fxj g do ajk := aaiikj ; 4 aji := a1ij 5 Then, we substitute xj in all other rows with a1ij xi 6 for xl 2 B do 7 foreach xk 2 N n fxj g do alk := alk + alj ajk; 8 ali := alj aji; alj := 0 9 end 10 N = (N [ fxig) n fxj g; B = (B [ fxj g) n fxig
P k2N nfxjg aaiikj xk Input : A non-basic variable xj and a value v 2 Q
E ect : Sets the value (xj ) of xj to v and updates the values of all basic variables 1 foreach xi 2 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 2 Q E ect : Pivots variables xi and xj and updates the value (xi) of xi to v 1 := v ai(jxi) 2 (xi) := v; (xj ) := (xj ) + 3 foreach xk 2 B n fxig do (xk) := (xk) + akj ; 4 pivot(xi; xj )
Output : Returns true i there exists a satis able assignment for the tableau and the bounds u and l; otherwise, it returns (false,xi), where xi is the con icting 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 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 ful lling the conditions for pivoting.
B
An equality basis for a satis able 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 simpli es to a tableau and a set of tightly bounded variables, i.e., (xj) := lj or (xj) := uj for all satis able assignments . Therefore, one way of determining an equality basis is to nd all tightly bounded variables.
To nd 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 nd all bounds lj xj (xj uj) that hold tightly for all satis able assignments , and then turns them into explicit equalities by setting uj := lj (lj := uj). But rst of all, FindTightBounds() determines if our constraint system is actually satis able with a call of Check(). If the system is unsatis able, then it has no solutions and, therefore, implies all equalities. In this case, FindTightBounds() stops an returns false.
Otherwise, we get a satis able 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 satis able 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 nonbasic variables xj with non-zero coe cient aij also have tight bounds lj = uj. However, in this case the complete row xi = Pxj2N aijxj simpli es to xi = li, so it will never produce a con ict 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 coe cient 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 xing 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 di erence 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()
E ect : 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 2 B [ N do 2 if (xk) > lk then lk := 1; 3 if (xk) < uk then uk := +1; 4 if (xk) = pk + qk such that qk 6= 0 then lk := 1; uk := 1; 5 end 6 for xi 2 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 2 B [ N do 13 if lk < uk then 14 if lk 6= 1 then lk := lk + ; 15 if uk 6= +1 then uk := uk ; 16 if lk 6= 1 and xk 2 N then update(xk; lk); 17 if uk 6= +1 and xk 2 N then update(xk; uk); 18 end 19 end
Algorithm 9: FixEqualities(xi)
Input : A basic variable xi that explains the con ict
E ect : Turns the bounds of all variables responsible for the con ict into equalities 1 for xj 2 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()
E ect : Finds as many tightly bounded variables as possible
Output : false i the system of linear arithmetic constraints is unsatis able 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 original constraint system. Hence, we can continue with other computations on the tableau without losing our equality basis.
The algorithm FindTightBounds() terminates because every call to FixEqualities(xi) simpli es the row xi = Pxj2N aijxj 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 = g. The algorithm substitutes all basic variables xi in hT x = g with their row de nition Pxj2N aijxj. 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 simpli es 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.