{'fraction_non_alphanumeric': 0.04659320704882176, 'fraction_numerical': 0.01103957740085015, 'mean_word_length': 4.133248596546976, 'pattern_counts': {'":': 0, '<': 12, '<?xml version=': 0, '>': 8, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 9, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems

We present a combination of the Mixed-Echelon-Hermite transformation and the Double-Bounded Reduction for systems of linear mixed arithmetic that preserve satisfiability and can be computed in polynomial time. Together, the two transformations turn any system of linear mixed constraints into a bounded system, i.e., a system for which termination can be achieved easily. Existing approaches for linear mixed arithmetic, e.g., branch-and-bound and cuts from proofs, only explore a finite search space after application of our two transformations. Instead of generating a priori bounds for the variables, e.g., as suggested by Papadimitriou, unbounded variables are eliminated through the two transformations. The transformations orient themselves on the structure of an input system instead of computing a priori (over-)approximations out of the available constants. Experiments provide further evidence to the efficiency of the transformations in practice. We also present a polynomial method for converting certificates of (un)satisfiability from the transformed to the original system.


Introduction
Efficient linear arithmetic decision procedures are important for various independent research lines, e.g., optimization, system modeling, and verification. We are interested in feasibility of linear arithmetic problems in the context of the combination of theories, as they occur, e.g., in SMT solving or theorem proving.
The SMT and theorem proving communities have presented several interesting and efficient approaches for pure linear rational arithmetic [17] as well as linear integer arithmetic [5,7,15,19]. SMT research also starts to extend into linear mixed arithmetic [11,17] because some applications require both rational and integer variables, e.g., planning/scheduling problems and verification of timed automata and hybrid systems.
We are interest in decision procedures for mixed arithmetic because of a possible combination with superposition [1,4,18]. In the superposition context, arithmetic constraints are part of the first-order clauses. The problems are typically unbounded due to transformations that turn the input formula into a superposition specific input format. Since these problems are unbounded, the search space becomes infinite, which is the case where termination becomes difficult for most linear arithmetic approaches. Unbounded problems appear also in other areas of automated reasoning. Either because of bad encodings, necessary but complicating transformations, e.g., slacking (see Section 5), or the sheer complexity of the verification goal. Hence, efficient techniques for handling unbounded problems are necessary for a generally reliable combined procedure.
It is theoretically very easy to achieve termination for linear integer and mixed arithmetic because of so called a priori bounds. For example, the a priori bounds presented by Papadimitriou [21] guarantee that a problem has a mixed solution if and only if the problem extended by the bounds |x i | ≤ 2n(ma) 2m+1 for every variable x i has a mixed solution. In these a priori bounds, n is the number of variables, m the number of inequalities, and a the largest absolute value of any integer coefficient or constant in the problem. By extending a problem with those a priori bounds, we reduce the search space for a branch-and-bound solver (and many other mixed arithmetic decision procedures) to a finite search space. So branch-and-bound is guaranteed to terminate.
However, these bounds are so large that the resulting search space cannot be explored in reasonable time for many practical problems. One reason for the impracticability of a priori bounds is that they only take parameter sizes into account and not actually the structure of each problem. A priori bounds are not integrated in any state-of-the-art SMT solvers [3,12,13,14,16] since they are no help in practice. As far as we know, none of the state-of-the-art SMT solvers use any method that guarantees termination for linear integer or mixed arithmetic.
In this paper, we present satisfiability preserving transformations that reduce unbounded problems into bounded problems. On these bounded problems, most linear mixed decision procedures become terminating, which we show on the example of branch-and-bound. Our reduction works by eliminating unbounded variables. First, we use the Double-Bounded reduction (Section 4) to eliminate all unbounded inequalities from our constraint system. Then we use the Mixed-Echelon-Hermite transformation (Section 3) to shift the variables of our system to ones that are either bounded or do not appear in the new inequalities and are, therefore, eliminated. With Corollary 14 & Lemma 22 we explain how to efficiently convert certificates of (un)satisfiability between the transformed and the original system. Our method is efficient because it is fully guided by the structure of the problem. This is confirmed by experiments (Section 5). We also show how to efficiently determine when a problem is unbounded (Lemma 19). This prevents our solver from applying our transformations on bounded problems.
In Appendix A of this paper, we explain how to implement the presented procedures in an incrementally efficient way. This is relevant for an efficient SMT implementation.
The original version of this paper has been accepted by IJCAR 2018 and will be published by Springer as part of the Lecture Notes of Computer Science Series.
Lemma 1 (Farkas' Lemma [6]). Q(Ax ≤ b) = ∅ iff there exists a y ∈ Q m with y ≥ 0 m and y T A = 0 n so that y T b < 0, i.e., there exists a non-negative linear combination of inequalities in Ax ≤ b that results in an inequality y T Ax ≤ y T b that is constant and unsatisfiable. If such a y exists, then we call it a certificate of unsatisfiability.
We also frequently use the following lemma, which is just a reformulation of Farkas' Lemma: , there exists a non-negative linear combination of inequalities in Ax ≤ b that results in the inequality h T x ≤ g.
As we mentioned in the introduction, this paper describes equisatisfiable transformations for constraint systems. We transform the systems in such a way that most linear mixed decision procedures become terminating and still retain their general efficiency. We even show this on the example of branch-andbound. Although we do not have the time to discuss all facets of branch-andbound [22], we still want to give a short summary of the algorithm. Branchand-bound is a recursive algorithm that computes mixed solutions for constraint systems. In each call of the algorithm, it first computes a rational solution s to a constraint system Ax ≤ b 4 . If there are none, then we know that Ax ≤ b has no mixed solution. We are also done in the case that s is a mixed solution. Otherwise, we select one of the integer variables x i assigned to a fractional value s i ∈ Z and call branch-and-bound recursively on (Ax ≤ b) ∪ (x i ≥ s i ) and (Ax ≤ b) ∪ (x i ≤ s i ). If none of the recursive calls returns a mixed solution, then Ax ≤ b also does not have a mixed solution. Likewise, if one of them returns a mixed solution s, then it also is a mixed solution to Ax ≤ b.
Branch-and-bound alone is already complete on bounded constraint systems, i.e., systems where all directions are bounded: Figure 1a for an example.) Figure 1b for an example.) For bounded systems, branch-and-bound is one of the most popular and efficient algorithms. It may, however, diverge if the system has unbounded directions. Even so, not all unbounded systems are equally difficult. For instance, a system where all directions are unbounded has always a mixed solution: Lemma 5 (Absolutely Unbounded [9]). If all directions are unbounded in a constraint system Ax ≤ b, then the constraint system has an integer solution.
(See Figure 1c for an example.) In a previous article, we described two cube tests that detect and solve constraint systems with infinite lattice width (another name for absolutely unbounded systems) in polynomial time [9]. The case of absolutely unbounded systems is, therefore, trivial and branch-and-bound can be easily extended so it also becomes complete for absolutely unbounded systems. The actual difficult case is when some directions are bounded and others unbounded. We call these systems partially unbounded. Here, branch-and-bound and most other algorithms diverge or become inefficient in practice. The transformations, which we present, are designed to efficiently handle this subclass of problems.

Mixed-Echelon-Hermite Transformation
Our overall goal is to present an equisatisfiable transformation that turns any constraint system into a system that is bounded, i.e., a system on which branchand-bound and many other arithmetic decision procedures terminate. In this section, we only present such a transformation for a subset of constraint systems, which we call double-bounded constraint systems. We then show in the next section that each constraint system can be reduced to an equisatisfiable doublebounded system. We also show how to efficiently transform a mixed solution from the double-bounded reduction to a mixed solution for the original system.
For such a double-bounded system, we call the bounds u the upper bounds of Dx and the bounds l the lower bounds of Dx. Moreover, we typically write l ≤ Dx ≤ u instead of Dx ≤ u although the lower bounds l are only implicit.
Note that only the inequalities in a double-bounded constraint system are guaranteed to be bounded. Variables might still be unbounded. For instance, in the constraint system 1 ≤ 3x 1 − 3x 2 ≤ 2 both inequalities are bounded but the variables x 1 and x 2 are not. Moreover, the above constraint system is also an example where branch-and-bound diverges. This means that even bounding all inequalities does not yet guarantee termination. So for our purposes, a doublebounded constraint system is still too complex.
This changes, however, if we also require that the coefficient matrix D of our constraint system is a lower triangular matrix with gaps: Definition 7 (Lower Triangular Matrix with Gaps). A matrix A ∈ Q m×n is lower triangular with gaps if it holds for each column j that piv(A, j) > m or that piv(A, j) < piv(A, k) for all columns k with j < k ≤ n, i.e., column j either has only zero entries or all pivoting entries right of j have a higher row index.
A matrix is lower triangular if and only if the row indices of its pivots are strictly increasing, i.e., piv(A, 1) < . . . < piv(A, n). If we also allow it to have gaps, only the row indices of pivots with non-zero columns have to be strictly increasing. Now we get termination for free because of our restrictions: Lemma 8 (Lower Triangular Double-Bounded Systems). Let D ∈ Q m×n be a lower triangular matrix with gaps and l ≤ Dx ≤ u be a double-bounded constraint system. Then each variable x j is either bounded, i.e., l ≤ Dx ≤ u implies that l j ≤ x j ≤ u j or its column in D has only zero entries.
Proof. Proof by induction. Assume that the above property already holds for all variables x k with k < j. Let p = piv(D, j). If p > m, then the column j of D is zero and we are done. If p ≤ m, then the pivoting entry d pj of column j is non-zero. Because of Definition 7 and our induction hypothesis, this also means that each column k with k < j has either a zero entry in row p or the variable x k is bounded by our induction hypothesis, i.e., l ≤ Dx ≤ u implies l k ≤ x k ≤ u k . Since Definition 7 also implies that row p has only zero entries to the right of d pj , the row p has only one unbounded variable with a non-zero entry, viz., x j . This means we can transform the row l p ≤ d T p x ≤ u p into the following two inequalities: l p − j−1 k=1 d pk x k ≤ d pj x j and u p − j−1 k=1 d pk x k ≥ d pj x j , where the variables x k on the left sides are either bounded or d pk = 0. Hence, we can derive an upper and lower bound for x j via bound propagation/refinement [20].
Corollary 9 (BnB-LTDB-Termination). Branch-and-bound terminates on every double-bounded system l ≤ Dx ≤ u where D is lower triangular with gaps.
Our next goal is to efficiently transform every double-bounded system l ≤ Dx ≤ u into an equisatisfiable system that also has a lower triangular coefficient matrix with gaps. We start by defining a class of transformations that do not only preserve mixed equisatisfiability, but are also very expressive.
Definition 10 (Mixed Column Transformation Matrix [11]). Given a mixed constraint system. A matrix V ∈ Q n×n is a mixed column transformation matrix if it is invertible and consists of an invertible matrix V (Q) ∈ Q n1×n1 , a unimodular matrix V (Z) ∈ Z n2×n2 , and a matrix V (M ) ∈ Q n1×n2 such that The formal definition of mixed column transformation matrices may seem anything but intuitive. However, they actually describe a straightforward class of transformations, viz., any combination of mixed equisatisfiable column transformations that can be performed on a matrix A. Mixed equisatisfiable column transformations are either (i) multiplying a column by −1; (ii) the swapping of two columns i, j of the same type, i.e., i, j ≤ n 1 or i, j > n 1 ; (iii) multiplying a rational column j (i.e., j ≤ n 1 ) with a non-zero rational factor; (iv) adding a rational multiple of a column j with j ≤ n 1 to any other column i; and (v) adding an integer multiple of a column j > n 1 to a different column i with i > n 1 . If we perform the same mixed equisatisfiable column transformations that resulted in H from A to an n × n identity matrix, then the transformed identity matrix V is a mixed column transformation matrix and H = AV . We just compacted the column transformations into a matrix. We cannot just use V to redo the column transformations, but we can also use its inverse to undo them: Lemma 11 (Mixed Column Transformation Inversion [11]). Given a mixed constraint system. Let V ∈ Q n×n be a mixed column transformation matrix. Then V −1 is also a mixed column transformation matrix.
This means that each mixed column transformation matrix defines a bijection from (Q n1 × Z n2 ) to (Q n1 × Z n2 ). Hence, they guarantee mixed equisatisfiability: Lemma 12 (Mixed Column Transformation Equisatisfiability [11]). Let Ax ≤ b be a mixed constraint system. Let V ∈ Q n×n be a mixed column transformation matrix. Then every solution y ∈ M((AV )y ≤ b)) can be converted into a solution V y = x ∈ M(Ax ≤ b) and vice versa.
Moreover, the mixed column transformation matrix V also establishes a direct relationship between the linear combinations of the original constraint system and the transformed one: Corollary 14 (Mixed Column Transformation Certificates). Let Ax ≤ b be a constraint system. Let V ∈ Q n×n be a mixed column transformation matrix. Then y is a certificate of unsatisfiability for Ax ≤ b iff it is one for AV z ≤ b. Now we only need a mixed column transformation matrix V for every coefficient matrix A such that H = AV is lower triangular with gaps. One such matrix V is the one that transforms A into Mixed-Echelon-Hermite normal form: where E is an r × r identity matrix (with r ≤ n 1 ), E ∈ Q (m−r)×r , and H ∈ Q (m−r)×n2 is a matrix in hermite normal form, i.e., a lower triangular matrix without gaps, where each entry h piv(H ,j)k in the row piv(H , j) is non-negative and smaller than h piv(H ,j)j ).
The following proof for the existence of the Mixed-Echelon-Hermite normal form is constructive and presents the Mixed-Echelon-Hermite transformation.
Lemma 16 (Mixed-Echelon-Hermite Transformation). Let A ∈ Q m×n be a matrix, where the upper left r × n 1 submatrix has the same rank r as the complete left m × n 1 submatrix. Then there exists a mixed transformation matrix V ∈ Q n×n such that H = AV is in Mixed-Echelon-Hermite normal form.
Proof. Proof from [11] with slight modifications so it also works for singular matrices. We subdivide A into Then we bring A 11 with an invertible matrix V 11 ∈ Q n1×n1 into reduced echelon column form H 11 = (E 0 r×(n1−r) ) = A 11 V 11 , where E is an r × r identity matrix. We get V 11 and H 11 by using Bareiss algorithm instead of the better known Gaussian elimination as it is polynomial in time [2]. 5 Note that the last n 1 − r columns of H 21 = (H 21 0 (m−r)×(n1−r) ) = A 21 V 11 are also zero because all rows in A 21 are linear dependent of A 11 (due to the rank). Next we notice that A 12 0 (n1−r)×n2 = 0 r×n2 so we can reduce the upper right submatrix A 12 to zero by adding multiples of the n 1 columns with rational variables to the n 2 columns with integer variables. However, this also transforms the lower right submatrix A 22 into Finally, we transform this new submatrix H 22 into hermite normal form H 22 via the algorithm of Kannan and Bachem (or a similar polynomial time algorithm). 5 This algorithm also returns a unimodular matrix H 22 V 22 . To summarize: our total mixed transformation matrix is It is not possible to transform every matrix A ∈ Q m×n into Mixed-Echelon-Hermite normal form. We have to restrict ourselves to matrices, where the upper left r × n 1 submatrix has the same rank r as the complete left m × n 1 submatrix. However, this is very easy to accomplish for a system of linear mixed arithmetic constraints l ≤ Ax ≤ u. The reason is that the order of inequalities does not change the set of satisfiable solutions. Hence, we can swap the inequalities and, thereby, the rows of A until its upper left r × n 1 submatrix has the desired form. This also means that there are usually multiple possible inequality orderings that each have their own Mixed-Echelon-Hermite normal form H.
To conclude this section: whenever we have a double-bounded constraint system l ≤ Dx ≤ u, we can transform it (after some row swapping) into an equisatisfiable system l ≤ Hy ≤ u where H = DV is in Mixed-Echelon-Hermite normal form and V y = x. Since H is also a lower triangular matrix with gaps, branch-and-bound terminates on l ≤ Hy ≤ u with a mixed solution t or it will return unsatisfiable (Corollary 9). Moreover, we can convert any mixed solution t for l ≤ Hy ≤ u into a mixed solution s for l ≤ Dx ≤ u by setting s := V t. Hence, we have a complete algorithm for double-bounded constraint systems.

