[gecode-users] BoolExpr example

[Mikael Zayenz Lagerkvist]

On Thu, Nov 20, 2008 at 7:52 AM, Malcolm Ryan <malcolmr at cse.unsw.edu.au> wrote:
> I'm not sure I understand that code. Would you mind explaining in more
> detail?

First of all, the loops in the code looping through layers can be
ignored for exposition, since they are there to handle the cases when
cards are in the bottom, middle, or top of a pile of three cards.
Assume that we have two piles of card (X1, X2, X3) and (Y1, Y2, Y3)
where Xv and Xv are integer variables, and where X2 and Y2 have the
same function for purposes of the game. The values of the cards
represent when they are played (note that I mistranslated the
condition in my earlier post, X1 and Y1 should be exchanged, as should
X3 and Y3). Now the code can be simplified to
  // cond is the condition for the symmetry
   BoolVarArgs ba(4);
   // Both cards played after the ones on top of them
   ba[0] = post(this, ~(X2 < Y3));
   ba[1] = post(this, ~(Y2 < X3));
   // Both cards played before the ones under them
   ba[2] = post(this, ~(Y1 < X2));
   ba[3] = post(this, ~(X1 < Y2));
   // Cond holds when all the above holds
   BoolVar cond(this, 0, 1);
   rel(this, BOT_AND, ba, cond);

   // If cond is fulfilled, then we can order the cards
   // cond -> (X2 < Y2)
   post(this, tt(!cond || ~(X2 < Y2)));

The ba-array holds a set Boolean variables for reified relations, and
the rel-function takes the conjunction of these. The final post just
uses the standard unfolding of an implication since there is no
implication-operator. You can also use the implication-function
together with post to get it:
   post(this, tt(imp(cond, ~(X2 < Y2))));


> How do you do reified constraints in Gecode?

By using the reified post-functions, such as
   rel(this, x, IRT_LE, y, b);
with x and y integer variables and b a Boolean control variable. In
MiniModel expressions, you can use the unary tilde-operator to reify
an expression:
   BoolVar b = post(this, ~(x < y));

Cheers,
Mikael

-- 
Mikael Zayenz Lagerkvist, http://www.ict.kth.se/~zayenz/