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: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] On Behalf Of Andrea Rendl Sent: Monday, August 18, 2008 4:19 PM To: Christian Schulte Cc: [EMAIL PROTECTED]; [EMAIL PROTECTED] 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 <[EMAIL PROTECTED]>: > 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: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] On Behalf > Of Andrea Rendl > Sent: Monday, August 18, 2008 3:15 PM > To: [EMAIL PROTECTED]; [EMAIL PROTECTED] > 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 > [EMAIL PROTECTED] > https://www.gecode.org/mailman/listinfo/gecode-users > > _______________________________________________ Gecode users mailing list [EMAIL PROTECTED] https://www.gecode.org/mailman/listinfo/gecode-users _______________________________________________ Gecode users mailing list [EMAIL PROTECTED] https://www.gecode.org/mailman/listinfo/gecode-users