Double-Bounded Reduction
In the previous Section, we have shown how to solve a double-bounded constraint system. Now we show how to reduce any constraint system A x ≤ b to an equisatisfiable double-bounded system l ≤ Dx ≤ u. Moreover, we explain how to take any solution of l ≤ Dx ≤ u and turn it into a solution for A x ≤ b .
As the first step of our reduction, we reformulate the constraint system into a so called split system: . Moreover, we call Ax ≤ b the unbounded part and l ≤ Dx ≤ u the bounded part of the split system.
A split system consists of an unbounded part Ax ≤ b that is guaranteed to have (infinitely many) integer solutions (see Lemma 5) and a double-bounded part l ≤ Dx ≤ u. Any constraint system can be brought into the above form (see Figures 2a-2c for an example). We just have to move all unbounded inequalities into the unbounded part and all bounded inequalities into the bounded part.
Proof. For (i), (ii), and the equivalence, it is enough to move all bounded in- j=1,j =k z j a T j , and use the bounds of the inequalities in Dx ≤ u and Ax ≤ b to derive a lower bound for a T k x: Hence, a T k is bounded in A x ≤ b and we have our contradiction.
The above Lemma also shows that the bounded part of a constraint system is self-contained, i.e., a constraint system implies that a direction is bounded if and only if its bounded part does. The actual difficulty of reformulating a system into a split system is not the transformation per se, but finding out which inequalities are bounded or not. There are many ways to detect whether an inequality is bounded by a constraint system. Most work even in polynomial time. For instance, solving the linear rational optimization problem "minimize has no rational solution, and the optimal lower bound l i for a T i x otherwise. However, it still requires us to solve m linear optimization problems.
A, in our opinion, more efficient alternative is based on our previously presented algorithm for finding equality bases [8]. This is due to the following relationship between bounded directions and equalities:

