<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
<HTML><HEAD><TITLE>8.1 Getting Started</TITLE><LINK href="ozdoc.css" rel="stylesheet" type="text/css"></HEAD><BODY><TABLE align="center" border="0" cellpadding="6" cellspacing="6" class="nav"><TR bgcolor="#DDDDDD"><TD><A href="node35.html">- Up -</A></TD><TD><A href="node37.html#section.reified.photo">Next >></A></TD></TR></TABLE><DIV id="section.reified.started"><H2><A name="section.reified.started">8.1 Getting Started</A></H2><P class="margin">reification of a constraint</P><P> The <EM>reification of a constraint</EM> <IMG alt="C" src="latex31.png"> with respect to a variable <IMG alt="x" src="latex42.png"> is the constraint </P><BLOCKQUOTE><P><IMG alt="(C \leftrightarrow x=1)
\;\land\;x\in0\#1" src="latex166.png"></P></BLOCKQUOTE><P> where it is assumed that <IMG alt="x" src="latex42.png"> does not occur free in <IMG alt="C" src="latex31.png">. </P><P>The operational semantics of a propagator for the reification of a constraint <IMG alt="C" src="latex31.png"> with respect to <IMG alt="x" src="latex42.png"> is given by the following rules: </P><OL type="1"><LI><P>If the constraint store entails <IMG alt="x=1" src="latex167.png">, the propagator for the reification reduces to a propagator for <IMG alt="C" src="latex31.png">.</P></LI><LI><P>If the constraint store entails <IMG alt="x=0" src="latex168.png">, the propagator for the reification reduces to a propagator for <IMG alt="\neg C" src="latex63.png">}.</P></LI><LI><P>If a propagator for <IMG alt="C" src="latex31.png"> would realize that the constraint store entails <IMG alt="C" src="latex31.png">, the propagator for the reification tells <IMG alt="x=1" src="latex167.png"> and ceases to exist.</P></LI><LI><P>If a propagator for <IMG alt="C" src="latex31.png"> would realize that the constraint store is inconsistent with <IMG alt="C" src="latex31.png">, the propagator for the reification tells <IMG alt="x=0" src="latex168.png"> and ceases to exist.</P></LI></OL><P> </P><P>To understand these rules, you need to be familiar with the definitions in <A href="node4.html#section.constraints.propagation">Section 2.2</A>. </P><P class="margin">0/1-variables</P><P> A <EM>0/1-variable</EM> is a variable that is constrained to the finite domain <IMG alt="0\#1" src="latex169.png">. The control variables of reified constraints are 0/1-variables. </P><P class="margin">posting refied constraints</P><P> Here are examples for statements creating propagators for reified constraints: </P><UL><LI><P><CODE>(X<SPAN class="keyword"><:</SPAN>Y)=B</CODE> creates a propagator for the reification of <IMG alt="X<Y" src="latex29.png"> with respect to <IMG alt="B" src="latex39.png">.</P></LI><LI><P><CODE>(X<SPAN class="keyword">+</SPAN>Y<SPAN class="keyword">+</SPAN>Z<SPAN class="keyword">=:</SPAN>0)=B</CODE> creates a propagator for the reification of <IMG alt="X+Y+Z=0" src="latex170.png"> with respect to <IMG alt="B" src="latex39.png">.</P></LI><LI><P><CODE>(X<SPAN class="keyword">\=:</SPAN>Y)=B</CODE> creates a propagator for the reification of <IMG alt="X\neq Y" src="latex171.png"> with respect to <IMG alt="B" src="latex39.png">.</P></LI><LI><P><CODE>(X<SPAN class="keyword">::</SPAN>0<SPAN class="keyword">#</SPAN>10)=B</CODE> creates a propagator for the reification of <IMG alt="X\in0\#10" src="latex172.png"> with respect to <IMG alt="B" src="latex39.png">.</P></LI><LI><P><CODE>{FD<SPAN class="keyword">.</SPAN>reified<SPAN class="keyword">.</SPAN>distance X Y <SPAN class="string">'=:'</SPAN> Z B}</CODE> creates a propagator for the reification of <IMG alt="|X-Y|=Z" src="latex173.png"> with respect to <IMG alt="B" src="latex39.png">.</P></LI></UL><P> </P><P class="margin">expressing equivalences</P><P> With reified constraints it is straightforward to express equivalences of constraints. For instance, the equivalence </P><BLOCKQUOTE><P><IMG alt="X<Y\;\leftrightarrow\; X<Z" src="latex174.png"></P></BLOCKQUOTE><P> can be posted with the statement </P><BLOCKQUOTE class="code"><CODE>X<SPAN class="keyword"><:</SPAN>Y = X<SPAN class="keyword"><:</SPAN>Z</CODE></BLOCKQUOTE><P> This statement is a notational convenience for </P><BLOCKQUOTE class="code"><CODE><SPAN class="keyword">local</SPAN> B <SPAN class="keyword">in</SPAN> <BR> X<SPAN class="keyword"><:</SPAN>Y=B X<SPAN class="keyword"><:</SPAN>Z=B <BR><SPAN class="keyword">end</SPAN></CODE></BLOCKQUOTE><P> and creates 2 propagators for reified constraints. </P><P class="margin">Boolean connectives</P><P> We can define the Boolean connectives (e.g., conjunction or negation) by associating 0 with false and 1 with true. The respective Boolean constraints can be posted by means of the following procedures: </P><UL><LI><P><CODE>{FD<SPAN class="keyword">.</SPAN>conj X Y Z}</CODE> posts the constraint <IMG alt="(X\land Y)=Z" src="latex175.png">.</P></LI><LI><P><CODE>{FD<SPAN class="keyword">.</SPAN>disj X Y Z}</CODE> posts the constraint <IMG alt="(X\lor Y)=Z" src="latex176.png">.</P></LI><LI><P><CODE>{FD<SPAN class="keyword">.</SPAN>impl X Y Z}</CODE> posts the constraint <IMG alt="(X\to Y)=Z" src="latex177.png">.</P></LI><LI><P><CODE>{FD<SPAN class="keyword">.</SPAN>equi X Y Z}</CODE> posts the constraint <IMG alt="(X\leftrightarrow Y)=Z" src="latex178.png">.</P></LI><LI><P><CODE>{FD<SPAN class="keyword">.</SPAN>nega X Y}</CODE> posts the constraint <IMG alt="\neg X=Y" src="latex179.png">.</P></LI></UL><P> </P><DIV class="unnumbered"><H3><A name="label100">Exercises</A></H3><DIV class="exercise" id="reified.ex.a"><P><B>Exercise 8.1</B> (<A href="answers.html#label188">See solution</A>)</P><BLOCKQUOTE><P>Write a statement that posts the constraint </P><BLOCKQUOTE><P><IMG alt="(X<Y\;\to\; X+Y=Z)
\;\;\leftrightarrow\;\;
(X\cdot Y=Z\;\lor\;Z\neq 5)" src="latex180.png"></P></BLOCKQUOTE><P></P></BLOCKQUOTE></DIV><DIV class="exercise" id="reified.ex.b"><P><B>Exercise 8.2</B> (<A href="answers.html#label187">See solution</A>)</P><BLOCKQUOTE><P>Write a procedure <CODE>{Conj X Y Z}</CODE> that posts the constraints </P><BLOCKQUOTE><P><IMG alt="(X\land Y)=Z
,\quad
X\in0\#1
,\quad
Y\in0\#1" src="latex181.png"></P></BLOCKQUOTE><P></P><P>The procedure should post the conjunction <IMG alt="(X\land Y)=Z" src="latex175.png">. by means of the reified form of the infix operator <CODE><SPAN class="keyword">=:</SPAN></CODE>.</P><P>Write analogous procedures <CODE>Equi</CODE> and <CODE>Nega</CODE> posting equivalences and negations.</P><P>Write an analogous procedure <CODE>Dis</CODE> posting a disjunction <IMG alt="(X\lor Y)=Z" src="latex176.png">. Use the reified form of <CODE><SPAN class="keyword"><:</SPAN></CODE> to post the disjunction.</P><P>How would you write a procedure posting an implication <IMG alt="(X\to Y)=Z" src="latex177.png">?</P></BLOCKQUOTE></DIV></DIV></DIV><TABLE align="center" border="0" cellpadding="6" cellspacing="6" class="nav"><TR bgcolor="#DDDDDD"><TD><A href="node35.html">- Up -</A></TD><TD><A href="node37.html#section.reified.photo">Next >></A></TD></TR></TABLE><HR><ADDRESS><A href="http://www.ps.uni-sb.de/~schulte/">Christian Schulte</A> and <A href="http://www.ps.uni-sb.de/~smolka/">Gert Smolka</A><BR><SPAN class="version">Version 1.4.0 (20090610)</SPAN></ADDRESS></BODY></HTML>
distrib
>
Mandriva
>
2010.0
>
i586
>
media
>
contrib-release
>
by-pkgid
>
bd5c3d824c3db63ffd9226c15941e6ad
>
files
>
1210
