6
$\begingroup$

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>=-1, p<q, y>=q, y<n, n>=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)

Improve this question
$\endgroup$
5
  • 1
    $\begingroup$ Well, you can go from semilinear sets to (Parikh images of) regular languages and back; do a minimization in between would help? $\endgroup$
    – Michaël Cadilhac
    Commented Feb 27, 2014 at 22:34
  • 1
    $\begingroup$ 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. $\endgroup$
    – Kaveh
    Commented Feb 27, 2014 at 22:59
  • $\begingroup$ 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, but didn't test/used it yet. Perhpas it can be helpful for you. $\endgroup$
    – Marzio De Biasi
    Commented Feb 27, 2014 at 23:54
  • $\begingroup$ 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. $\endgroup$
    – David Monniaux
    Commented Feb 28, 2014 at 21:40
  • $\begingroup$ Marzio, I'm so silly! I know the author of TaPAS, Jérôme Leroux, and his taste for Presburger! $\endgroup$
    – David Monniaux
    Commented Feb 28, 2014 at 21:42

4 Answers 4

Reset to default
3
$\begingroup$

Conjunctions of linear arithmetic inequalities can be solved using Fourier-Motzkin variable 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), which has an exponential worst-case behaviour, but which is apparently polynomial on formulas coming from many common sources (such as compiler loop optimizations).

Improve this answer
$\endgroup$
2
  • $\begingroup$ 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.verasco.imag.fr/wiki/VPL $\endgroup$
    – David Monniaux
    Commented Feb 28, 2014 at 21:31
  • $\begingroup$ 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. $\endgroup$
    – David Monniaux
    Commented Mar 1, 2014 at 7:29
3
$\begingroup$

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 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 < 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.

Improve this answer
$\endgroup$
2
$\begingroup$

You may know this, but SMT 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 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) seems to do what you want, i.e. simplify formulas to an equivalent form.

Improve this answer
$\endgroup$
4
  • 1
    $\begingroup$ 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) $\endgroup$
    – David Monniaux
    Commented Feb 28, 2014 at 21:32
  • $\begingroup$ 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: stackoverflow.com/questions/14220826/optimising-z3-input and, unfortunately, the source code is probably the definitive documentation for tactics: z3.codeplex.com/SourceControl/latest#src/tactic/arith/… $\endgroup$
    – cody
    Commented Feb 28, 2014 at 22:45
  • 2
    $\begingroup$ 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.). $\endgroup$
    – David Monniaux
    Commented Mar 1, 2014 at 7:32
  • $\begingroup$ Ok, sorry my bad. $\endgroup$
    – cody
    Commented Mar 5, 2014 at 16:29
1
$\begingroup$

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')).

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.