Lemma 19 (Bounds and Equalities
Symmetrically, Ax ≤ 0 implies that h T x = 0 is equivalent to: there exist a y, z ∈ Q m with y, z ≥ 0 m and y T A = h T = −z T A so that y T 0 m ≤ 0 and z T 0 m ≤ 0. Since u and l only have to exists, we can trivially choose them as u := y T b and l := −z T b. This means that y T b ≤ u, z T b ≤ −l, y T 0 m ≤ 0, and z T 0 m ≤ 0 are all trivially satisfied by any pair of linear combinations y, z ∈ Q m with y, z ≥ 0 m such that y T A = h T = −z T A. Hence, the two definitions are equivalent and our lemma holds. It is easy and efficient to compute an equality basis for Ax ≤ 0 m and to determine with it the inequalities in Ax ≤ b that are bounded [8]. The only disadvantage towards the optimization approach is that we do not derive an optimal lower bound l for the inequalities. This is no problem because only the existence of lower bounds is relevant and not the actual bound values. In a split system (Ax ≤ b) ∪ (l ≤ Dx ≤ u), the unbounded part is actually inconsequential to the rational/mixed satisfiability of the system. It may reduce the number of rational/mixed solutions, but it never removes them all. Hence, We first show this equisatisfiability for the rational case: Lemma 20 (Rational Extension). Let (Ax ≤ b) ∪ (l ≤ Dx ≤ u) be a split system. Let s ∈ Q n be a rational solution to the bounded part l ≤ Dx ≤ u such that Ds = g, where g ∈ Q m2 . Then (Ax ≤ b) ∪ (Dx = g) has a solution s .
Proof. Assume for a contradiction that (Ax ≤ b) ∪ (Dx = g) has no solution. By Lemma 1, this means that there exist a y ∈ Q m1 with y ≥ 0 m1 and z, z ∈ Q m2 with z, z ≥ 0 m2 such that y T A + z T D − z T D = 0 n and y T b + z T g − z T g < 0.
Since Dx = g is satisfiable by itself, there must exist a y i > 0. Now we use this fact to reformulate the equation from which we deduce a lower bound for Note that the bounded part l ≤ Dx ≤ u of a split system can still have unbounded directions (not inequalities). Some of these unbounded directions in l ≤ Dx ≤ u are the orthogonal directions to the row vectors d i , i.e., vectors v j ∈ Z n such that d T i v j = 0 for all i ∈ {1, . . . , m 2 }. This also means that the existence of one mixed solution s ∈ (Q n1 × Z n2 ) and one unbounded direction proves the existence of infinitely many mixed solutions. We just need to follow the orthogonal directions, i.e., for all λ ∈ Z, s = λ·v j +s is also a mixed solution because Figures 2a-2c for an example.) In the next two steps, we prove that Ax ≤ b cannot cut off all of these orthogonal solutions because it is completely unbounded. The first step proves that Ax ≤ b remains absolutely unbounded even if we settle on one set of orthogonal solutions, i.e., enforce Dx = Ds for some solution s.
Lemma 21 (Persistence of Unboundedness). Let (Ax ≤ b) ∪ (l ≤ Dx ≤ u) be a split system. Let s ∈ Q n be a rational solution for l ≤ Dx ≤ u such that Ds = g (with g ∈ Q m2 ). Then all row vectors a i from A are still unbounded in Proof. By Lemma 20, (Ax ≤ b) ∪ (Dx = g) has at least a rational solution s * . Moreover, (Ax ≤ 0) ∪ (Dx = 0) does not imply a T i x = 0 because of Lemma 19 and the assumption that the row vectors a i from A are unbounded in (Ax ≤ b) ∪ (l ≤ Dx ≤ u). In reverse, (Ax ≤ b) ∪ (Dx = g) having a real solution, (Ax ≤ 0) ∪ (Dx = 0) does not imply a T i x = 0, and Lemma 19 prove together that the row vectors a i from A are also unbounded in (Ax ≤ b) ∪ (Dx = g).
The next step proves how to extend the mixed solution from the bounded part to the complete system with the help of the Mixed-Echelon-Hermite normal form and the absolute unboundedness of Ax ≤ b.
Proof. Let g = Ds. Without loss of generality we assume that the upper left r×n 1 submatrix of D has the same rank r as the complete left m 1 ×n 1 submatrix of D. (Otherwise, we just reorder the rows accordingly.) Therefore, there exists a mixed column transformation matrix V such that H = DV is in mixed-echelonhermite normal form (see Lemma 16). By Lemma 12, there exists a mixed vector t ∈ (Q n1 × Z n2 ) such that s = V t and t is a mixed-solution to l ≤ Hy ≤ u as well as Hy = g. Let U be the set of indices with 0 columns in H and B the column indices with bounded variables. Then the equation system (Hy = g) fixes each variable y j with j ∈ B to the value t j because H is lower triangular with gaps. Hence, ((AV )y ≤ b) ∪ (Hy = g) is equivalent to Due to Lemma 21 and 13, all directions are unbounded in (1). This means (1) has an integer solution (Lemma 5) assigning each variable y j with j ∈ U to a t j ∈ Z. (Can be computed via the unit cube test [10]). We extend this solution to all variables y by setting t j := t j for j ∈ B and we have a mixed solution t ∈ (Q n1 × Z n1 ) for ((AV )y ≤ b) ∪ (l ≤ Hy ≤ u). Hence, we have via Lemma 12 a mixed solution s ∈ (Q n1 ×Z n2 ) for (Ax ≤ b)∪(l ≤ Dx ≤ u) with s = V t .

