Simplification of Presburger formulas in practice I have formulas in 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&gt;=-1, p&lt;q, y&gt;=q, y&lt;n, n&gt;=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)
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$.)

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 and the project's homepage. 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.)

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.