[gecode-users] Linear expressions in 'post'

[Christian Schulte]

Dear Andrea,

no, there is nothing interesting really. Again, we work with relations
internally and rewrite the expressions into that. The only thing we
currently exploit is associativity, that is, for x & (y & z) we post a
single conjunction propagator rather than two with an additional variable.
Ah right, and we remove duplicates x & x to x.

What we will do for Gecode 3.0 is rewriting the expression into NNF (push
negation in front of variables) so that there will never be a need to have
negation propagator (that is due to the fact that Gecode will have then a
clause propagator for both positive and negative literals).

Cheers
Christian

--
Christian Schulte, www.ict.kth.se/~cschulte/


-----Original Message-----
From: users-bounces at gecode.org [mailto:users-bounces at gecode.org] On Behalf
Of Andrea Rendl
Sent: Monday, August 18, 2008 4:19 PM
To: Christian Schulte
Cc: andrea at cs.st-andrews.ac.uk; users at gecode.org
Subject: Re: [gecode-users] Linear expressions in 'post'

Dear Christian,

Thanks for the quick reply. I have suspected that Peter Stuckey's and
Warwick's paper was somehow involved :)

I've noticed that you also have Boolean expressions
(Gecode::MiniModel::BoolExpr) in 'post'. I haven't done any testing
with them yet, but I'm curious if you apply similar re-write rules on
Boolean expressions?

Thanks again,
Andrea

2008/8/18 Christian Schulte <cschulte at kth.se>:
> Dear Andrea,
>
> what we do is pretty much what you had guessed already, however there are
> two stages of rewriting going on, one for mapping linear expressions into
a
> linear constraint (that is, a relation between linear expressions) and a
> second stage that is done by the functions that post a linear constraint.
>
> Linear expressions are composed as sums and differences of linear terms
a*x
> + c. What happens is that this is turned into a linear constraint of the
> form (of course, this also holds for <=, >=, !=, <, >). So rather than
> creating an expression we create a relation:
>        a_1 * x_1 + ... + a_n * x_n = c
>
> The routines for posting a linear constraint then do some additional
> transformations:
>        a * x + b * x   is rewritten to         (a + b) * x     [must be
> done for better propagation!]
>        0 * x           will be removed
>        if g is the non-trivial gcd of a_1, ..., a_, c then all
coefficients
> are devided by g
>
> All these rewriting steps will check for overflow. After that the routines
> will decide which precision is needed for propagation and will throw an
> exception if propagation might generate an overflow (very important,
> otherwise, constraint propagation would be not sound).
>
> I think that's what most systems do and an important aspect is to deal
with
> relations and not expressions (with expressions you always have the need
for
> intermediate variables where it is difficult to guess a domain for the
> variable so that no overflow occurs). For a discussion of which
> transformations change the propagation behaviour, you could check the
> following paper:
>
> @Article{newprop-journal,
>  author =       {W.~Harvey and  P.J.~Stuckey},
>  title =        {Improving linear constraint propagation by
>                  changing constraint representation},
>  journal =      {Constraints},
>  volume =       {7},
>  pages =        {173--207},
>  year =         {2003},
> }
>
> Please do not hesitate to ask if you have more questions.
>
> Cheers
> Christian
>
> --
> Christian Schulte, www.ict.kth.se/~cschulte/
>
>
> -----Original Message-----
> From: users-bounces at gecode.org [mailto:users-bounces at gecode.org] On Behalf
> Of Andrea Rendl
> Sent: Monday, August 18, 2008 3:15 PM
> To: users at gecode.org; andrea at cs.st-andrews.ac.uk
> Subject: [gecode-users] Linear expressions in 'post'
>
> Dear Gecoders,
>
> I've noticed that Gecode is very effective with solving linear
> expressions (Gecode::MiniModel::LinExpr)  given in the 'post'
> constraint. I was wondering how you deal with them internally. I guess
> you build some kind of expression tree from the linear expression and
> then map the tree to an adequate 'linear' constraint? How do you deal
> with more 'complex' linear expressions that you cannot directly map to
> linear, such as
>
> x + c1 != y + c2                   (where x,y are IntVars and c1,c2
> are constants)
>
> In this case, do you internally re-write the expression to 'x + c1 - y
> != c2' (or similar) to match with linear? If yes, are there any
> particular rules you apply for re-writing? I assume there is no case
> where you flatten any expressions (and introduce auxiliary variables
> internally)? If there exists some published work on it, I'd be happy
> if you could point it out to me.
>
> Thank you,
> Andrea
>
> _______________________________________________
> Gecode users mailing list
> users at gecode.org
> https://www.gecode.org/mailman/listinfo/gecode-users
>
>

_______________________________________________
Gecode users mailing list
users at gecode.org
https://www.gecode.org/mailman/listinfo/gecode-users