Experiments
We integrated the Double-Bounded reduction and the Mixed-Echelon-Hermite transformation into our own theory solver SPASS-IQ v0.2 6 and ran it on four families of newly constructed benchmarks 6 . Once with the transformations turned on (SPASS-IQ) and once with the transformations turned off (SPASS-IQ-Off ). If SPASS-IQ encounters a system Ax ≤ b that is not explicitly bounded, i.e., where not all variables have an explicit upper and lower bound, then it computes an equality basis for Ax ≤ 0 m . This basis is used to determine whether the system is implicitly bounded, absolutely unbounded or partially bounded, as well as which of the inequalities are bounded. Our solver only applies our two transformations if the problem is partially unbounded. The resulting equisatisfiable but bounded problem is then solved via branch-and-bound. The other two cases, absolutely unbounded and implicitly bounded, are solved respectively via the unit cube test [10] and branch-and-bound on the original system. Our solver also converts any mixed solutions from the transformed system into mixed solutions for the original system following the proof of Lemma 22. Rational conflicts are converted between the two systems by using Corollary 14.
We tried to restrict our benchmarks to partially unbounded problems since we only apply our transformations on those problems. We even found some partially unbounded problems in the SMT-LIB benchmarks for QF LIA (quantifier free linear arithmetic). However, there are not many such benchmarks: only one in CAV-2009, five in cut lemmas, and three in slacks. So we created in addition four new benchmark families: SlackedQFLIA: are linear integer benchmarks based on the SMT-LIB classes CAV-2009 [15], cut lemmas [19], and dillig [15]. We simply took all of the unsatisfiable benchmarks and replaced in them all variables x with x + − x − where x + and x − are two new variables such that x + , x − ≥ 0. This transformation, called slacking, is equisatisfiable and the slacked version of the dillig-benchmarks, called slacked [20], is already in the SMT-LIB. Slacking turns any unsatisfiable problem into a partially unbounded one. Hence, all problems in SlackedQFLIA are partially unbounded. Slacking is commonly used to integrate absolute values into linear systems or for solvers that require non-negative variables [22].
RandomUnbd : are linear integer benchmarks that are all partially unbounded and satisfiable with 10, 25, 50, 75, and 100 variables. All problems are randomly created via a sagemath script 6 .
FlippedQFLIA and FlippedRandomUnbd : are linear mixed benchmarks that are all partially unbounded. They are based on SlackedQFLIA and RandomUnbd. We constructed them by first copying ten versions of the integer benchmarks and then randomly flipping the type of some of the variables to rational (probability of 20%). Some of the flipped instances of SlackedQFLIA became satisfiable.
We compared our solver with some of the state-of-the-art SMT solvers currently available for linear mixed arithmetic: cvc4-1.5 [3], mathsat5-5.1 [13], SMTInterpol 2.1-335-g4c543a5 [12], yices2.5.4 [16], and z3-4.6.0 [14]. Most of these solvers employ a branch-and-bound approach with an underlying dual simplex solver [17], which is also the basis for our own solver. As far as we are aware, none of them employ any techniques that guarantee termination.
SMTInterpol extends branch-and-bound via the cuts from proofs approach, which uses the Mixed-Echelon-Hermite transformation to find more versatile branches and cuts [11]. Although the procedure is not complete, the similarities to our own approach make an interesting comparison. Actually, the Double-Bounded reduction alone would be sufficient to make SMTInterpol terminating since it already builds branches via a Mixed-Echelon-Hermite transformation.
We also compared our solver with the ctrl-ergo solver [5] although it is restricted to pure integer arithmetic. Ctrl-ergo is complete over linear integer arithmetic and uses the most similar approach to our transformations that we found in the literature. It dynamically eliminates one linear independent bounded direction at a time via transformation. The disadvantages of the dynamic approach are that it is very restrictive and does not leave enough freedom to change strategies or to add complementing techniques. Moreover, ctrl-ergo uses this transformation approach for all problems and not only the partially unbounded ones, which sometimes leads to a massive overhead on bounded problems.
For the experiments, we used a Debian Linux cluster and allotted to each problem and solver combination 2 cores of an Intel Xeon E5620 (2.4 GHz) processor, 4 GB RAM, and 40 minutes. The only solver benefiting from multiple cores is SMTInterpol. The plots in Figures 3 and 4 depict the results of the different solvers. In the legends of the plots, the numbers behind the solver names are the number of solved instances. For FlippedQFLIA, there are two numbers to indicate the number of satisfiable/unsatisfiable instances solved. This is only necessary for FlippedQFLIA because it is the only tested benchmark family with satisfiable and unsatisfiable instances. (We verified that the results match if two solvers solved the same problem. 7 ) Although our solver could not solve all problems (due to time and memory limits) it was still able to solve more problems than the other solvers. It was also faster on most instances than the other solvers. In some of the unsatisfiable, partially unbounded benchmarks ctrl-ergo is better than SPASS-IQ. This is due to its conflict focused, dynamic approach. For the same reason, ctrl-ergo is slower on the satisfiable, partially unbounded benchmarks. Only SPASS-IQ, ctrl-ergo, and yices solved all of the ten original SMT-LIB benchmarks that are partially unbounded, though the complete methods were still a lot faster (SPASS-IQ took 23s, ctrl-ergo took 42s, and yices took 1273s). On one of these benchmarks, 20-14.slacks.smt2 from slacks, all other solvers seem to diverge. Another interesting result of our experiments is that relaxing some integer variables to rational variables seems to make the problems harder instead of easier. We expected this for our transformations because the resulting systems become more complex and less sparse, but it is also true for the other solvers. The reason might be that bound refinement, a technique used in most branch-and-bound implementations, is less effective on mixed problems.
The time SPASS-IQ needs to detect the bounded inequalities and to apply our transformations is negligible. This is even true for the implicitly bounded problems we tested. As mentioned before, we do not have to apply our transformations to terminate on bounded problems. This is also the only advantage we gain from detecting that a problem is implicitly bounded. Since there is no noticeable difference in the run time, we do not further elaborate the results on bounded problems, e.g. with graphs.
An actual disadvantage of our approach is that the Mixed-Echelon-Hermite transformation increases the density of the coefficient matrix as well as the absolute size of the coefficients. Both are important factors for the efficiency of the underlying simplex solver. Moreover, SPASS-IQ reaches more often the memory limit than the time limit because it needs a (too) large number of branches and bound refinements before terminating.

