<p>Conjunctions of linear arithmetic inequalities can be solved using <a href="http://en.wikipedia.org/wiki/Fourier%E2%80%93Motzkin_elimination" rel="nofollow">Fourier-Motzkin variable elimination</a>, which IIRC has a doubly-exponential worst case complexity. </p>

<p>William Pugh improved upon this algorithm with his Omega test (see <a href="http://www.cs.utexas.edu/~pingali/CS380C/2013/papers/pugh92omega.pdf" rel="nofollow"><em>The Omega Test: a fast and practical integer programming algorithm for dependence analysis</em></a>), which has an exponential worst-case behaviour, but which is apparently polynomial on formulas coming from many common sources (such as compiler loop optimizations). </p>

CC BY-SA 3.0
2014-02-28T21:31:32.037Z
Fourier-Motzkin is for conjunctions of (in)equalities in real/rational linear arithmetic. Here I'm over integers (thus Omega, which is complicated) and I have disjunctions... Note that the double exponential in F-M can be avoided by pruning, see e.g. Fouilhé et al., SAS 2013.http://verasco.imag.fr/wiki/VPL
David Monniaux
CC BY-SA 3.0
2014-03-01T07:29:31.383Z
Let's add that, per se, Fourier-Motzkin does not simplify a system of inequalities. It eliminates existential quantifiers from it, and, if not using pruning, it outputs a very complicated (not simplified at all) system of inequalities.
David Monniaux
CC BY-SA 3.0
2014-02-28T09:38:37.670Z
2014-02-28T09:38:37.670Z
Neel Krishnaswami
<p>Not knowing anything about the input problem, I suspect that if the blow up is coming from quantifier elimination of Presburger formulas. Cooper's algorithm can introduce a lot of redundancies and duplication during case splitting.
My suggestion comes from a trivial observation: Any tool that can find "very simple" Presburger formula also has to be able to find "very simple" pure boolean formulas. (Just encode each propositional variable $x_i$ with some trivial Presburger atom $s_i &lt; 2$.)</p>

<p>BDDs are a fairly natural candidate for trying to get simple formulas (or at least unique wrt a variable order).
The closest work I am aware of to extending BDDs over Presburger is the Linear Decision Diagram (LDD) work of Chaki et al: <a href="http://fmv.jku.at/fmcad09/slides/gurfinkel.pdf" rel="nofollow">slides</a> and the <a href="http://sourceforge.net/apps/trac/lindd" rel="nofollow">project's homepage</a>. Links to the papers are on the project's site.  This work combines linear real/rational arithmetic with BDDs.  The goal of this work was to have a compact representation in order to do Fourier-Motzkin quantifier elimination. Already LDDs do not try to be canonical, just "canonical enough".  The main idea is to add local conditions to eliminate certain kinds of redundancy during construction. These local conditions are things like: put the constraints on $x$ next to each other in the variable order, if $x &lt; 5$, then $x&lt;7$ always holds on the high branch, etc.  They do mention support for UTVPI constraints over integers in the paper and slides (like what you have above). The tool's API does not seem to support divisibility constraints coming from quantifier elimination or other more elaborate kinds of integer specific reasoning (gcd computations, conversion of $x &lt; 2$ to $x \leq 1$, etc.)</p>

<p>If the formulas have a lot of propositional redundancy introduced by quantifier elimination, this might be a reasonable thing to look into.  (I doubt this includes all of the reasoning you used to get down to the smaller formulas so it might not work out of the box.) I've used tricks like BDDs + unate implications (eg. $x &lt; 2 \implies x &lt; 3$) to reduce Presburger formulas that were blown up by a different algorithm to "very simple" equivalent ones. But I did this for debugging purposes only. It has never made sense to stick what I did into a real implementation so I do not have a tool I can point you to. Good luck.</p>

CC BY-SA 3.0
2014-02-28T02:20:10.773Z
2014-02-28T15:31:19.650Z
2014-02-28T15:31:19.650Z
Tim
<p>You may know this, but <a href="http://www.smtlib.org/" rel="nofollow">SMT</a> solvers very often handle "quantifier-free" (implicitly universally quantified) linear arithmetic on integers, and sometimes even formulas with quantifier alternations (though with more limited success).</p>

<p>You might want to try <a href="http://z3.codeplex.com/" rel="nofollow">Z3</a> which performs quite well in practice, using variants of the Omega method referred to above, but with many twists and heuristics. In particular, the <strong>simplify</strong> command (explained <a href="http://rise4fun.com/Z3/tutorial/guide" rel="nofollow">here</a>) seems to do what you want, i.e. simplify formulas to an equivalent form.</p>

