Decision Procedures for Presburger Arithmetic

Note: This post will be edited as I learn more.

One of the results of Gödel's Incompleteness Theorem is that deciding the validity of arbitrary mathematical formulas is impossible. Here, deciding the validity means telling if "1 < 2" is true or false. Of course, the impossibility result is for arbitrary mathematical formulas and not for simple equalities and inequalities. If we could somehow restrict ourselves to simple formulas (which arise in practice), we might get a complete decision procedure.

Presburger Arithmetic is a first-order theory of natural numbers with addition. Though it doesn't support division amongst other things, it's of interest because it is decidable. Again, decidability means that we can build machines (or algorithms - doesn't make any difference) which, given a Presburger formula, correctly return "true" or "false" but never say "don't know".

Michael Norrish of ANU gives an overview of two such algorithms: Fourier-Motzkin Variable Elimination and Omega Test. John Harrison of Intel has provided a library of OCaml functions for automated theorem proving, which includes Cooper's algorithm.

I'll briefly cover how to use John Harrison's library and Omega Test as part of your system. My interest is in checking if a list of linear constraints has a solution or not. As an example, we'll see how to use these libraries to check

exists y. y > 2 && y < 50;

John Harrison's OCaml Library

You need OCaml to interactively run or build an executable of this library. Unzip and un-tar the archive and build using "make." Once you have done that, you can run a set of examples by running "./example" built by the make process.

The .ml files in the package are dependent on each other. It's not easy to take a fragment out of it and compile that separately (unless you are a good Caml programmer). But you don't need to take out the needed fragments, either. You can make your own example file (example.ml) and re-build using "make." In my case, I changed example.ml to:

open Atp;;
open Format;;

let print_formula fm = formula_printer print_atom fm; print_newline();;
let result = integer_qelim << exists x. x > 2 /\ x < 50 >> in
print_formula result

If I run "./example" I get <<true>> at the console. Unfortunately, no documentation is available but there are several examples in the .ml files that can give you insight into how to use it.

There are several ways to integrate it with your software. The ugliest one is to write an example.ml that reads formulas from a text file (generated by your software) and invokes integer_qelim on it. The result can be written back to an output file. If you are using Java, you might be interested in CamlJava which provides an interface between Java and Caml using JNI and extern. I might try that out and post my experience.

Omega Test

I could compile Omega only with gcc 2.95 on a Solaris box. The later versions of gcc give errors. The project also seems to be abandoned but it's widely quoted at different places. You can get release 1.2 from here. Follow the following steps to compile:

make depend
make libomega.a
make libuniform.a
make libcode_gen.a
make oc

Omega works on sets and relations. The compiled executable (called Omega Calculator) can be found in omega/omega_calc/obj. It's built on top of Omega Library. Instead of using the calculator, you can invoke the library from your code as well, as this interface document explains.

I created a test.txt file with the following contents:

S := {[i] : i <= 50};
T := {[j] : j >= 20};

S intersection T;

And I could run the calculator on this file ("./oc test.txt") and get the following output:

Omega Calculator v1.2 (based on Omega Library 1.2, August, 2000):
# S := {[i] : i <= 50};
#
# T := {[j] : j >= 20};
#
# S intersection T;

{[In_1]: 20 <= In_1 <= 50}

As you can see the constraints have been combined. If they were unsatisfiable (such as contradictory constraints) you would have gotten:

Omega Calculator v1.2 (based on Omega Library 1.2, August, 2000):
# S := {[i] : i >= 50};
#
# T := {[j] : j <= 20};
#
# S intersection T;

{[In_1]: FALSE}

I hope there is a way of getting a "witness" back from these decision procedures.