Conclusion
We have presented the Mixed-Echelon-Hermite transformation (Lemma 16) and the Double-Bounded reduction (Lemma 18 & Corollary 23). We have shown that both transformations together turn any constraint system into an equisatisfiable system that is also bounded (Lemma 8). This is sufficient to make branch-andbound, and many other linear mixed decision procedures, complete and terminating. We have also shown how to convert certificates of (un)satisfiability efficiently between the transformed and original systems (Corollary 14 & Lemma 22). Moreover, experimental results on partially unbounded benchmarks show that our approach is also efficient in practice.
unsatisfiable. We checked their returned "satisfiable" assignments and they were in fact not correct. We contacted the mathsat and yices teams about the bugs and excluded the supposedly wrong results from the experiments table.
Our approach can be nicely combined with the extensive branch-and-bound framework and its many extensions, where other complete techniques cannot be used in a modular way [5,7]. For future research, we plan to test our transformations in combination with other algorithms, e.g., cuts from proofs, or as a dynamic version similar to the approach used by ctrl-ergo [5]. We also want to test whether our transformations are useful preprocessing steps for select constraint system classes that are bounded.

A Incremental Implementation
Suppose an SMT theory solver has to solve (Ax ≤ b) ∪ (Dx ≤ c). Moreover, the last problem it has solved was (Ax ≤ b). Then we call the run time advantage it gains from having already solved a subset of the problem its incremental efficiency. Since all problems sent to an SMT theory solver are incrementally connected, its incremental efficiency is a major factor in determining its total efficiency. In this Section, we explain how to implement our transformation based approach more incrementally efficient and what limits there are with regard to incremental efficiency. We start our discussion with incrementally efficient implementations of the subcomponents of our procedure: finding bounded inquealities and computing the Mixed-Echelon-Hermite normal form.