CC BY-SA 3.0
2014-02-28T21:32:59.150Z
In fact, I've tried the ctx-solver-simplify tactic in Z3, but the quality of the output seems to depend on factors I don't understand, plus I've hit a bug (which I've signaled to Z3 authors). By the way, Z3 now has quantifier elimination over linear arithmetic (see Phan et al., SMT 2012)
David Monniaux
CC BY-SA 3.0
2014-02-28T22:45:52.763Z
Yes, but only linear arithmetic in the *reals* I believe. You might want to try having finer control with different *strategies* which are definable in Z3, see e.g. this answer to a similar question: http://stackoverflow.com/questions/14220826/optimising-z3-input and, unfortunately, the source code is probably the definitive documentation for tactics: http://z3.codeplex.com/SourceControl/latest#src/tactic/arith/normalize_bounds_tactic.h
cody
CC BY-SA 3.0
2014-03-01T07:32:19.240Z
As far as I know, Z3 implements quantifier elimination for both linear real arithmetic and linear integer arithmetic, the latter with a mixture of Omega and Cooper with some clever representation (see Bjørner, IJCAR 2010, and the above mentioned paper by Phan et al.).
David Monniaux
CC BY-SA 3.0
2014-03-05T16:29:36.253Z
Ok, sorry my bad.
cody
CC BY-SA 3.0
2014-02-28T16:43:46.820Z
2014-02-28T16:49:07.950Z
2014-02-28T16:49:07.950Z
cody
<p>My current best solution is to use the latest version of Z3 (which fixes a bug in simplification) and <code>Repeat(Then(OrElse('split-clause', 'nnf'), 'propagate-ineqs', 'ctx-solver-simplify'))</code>.</p>

CC BY-SA 3.0
2014-03-04T21:50:43.543Z
2014-03-04T21:50:43.543Z
David Monniaux
<p>I have formulas in <a href="http://en.wikipedia.org/wiki/Presburger_arithmetic">Presburger arithmetic</a> (with initial ∀, but I can apply quantifier elimination so they are quantifier-free) that are fairly complicated, yet, in many useful cases, are equivalent to very simple formulas such as conjunctions of simple arithmetic constrains (e.g. <code>p&gt;=-1, p&lt;q, y&gt;=q, y&lt;n, n&gt;=2</code> for a quantified formula taking up a whole screen page).</p>

<p>Is there any good simplification method for such formulas? (preferably in an off-the-shelf implementation)</p>

CC BY-SA 3.0
2014-02-27T22:34:07.447Z
Well, you can go from semilinear sets to (Parikh images of) regular languages and back; do a minimization in between would help?
Michaël Cadilhac
CC BY-SA 3.0
2014-02-27T22:59:52.187Z
It requires double exponential time for decide it in the worst case. Try to see what properties your formulas have (e.g. are they only have one universal quantifier?), there are some parameterized algorithms IIRC.
Kaveh
CC BY-SA 3.0
2014-02-27T23:54:24.400Z
I'm not an expert; recently I tried the omega tactic of Coq, but it is damn slow. After some search I saw the [Talence Presburger Arithmetic Suite](http://tapas.labri.fr/trac), but didn't test/used it yet. Perhpas it can be helpful for you.
Marzio De Biasi
CC BY-SA 3.0
2014-02-28T21:40:56.277Z
Kaveh, to my best remembrance of Fisher & Rabin, the double exponential is incurred because of quantifier alternation. Here, I have a single universal block in front.
David Monniaux
CC BY-SA 3.0
2014-02-28T21:42:40.890Z
Marzio, I'm so silly! I know the author of TaPAS, Jérôme Leroux, and his taste for Presburger!
David Monniaux
<lo.logic>
Simplification of Presburger formulas in practice
David Monniaux
# Simplification of Presburger formulas in practice

(Asked by: username_0 on 2014-02-27)

