Mjollnir, a tool for quantifier elimination over linear inequalities

Quantifier elimination

Mjollnir implements various quantifier eliminations algorithms for the theory of real (or rational) linear arithmetic:

• Option --action qelim-fr: Ferrante and Rackoff's algorithm substituting a finite disjunction over a family of witnesses (of quadratic length) for the existential quantification (Jeanne Ferrante and Charles Rackoff, A Decision Procedure for the First Order Theory of Real Addition with Order, SIAM Journal on Computing, vol 4 nr 1, 1975, pp. 69-76).
• Option --action qelim-lw: Loos and Weispfenning's virtual substitution algorithm with a linear length family of witnesses (Rüdiger Loos and Volker Weispfenning, Applying linear quantifier elimination, The Computer Journal, vol 36 nr 5, 1993, pp. 450-462)
• Default option --action qelim-m: my algorithm based on SMT-solving and polyhedral projection, yielding DNF formulas (David Monniaux, A Quantifier Elimination Algorithm for Linear Real Arithmetic, LPAR 2008, to appear in LNCS, Springer

Mjollnir is available here:

• Version 2009-07-10: source and x86 binaries

Mjollnir uses SRI Yices for SMT-solving. You'll need libyices.so to compile and run it.

According to a February 4 decision by CNRS' administration, Mjollnir is to be distributed under the GPL-compatible CeCILL license (I had begun doing the paperwork in November). More information will be posted here when available.

SMT-solving

Prior to writing Mjollnir, I wrote two hackish SMT-solvers as “proofs of concept”:

• The first one, written in Caml, also implements a version of the quantifier elimination procedure found in Mjollnir. The input syntax is a subset of Mathematica syntax. The SMT solving uses a fully lazy approach (theory conjunctions are tested after full SAT). The theory conjunctions are tested using the Parma Polyhedra Library (PPL), which you'll need to install, and the SAT part is handled by MiniSAT (no need to download it separately).
• The second one, written in C++, only implements SMT with a SMT-LIB input syntax (input parser based upon the kind indications of Bruno Dutertre). The theory part is again handled by PPL, and the SAT part again by MiniSAT, but the theory checker is now integrated more tightly into the prover, which results in better performance. It's still very far from state-of-the-art solvers such as Yices.

These tools are no longer much maintained. PPL implements a really inefficient emptyness testing algorithm. I hope to replace it with a fast incremental simplex code.