A.1 Finding Bounded Inequalities Incrementally
In Section 4, we explained via Lemma 19 that all bounded directions in Ax ≤ b are equalities in Ax ≤ 0 m and vice versa. Based on this fact, we recommend to use the method outlined in [8] to compute an equality basis for Ax ≤ 0 m and to determine with it the inequalities in Ax ≤ b that are bounded.
We also recommend the equality basis method because it is incrementally efficient [10]. This incremental efficiency directly translates to determining bounded inequalities. Since determining the bounded inequalities is the bottleneck of splitting (Section 4), the incremental efficiency also translates to splitting a constraint system.

A.2 Extending the Mixed-Echelon-Hermite Normal Form Incrementally
The Mixed-Echelon-Hermite normal form (MEHNF) can also be computed incrementally efficient. However, the polynomial time algorithms for computing the reduced echelon column form and the hermite normal form are typically less incrementally efficient than the ones based on Gaussian elimination. So to achieve incremental efficiency, we have to accept a worst case exponential run time. Fortunately, the Gaussian based transformations rarely seem to reach their exponential worst case in practice. Our experiments support this assumption since the transformation cost is negligible (if not immeasurable) on all of the tested benchmarks.
where H (k) ∈ Q k×n is in Mixed-Echelon-Hermite normal form and u (k) ∈ Q k , a mixed column transformation matrix V (k) ∈ Q n×n , and an inequality a T k+1 x ≤ b k+1 , where a k+1 ∈ Q n and b k+1 ∈ Q Effect : Extends H (k) y ≤ u (k) by a T k+1 V (k) y ≤ b k+1 and transforms it into Mixed-Echelon-Hermite normal form H (k+1) y ≤ u (k+1) via mixed column transformation operations, which are stored in V (k+1) . H (k+1) has at most one more non-zero column than H (k) and Before we can explain the incrementally efficient version of the Mixed-Echelon-Hermite transformation (see ExtendMEH() in Figure 5)), we need to introduce one final notation: we denote by A (k) the k-th element of a series of matrices.
With the algorithm ExtendMEH(), we incrementally compute the MEHNFs H (k) y ≤ u (k) for the constraint systems A (k) x ≤ b (k) , where A (k) := (a 1 , . . . , a k ) T and b (k) := (b 1 , . . . , b k ) T . As already mentioned in Section 3, it is not possible to transform every matrix A (k) ∈ Q k×n into Mixed-Echelon-Hermite normal form. We have to restrict ourselves to matrices, where the upper left r × n 1 submatrix has the same rank r as the complete left k×n 1 submatrix. This is very easy to accomplish because we are looking at constraint systems A (k) x ≤ b (k) and not just matrices. This means we can simply swap the inequalities in ExtendMEH() works as follows: Initially, our MEHNF H (0) y ≤ u (0) is just the empty set and our transformation matrix V (0) is just the n × n identity matrix. Then we incrementally extend H (k) y ≤ u (k) and V (k) one inequality a T k+1 x ≤ b k+1 at a time by computing (H (k+1) y ≤ u (k+1) , V (k+1) ) := ExtendMEH(H (k) y ≤ u (k) , V (k) , a T k+1 x ≤ b k+1 ). (Note that V (k+1) encompasses all column transformations necessary to transform C (k+1) into H (k+1) .)