I have formulas in [Presburger arithmetic](http://en.wikipedia.org/wiki/Presburger_arithmetic) (with initial ∀, but I can apply quantifier elimination so they are quantifier-free) that are fairly complicated, yet, in many useful cases, are equivalent to very simple formulas such as conjunctions of simple arithmetic constrains (e.g. `p>=-1, p=q, y=2` for a quantified formula taking up a whole screen page).

Is there any good simplification method for such formulas? (preferably in an off-the-shelf implementation)

**Tags:** lo.logic

> **Comments:**
> **username_1**: Well, you can go from semilinear sets to (Parikh images of) regular languages and back; do a minimization in between would help?  
> **username_2**: It requires double exponential time for decide it in the worst case. Try to see what properties your formulas have (e.g. are they only have one universal quantifier?), there are some parameterized algorithms IIRC.  
> **username_3**: I'm not an expert; recently I tried the omega tactic of Coq, but it is damn slow. After some search I saw the [Talence Presburger Arithmetic Suite](http://tapas.labri.fr/trac), but didn't test/used it yet. Perhpas it can be helpful for you.  
> **username_0**: username_2, to my best remembrance of Fisher & Rabin, the double exponential is incurred because of quantifier alternation. Here, I have a single universal block in front.  
> **username_0**: Marzio, I'm so silly! I know the author of TaPAS, Jérôme Leroux, and his taste for Presburger!  

---

## 4 answers

### Answer by username_4 on 2014-02-28. Score: 3

Conjunctions of linear arithmetic inequalities can be solved using [Fourier-Motzkin variable elimination](http://en.wikipedia.org/wiki/Fourier%E2%80%93Motzkin_elimination), which IIRC has a doubly-exponential worst case complexity.

William Pugh improved upon this algorithm with his Omega test (see [*The Omega Test: a fast and practical integer programming algorithm for dependence analysis*](http://www.cs.utexas.edu/~pingali/CS380C/2013/papers/pugh92omega.pdf)), which has an exponential worst-case behaviour, but which is apparently polynomial on formulas coming from many common sources (such as compiler loop optimizations).

> **Comments:**
> **username_0**: Fourier-Motzkin is for conjunctions of (in)equalities in real/rational linear arithmetic. Here I'm over integers (thus Omega, which is complicated) and I have disjunctions... Note that the double exponential in F-M can be avoided by pruning, see e.g. Fouilhé et al., SAS 2013.http://verasco.imag.fr/wiki/VPL  
> **username_0**: Let's add that, per se, Fourier-Motzkin does not simplify a system of inequalities. It eliminates existential quantifiers from it, and, if not using pruning, it outputs a very complicated (not simplified at all) system of inequalities.  

---

### Answer by username_5 on 2014-02-28. Score: 3

Not knowing anything about the input problem, I suspect that if the blow up is coming from quantifier elimination of Presburger formulas. Cooper's algorithm can introduce a lot of redundancies and duplication during case splitting.
My suggestion comes from a trivial observation: Any tool that can find "very simple" Presburger formula also has to be able to find "very simple" pure boolean formulas. (Just encode each propositional variable $x\_i$ with some trivial Presburger atom $s\_i < 2$.)

BDDs are a fairly natural candidate for trying to get simple formulas (or at least unique wrt a variable order).
The closest work I am aware of to extending BDDs over Presburger is the Linear Decision Diagram (LDD) work of Chaki et al: [slides](http://fmv.jku.at/fmcad09/slides/gurfinkel.pdf) and the [project's homepage](http://sourceforge.net/apps/trac/lindd). Links to the papers are on the project's site. This work combines linear real/rational arithmetic with BDDs. The goal of this work was to have a compact representation in order to do Fourier-Motzkin quantifier elimination. Already LDDs do not try to be canonical, just "canonical enough". The main idea is to add local conditions to eliminate certain kinds of redundancy during construction. These local conditions are things like: put the constraints on $x$ next to each other in the variable order, if $x < 5$, then $x<7$ always holds on the high branch, etc. They do mention support for UTVPI constraints over integers in the paper and slides (like what you have above). The tool's API does not seem to support divisibility constraints coming from quantifier elimination or other more elaborate kinds of integer specific reasoning (gcd computations, conversion of $x < 2$ to $x \leq 1$, etc.)

If the formulas have a lot of propositional redundancy introduced by quantifier elimination, this might be a reasonable thing to look into. (I doubt this includes all of the reasoning you used to get down to the smaller formulas so it might not work out of the box.) I've used tricks like BDDs + unate implications (eg. $x < 2 \implies x < 3$) to reduce Presburger formulas that were blown up by a different algorithm to "very simple" equivalent ones. But I did this for debugging purposes only. It has never made sense to stick what I did into a real implementation so I do not have a tool I can point you to. Good luck.


---

### Answer by username_6 on 2014-02-28. Score: 2

You may know this, but [SMT](http://www.smtlib.org/) solvers very often handle "quantifier-free" (implicitly universally quantified) linear arithmetic on integers, and sometimes even formulas with quantifier alternations (though with more limited success).

You might want to try [Z3](http://z3.codeplex.com/) which performs quite well in practice, using variants of the Omega method referred to above, but with many twists and heuristics. In particular, the **simplify** command (explained [here](http://rise4fun.com/Z3/tutorial/guide)) seems to do what you want, i.e. simplify formulas to an equivalent form.

> **Comments:**
> **username_0**: In fact, I've tried the ctx-solver-simplify tactic in Z3, but the quality of the output seems to depend on factors I don't understand, plus I've hit a bug (which I've signaled to Z3 authors). By the way, Z3 now has quantifier elimination over linear arithmetic (see Phan et al., SMT 2012)  
> **username_6**: Yes, but only linear arithmetic in the *reals* I believe. You might want to try having finer control with different *strategies* which are definable in Z3, see e.g. this answer to a similar question: http://stackoverflow.com/questions/14220826/optimising-z3-input and, unfortunately, the source code is probably the definitive documentation for tactics: http://z3.codeplex.com/SourceControl/latest#src/tactic/arith/normalize_bounds_tactic.h  
> **username_0**: As far as I know, Z3 implements quantifier elimination for both linear real arithmetic and linear integer arithmetic, the latter with a mixture of Omega and Cooper with some clever representation (see Bjørner, IJCAR 2010, and the above mentioned paper by Phan et al.).  
> **username_6**: Ok, sorry my bad.  

---

### Answer by username_0 on 2014-03-04. Score: 1

My current best solution is to use the latest version of Z3 (which fixes a bug in simplification) and `Repeat(Then(OrElse('split-clause', 'nnf'), 'propagate-ineqs', 'ctx-solver-simplify'))`.


---

