Craig Interpolation for Presburger Arithmetic in OpenSMT

In the context of our LPAR paper on interpolation in Presburger arithmetic, we have implemented a version of the open-source SMT solver OpenSMT that can extract Craig interpolants from unsatisfiable problems in quantifier-free Presburger arithmetic.

Note that this is not an official version of OpenSMT, and that the implementation is not maintained anymore. Do not call it "OpenSMT" in publications! If you are searching for stable interpolating SMT solvers, you might rather consider tools like Princess or MathSAT.

You can currently download binaries for Linux (on 32-bit and 64-bit x86 platforms):

Because our implementation is based on a development version of OpenSMT, we only provide the source code on request.

After unpacking any of the packages from above, you can change into the directory opensmtint_x86_* and start OpenSMT by calling ./opensmt <filename>. Given an unsatisfiable problem in the QF_LIA logic (that is partitioned as demonstrated in the examples/ directory), OpenSMT will write interpolants to the file inter.smt.

Experimental Evaluation

We have compared the performance of our interpolation procedure with the following tools:

The benchmarks for our experiments are derived from different families of the SMT-LIB category QF-LIA. Because SMT-LIB benchmarks are usually conjunctions at the outermost level, we partitioned them into A ∧ B by choosing the first 10 · n of the benchmark conjuncts as A, the rest as B (where n is the total number of conjuncts, and k ∈ {1, ... , 9}). This yields 9 interpolation problems for each SMT-LIB benchmark.

Results of the experiments (as an Excel spreadsheet), which were done on an Intel Xeon X5667 4-core machine with 3.07GHz, heap-space limited to 12GB, running Linux, with a timeout of 900s.

Authors