Algorithm 2: PivR(k, H)
Input : A row dimension k and a matrix H ∈ Q k×n 1 return If all columns j ≤ n1 in H are 0 k , then 0 is returned. Otherwise, this function returns the largest 0 < j ≤ n1 such that column j in H is not 0 k .

Algorithm 3: PivI(k, H)
Input : A row dimension k and a matrix H ∈ Q k×n 1 return If all columns j > n1 in H are 0 k , then n1 is returned instead.
Otherwise, this function returns the largest n1 < j ≤ n such that column j in H is not 0 k .

Fig. 6. Helper functions
To this end, ExtendMEH() first applies the previous column transformations V (k) to a T k+1 x ≤ b k+1 to get the inequality h T k+1 y ≤ b k+1 (line 1). Next, ExtendMEH() checks whether h T k+1 has any non-zero entries h k+1j in one of the zero columns j of H (k) . If h T k+1 does not have any such entries, then no column transformations are necessary and k+1 fills one of the gaps of H (k) , i.e, has a non-zero coefficient in a zero column of H (k) . In order to resolve this, we have to distinguish between two cases: Case 1: h T k+1 fills a rational gap of H (k) , i.e., there exists a zero column 0 < j ≤ n 1 in H (k) such that h k+1j = 0. In this case, we have to extend H (k) from p − 1 non-zero rational columns to p non-zero rational columns. We do so with the function ExtendR() (Figure 7). ExtendR() first inserts the inequality h T k+1 y ≤ b k+1 at an appropriate position p (line 3), to solve the rank requirements we discussed before. So in the new constraint system (H (k+1) y ≤ u (k+1) ) the inequality h T k+1 y ≤ b k+1 is located in row p. Then ExtendR() swaps column j with column p and uses column operations to eliminate all other coefficients in h T k+1 that have filled gaps in H (k) . The result H (k+1) y ≤ u (k+1) is then again in MEHNF (and V (k+1) is the transformation matrix as specified above). Since all column operations are performed on columns with gaps in H (k) , all inequalities in ). Case 2: h T k+1 fills no rational gap, but an integer gap of H (k) , i.e., there exists a zero column n 1 < j ≤ n in H (k) such that h k+1j = 0. In this case, we have to extend H (k) from p − 1 non-zero integer columns to p non-zero integer columns. We do so with the function ExtendI() (Figure 8). ExtendI() first inserts the inequality h T k+1 y ≤ b k+1 at an appropriate position p (line 2), to solve the rank requirements we discussed before. So in the new constraint system (H (k+1) y ≤ u (k+1) ) the inequality h T k+1 y ≤ b k+1 is located in row p. Then ExtendI() swaps column j with column p and uses column operations to where H (k) ∈ Q k×n is in Mixed-Echelon-Hermite normal form and u (k) ∈ Q k , a mixed column transformation matrix V (k) ∈ Q n×n , an inequality h T k+1 y ≤ b k+1 , where h k+1 ∈ Q n and b k+1 ∈ Q, and a column index j > n1 such that h k+1j = 0 and h (k) ij = 0 for all i ≤ k Effect : Extends H (k) y ≤ u (k) by h T k+1 y ≤ b k+1 and transforms it into Mixed-Echelon-Hermite normal form H (k+1) y ≤ b (k+1) via mixed column transformation operations, which are stored in V (k+1) . H (k+1) has one more non-zero integer column than H (k) and to the constraint system (can be efficiently marked with a flag) to get again (H (k−1) y ≤ u (k−1) ). Since H (i) := C (i) V (k) for all i ≤ k, it is not necessary to change the transformation matrix 10 . Thus, we have found an incrementally and decrementally efficient way to compute the MEHNF of a constraint system.

