## reduce-algebra-developers — Discussion of development, administration and support for Reduce

You can subscribe to this list here.

 2009 2010 2011 2012 2013 2014 2015 Jan (2) Feb (5) Mar Apr May (2) Jun (8) Jul (4) Aug Sep Oct (2) Nov (6) Dec Jan (1) Feb (1) Mar (3) Apr (2) May (2) Jun (2) Jul (18) Aug (13) Sep (7) Oct Nov Dec (2) Jan Feb (11) Mar Apr (4) May Jun (1) Jul (18) Aug (16) Sep (12) Oct (12) Nov (19) Dec (42) Jan (16) Feb (3) Mar (8) Apr (14) May (30) Jun (5) Jul (7) Aug (3) Sep (10) Oct (4) Nov (10) Dec (1) Jan (14) Feb (8) Mar (5) Apr (3) May (9) Jun (19) Jul Aug (27) Sep (5) Oct (18) Nov (12) Dec (8) Jan (5) Feb (8) Mar (20) Apr (22) May (28) Jun (9) Jul (6) Aug (46) Sep (40) Oct (15) Nov (8) Dec (34) Jan (20) Feb (15) Mar (18) Apr (20) May (3) Jun (13) Jul (8) Aug Sep Oct Nov Dec
S M T W T F S
1

2

3

4

5

6

7

8

9

10

11

12
(2)
13

14

15

16
(3)
17

18
(1)
19

20

21

22

23

24

25

26

27

28

29

30

Showing 1 results of 1

 Re: [Reduce-algebra-developers] Simplification of inequalities usingredlog From: Marko Kääramees - 2009-11-18 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. > > ```

Showing 1 results of 1