From: Marko Kääramees <Marko.Kaaramees@tt...>  20091118 13:18:49

Thomas, thank you for the insight. marko Dr. Thomas Sturm wrote: > Am 16.11.2009 um 17:25 schrieb Marko Kääramees: > > >> Hi, >> >> I use Reduce and its package Redlog for simplifying the boolean >> combination of linear inequalities. I found that some quite obvious >> simplifications work only one way in the redlog. An example script >> >> load_package redlog; >> rlset pasf; >> c := (x = 1 or x >= 2) and (x = 6 or x <= 5); >> rlsimpl c; >> >> simplifies to >> >> x  1 >= 0 and (x  5 <= 0 or x  6 = 0) >> >> The first disjunction with >= is simplified, but the other with <= is >> not. Could somebody explain the reasons please or guide if it can be >> tuned somehow. >> > > This indeed puzzled me at first glance. In fact there is no simplification at all implemented that would discover this situation. What happens is the following (I am simplifying a bit): > > The atomic formula simplifier has some odd policy about deciding between strict (i.e., ">", "<") and weak (i.e. ">=", "<=") orderings to represent certain constraints. That might be tuned to support the quantifier elimination; I would have to look into that in more detail. > > Now x>=2 internally becomes x>1, and "x=1 or x>1" is something obvious to contract by literal comparison of terms. In contrast, x<=5 is *not* turned into x<6, and the possible simplification is not recognised. > > >> I am working in the finite domains (bounded integers) and >> generate lots of combinations of linear inequalities automatically, >> which should be simplified and converted to a normal form to handle >> complexity. >> >> Although Redlog seems to do exactly what I need, it is not too difficult >> to get to the situation where the system eats up all the memory or does >> not seem to finish the computation any time soon. Redlog seems to be >> quite general tool accepting more complex arithmetics and formulas. >> > > Recall that Presburger arithmetic is triply exponential (lower bound on size of the output and thus also on time). > > >> >> Could anybody point to some other tool which seems to be more suitable >> for such tasks? >> > > If you do not use any addition, then software focussing on on discrete orderings might be more efficient. Redlog does not offer this at present. > > 