=Paper=
{{Paper
|id=Vol-1617/paper2
|storemode=property
|title=Computing a Complete Basis for Equalities Implied by a System of LRA Constraints
|pdfUrl=https://ceur-ws.org/Vol-1617/paper2.pdf
|volume=Vol-1617
|authors=Martin Bromberger,Christoph Weidenbach
|dblpUrl=https://dblp.org/rec/conf/cade/BrombergerW16a
}}
==Computing a Complete Basis for Equalities Implied by a System of LRA Constraints==
https://ceur-ws.org/Vol-1617/paper2.pdf
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.