Institute for Computer Languages
Compilers and Languages Group

Bound Propagation

The bound propagation tool is implemented using the infrastructure of the first-order theorem prover Vampire. The goal of bound propagation is to solve linear rational arithmetic (LRA) problems, using the algorithm proposed by Konstantin Korovin and Andrei Voronkov. [1]

The tool takes as input problems written in either SMT-LIB syntax or MIPLIB (mps files).

Binary can be downloaded from here: Vampire

Tool Manual and Usage:

A short manual on the tool usage, together with its options can be found here

Benchmarks

See the examples to try Bound Propagation using Gorilla.

See this smtlib problems if you want to test the solver on hard smtlib problems.

See this if you are interested in some examples of miplib problems. Upon request, we provide them also in smtlib format.

References

[2] Bound Propagation for Arithmetic Reasoning in Vampire, Ioan Dragan, Konstantin Korovin, Laura Kovacs, Andrei Voronkov (SYNASC 2013) (preprint [pdf])

[1] Bound propagation is based on the technique presented here for solving systems of linear inequalities.

LICENCE