SPASS-IQ: A LA theory solver for SPASS

SPASS-IQ is a linear arithmetic solver specifically constructed as a theory solver for SPASS. It is especially fine tuned to efficiently handle subsumption and constraint refutation tests. The underlying algorithm is a branch-and-bound approach that uses the dual simplex algorithm proposed by Dutertre et al. [5]. Instead of focusing on non-chronological backtracking, as done by most branch-and-bound solvers of the SMT community, SPASS-IQ focuses on a dedicated branch selection strategy. This gives our solver the advantage of a better informed search and, together with a high rate of preprocessing and the use of a reliable rounding heuristic, SPASS-IQ is competitive with theory solvers found in state-of-the-art SMT solvers.

We extended SPASS-IQ with a subroutine called the unit cube test. This test is sound and efficiently finds solutions for many problems - including nearly one thousand problems from the SMT-LIB benchmarks. The test is based on the following three observations:

1. Every unit cube - i.e., a hypercube of edge length one that is parallel to the coordinate axes - contains an integer point.
2. The real solutions of a set of linear arithmetic constraints define a polyhedron.
3. It only takes polynomial time to determine whether a polyhedron contains a unit cube.

To summarize: finding a unit cube inside a polyhedron and thereby guaranteeing an integer solution is by far easier than computing an integer solution directly (P vs. NP). Therefore, it is favorable to first look for a unit cube before starting the complete branch-and-bound approach - which is exactly what the unit cube test does inside SPASS-IQ.

For more details on the unit cube test and detailed experiments see [2]. The unit cube test is by default turned on in SPASS-IQ.

We extended SPASS-IQ with the preprocessing transformations called the Double-Bounded reduction and the Mixed-Echelon-Hermite transformation. If SPASS-IQ encounters a constraint system A x <= 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 A x <= 0 [1]. 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 equisatisable 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 [2] 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. Rational conflicts are also converted between the two systems.

For more details on the Double-Bounded reduction and the Mixed-Echelon-Hermite transformation and detailed experiments see [3]. The transformations are by default turned on in SPASS-IQ.

As input format, SPASS-IQ uses the SMT-LIB language v2. However, we currently restrict ourselves to conjunctions of linear arithmetic inequalities and equalities because SPASS-IQ is only a theory solver and not a complete SMT solver.

Most recent version:

SPASS-IQ v 0.2   (Linux 64 bits AMD/Intel)

Old versions:

SPASS-IQ v 0.1  (Linux 64 bits AMD/Intel)

Benchmarks tested in "Fast Cube Tests for LIA Constraint Solving" [2]:

• CAV-2009 designed by Dillig et al. [4]
• dillig designed by Dillig et al. [4]
• prime-cone "a group of crafted benchmarks encoding a tight n-dimensional cone around the point whose coordinates are the first n prime numbers" [7]
• slacks the dillig benchmarks extended with slack variables [7]
• rotate the dillig benchmarks extended by four inequalities that describe a slightly rotated square [3]

Benchmarks tested in "A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems" [3]:

• UnbdLIB the partially unbounded, linear integer benchmarks from the SMT-LIB
• SlackedQFLIA are linear integer benchmarks based on the SMT-LIB benchmark classes CAV-2009 [4], cut_lemmas [6], and dillig [4], in which we replaced  all variables x with x₊ - x_- where x₊ and x_- are two new variables such that x₊, x_- >= 0.
• RandomUnbd are linear integer benchmarks that are all partially unbounded and satisfiable. All problems are randomly created via a sagemath script. The input parameters are n, number of variables in the problem; m, number of inequalities in the problem; a, maximum absolute value of any randomly generated number; and d, the density of any randomly created matrix or vector. (The benchmarks we created are 125 problems with a=4, d=0.75, and (n,m) \in {(10,15),(25,30),(50,55),(75,83),(100,110)}) Based on these parameters, each problem is constructed as follows:
  1. We randomly create n-1 rows. (This guarantees that at least one direction is unbounded.)
  2. We create m-n+1 linear negative combinations of these rows. (This guarantees that some of the inequalities will be bounded.) The result is an m x n coefficient matrix A.
  3. We create two random integer vectors v and s and set b such that A v + s = b. (This guarantees that A x <= b has an integer solution.)
  4. We test whether A x <= b is too easy, i.e:
     • A x = b has an integer solution.
     • contains a unit cube
  5. If A x <= b is too easy, then we go back to 3. and compute a new candidate b. Otherwise, A x <= b is returned.
• FlippedQFLIA and FlippedRandomUnbd: are linear mixed benchmarks that are all partially unbounded.They are based on the unsatisfiable instances from SlackedQFLIA and all of the instances from 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.
• Results of the tests

Please contact us for help, general questions, bug reports, etc.