# SPASS-IQ: A LIA theory solver for SPASS

SPASS-IQ is a linear integer 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. [3]. 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.

# Fast Cube Test

We recently extended SPASS-IQ with a new 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 [1]. The unit cube test is by default turned on in SPASS-IQ. To turn it off just add the option -UnitCubes = 0

# Input Format

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

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

# Benchmarks

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

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