A.3 The Complete Incremental Procedure
Now that we have incrementally efficient subprocedures, we can describe a version of our complete procedure that is incrementally efficient. As a reminder, the non-incremental version of our total procedure works as follows: Our input is a constraint system Ax ≤ b and we want to find a mixed solution for it. To this end, we first compute the equality basis of Ax ≤ 0 m to find the inequalities and directions in Ax ≤ b that are bounded. Next we do a case distinction depending on whether Ax ≤ b is bounded, absolutely unbounded or partially unbounded. If Ax ≤ b is bounded, we find the mixed solution via branch-and-bound 11 . If Ax ≤ b is absolutely unbounded, we find the mixed solution via the unit cube test [10]. The only slightly complicated case is if Ax ≤ b is partially unbounded.
In this case, we first split Ax ≤ b into a split system and transform the doublebounded part into its MEHNF. The double-bounded system in MEHNF is then solved with branch-and-bound.
Now assume that we have done all of the above for Ax ≤ b, but need to incrementally extend it to (Ax ≤ b) ∪ (A x ≤ b ). This means we want to find a mixed solution for (Ax ≤ b) ∪ (A x ≤ b ). If (Ax ≤ b) was already bounded, then we know that (Ax ≤ b) ∪ (A x ≤ b ) will also be bounded and we simply apply branch-and-bound to it. Otherwise, we have to extend the equality basis of Ax ≤ 0 m to the equality basis of (Ax ≤ 0 m ) ∪ (A x ≤ 0 m ) and use it to find the inequalities and directions in (Ax ≤ b) ∪ (A x ≤ b ) that are bounded. In Section A.1, we have shown how to do this incrementally efficient. Next we do a case distinction depending on whether is now bounded, we find the mixed solution via branch-and-bound.
is still absolutely unbounded, we find the mixed solution via the unit cube test (also an incrementally efficient procedure) [10].
is still partially unbounded, we continue as follows: We still have the split system for (Ax ≤ b) and can now use our extended equality basis for (Ax ≤ 0 m )∪(A x ≤ 0 m ) to efficiently extend it to a split system for (Ax ≤ b) ∪ (A x ≤ b ). Since adding new inequalities can only add bounded directions, the double-bounded part of the extended split system still contains all bounded inequalities from the previous double-bounded part. This means we can incrementally extend the MEHNF l ≤ Hy ≤ u by the new inequalities in the double-bounded part of (Ax ≤ b)∪(A x ≤ b ). In Section A.2, we have shown how to do this incrementally efficient. Finally, we solve the extended double-bounded constraint system (l ≤ Hy ≤ u)∪(l ≤ H y ≤ u ) with branch-and-bound. Since we only add inequalities to the running constraint system (l ≤ Hy ≤ u), we can continue our branchand-bound search incrementally efficient.
This shows that most parts of our procedure can be implemented incrementally efficient. However, there are two limits to the incremental efficiency. First of all, we have to store multiple constraint systems in our memory to stay incrementally efficient: we need one system to store the current equality basis, so we can later extend it; we need one system to store the current MEHNF, so we can later extend it; we need the current transformation matrix of the MEHNF transformation, so we can later extend it; and we need one copy of the MEHNF to perform branch-and-bound on. Secondly, we do not know how to make the assignment/solution conversion incrementally efficient, i.e., how to convert the mixed solution of the transformed system to a mixed solution of the original system in an incrementally efficient way (see Lemma 22 for the non-incremental subprocedure). However, this second limitation is in reality not a problem because there are ways to avoid the conversion until we know that the complete problem is satisfiable. So the conversion is used at most once for each SMT input problem. In the next subsection, we will elaborate why this is the case.

A.4 Avoiding Conversion
In order to explain why we can avoid the conversion, we first have to distinguish the origin of the incrementally connected problems, i.e., the origin of the problems sent from the SMT solver to the SMT theory solver. There are typically two reasons a theory solver might receive incrementally connected problems from the SMT solver: (1) The SMT solver tries to prune some partial models (i.e., conjunctions of literals) that are theory unsatisfiable. This case is actually not necessary for a complete SMT solver 12 . It is just a trick to speed-up the boolean search of the SMT solver. However, it would already be too expensive for the theory solver to check all partial models. Instead, they typically just check partial models when the SAT solver is about to do a decision. And even then the check is often just a sound approximation of the complete theory solver because the complete check is too expensive for some theories. One of those theories is in fact linear (mixed) integer arithmetic. For this theory, most SMT solvers check only the rational relaxation of the partial models for theory satisfiability. So this source of incrementally connected problems is not relevant to our complete approach.
(2) The SMT solver combines multiple theory solvers via the Nelson-Oppen method. As part of the Nelson-Oppen method, (2.1) each theory solver has to first determine the satisfiability of their own conjunctions of literals. (2.2) Then the theory solvers incrementally send to each other (negated) equalities over constant function symbols and test these extended problems for satisfiability. (2.3) This continues until they find a complete and satisfiable equivalence class over the constant function symbols. All of the above can be done with our transformation scheme without converting the intermediate solutions to the original system. However, most SMT solvers rely on the intermediate solutions to the original system to guess the (negated) equalities they send in step (2.2).
At a first glance, case (2) seems like it actually needs the solution conversion via Lemma 22. However, there is an easy and reasonable way to avoid it. Instead of using the intermediate solution to the complete original system, we just use the intermediate solution to the double-bounded part of the original system. This solution can be efficiently computed with the transformation matrix V , i.e., x := V y is the solution to the double-bounded part of the original system if y is the solution to the transformed system. This is a reasonable approximation for the guesses in (2.2) because we know that the unbounded part is irrelevant to the satisfiability of the original system (Corollary 23).
We conclude that our total incremental procedure never has to convert a complete solution more than once. So the procedure should be incrementally efficient in practice. However, we are unable to test this claim with experiments since we only have a working theory solver and not a complete SMT solver with multiple theory solvers.