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.

Downloads

Most recent version:

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]

Contacts

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

References

[1] M. Bromberger and C. Weidenbach. Fast Cube Tests for LIA Constraint Solving. Work in progress.

[2] I. Dillig, T. Dillig, and A. Aiken. Cuts from proofs: A complete and practical technique for solving linear inequalities over integers. In A. Bouajjani and O. Maler, editors, Computer Aided Verification, volume 5643 of Lecture Notes in Computer Science, pages 233–247. Springer Berlin Heidelberg, 2009.

[3] B. Dutertre and L. de Moura. A fast linear-arithmetic solver for dpll(t). In T. Ball and R. B. Jones, editors, Computer Aided Verification, volume 4144 of Lecture Notes in Computer Science, pages 81–94. Springer Berlin Heidelberg, 2006.

[4] D. Jovanović; and L. de Moura. Cutting to the chase. Journal of Automated Reasoning, 51(1):79–108, 2013.