/usr/share/mozart/doc/fdt/node38.html is in mozart-doc 1.4.0-8ubuntu1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 | <!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
<HTML><HEAD><TITLE>8.3 Example: Self-referential Aptitude Test</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="node37.html#section.reified.photo"><< Prev</A></TD><TD><A href="node35.html">- Up -</A></TD><TD><A href="node39.html#section.reified.bin">Next >></A></TD></TR></TABLE><DIV id="section.reified.srat"><H2><A name="section.reified.srat">8.3 Example: Self-referential Aptitude Test</A></H2><P>This example illustrates three issues: expressing complex propositional formulas as reified constraints, improving performance and presentation by elimination of common subconstraints, and using the symbolic constraint posted by <CODE>FD<SPAN class="keyword">.</SPAN>element</CODE>. </P><DIV class="unnumbered"><H3><A name="label106">Problem Specification</A></H3><P>The self-referential aptitude test (which is taken from <A href="bib.html#henz.96">[Hen96]</A>) consists of 10 multiple choice questions, referred to as 1 to 10. Each question allows for 5 possible answers, referred to as a to e. For each of the 50 possible answers, a condition is specified. For each question, exactly one of the conditions associated with its possible answers must hold. A solution of the test is a function assigning to every question a letter such that the condition selected by the assigned letter holds. Here are the questions and their possible answers: </P><OL type="1"><LI><P>The first question whose answer is b is question (a) 2; (b) 3; (c) 4; (d) 5; (e) 6.</P></LI><LI><P>The only two consecutive questions with identical answers are questions (a) 2 and 3; (b) 3 and 4; (c) 4 and 5; (d) 5 and 6; (e) 6 and 7.</P></LI><LI><P>The answer to this question is the same as the answer to question (a) 1; (b) 2; (c) 4; (d) 7; (e) 6.</P></LI><LI><P>The number of questions with the answer a is (a) 0; (b) 1; (c) 2; (d) 3; (e) 4.</P></LI><LI><P>The answer to this question is the same as the answer to question (a) 10; (b) 9; (c) 8; (d) 7; (e) 6.</P></LI><LI><P>The number of questions with answer a equals the number of questions with answer (a) b; (b) c; (c) d; (d) e; (e) none of the above.</P></LI><LI><P>Alphabetically, the answer to this question and the answer to the following question are (a) 4 apart; (b) 3 apart; (c) 2 apart; (d) 1 apart; (e) the same.</P></LI><LI><P>The number of questions whose answers are vowels is (a) 2; (b) 3; (c) 4; (d) 5; (e) 6.</P></LI><LI><P>The number of questions whose answer is a consonant is (a) a prime; (b) a factorial; (c) a square; (d) a cube; (e) divisible by 5.</P></LI><LI><P>The answer to this question is (a) a; (b) b; (c) c; (d) d; (e) e.</P></LI></OL><P> </P><P>To understand the test, verify that </P><TABLE align="center" bgcolor="#f0f0e0"><TR valign="top"><TD><P>1:c</P></TD><TD><P>2:d</P></TD><TD><P>3:e</P></TD><TD><P>4:b</P></TD><TD><P>5:e</P></TD></TR><TR valign="top"><TD><P>6:e</P></TD><TD><P>7:d</P></TD><TD><P>8:c</P></TD><TD><P>9:b</P></TD><TD><P>10:a</P></TD></TR></TABLE><P> is a correct set of answers for the test. In particular, convince yourself that for every question the remaining 4 possibilities to answer it are falsified. The script we are going to write will prove that there is no other set of correct answers. </P></DIV><DIV class="unnumbered"><H3><A name="label107">Model</A></H3><P>Our model has 0/1-variables <IMG alt="A_i" src="latex194.png">, <IMG alt="B_i" src="latex195.png">, <IMG alt="C_i" src="latex126.png">, and <IMG alt="D_i" src="latex196.png"> for <IMG alt="i\in1\#10" src="latex197.png"> such that: </P><OL type="1"><LI><P><IMG alt="A_i+B_i+C_i+D_i+E_i=1" src="latex198.png">.</P></LI><LI><P><IMG alt="A_i=1" src="latex199.png"> iff the answer to Question <IMG alt="i" src="latex115.png"> is a.</P></LI><LI><P><IMG alt="B_i=1" src="latex200.png"> iff the answer to Question <IMG alt="i" src="latex115.png"> is b.</P></LI><LI><P><IMG alt="C_i=1" src="latex201.png"> iff the answer to Question <IMG alt="i" src="latex115.png"> is c.</P></LI><LI><P><IMG alt="D_i=1" src="latex202.png"> iff the answer to Question <IMG alt="i" src="latex115.png"> is d.</P></LI><LI><P><IMG alt="E_i=1" src="latex203.png"> iff the answer to Question <IMG alt="i" src="latex115.png"> is e.</P></LI></OL><P> To obtain a compact representation of the questions, we also have variables <IMG alt="Q_i\in1\#5" src="latex204.png"> for <IMG alt="i\in1\#10" src="latex197.png"> such that </P><TABLE align="center" bgcolor="#f0f0e0"><TR valign="top"><TD><P><IMG alt="Q_i=1\leftrightarrow A_i=1" src="latex205.png"></P></TD><TD><P><IMG alt="Q_i=2\leftrightarrow B_i=1" src="latex206.png"></P></TD></TR><TR valign="top"><TD><P><IMG alt="Q_i=3\leftrightarrow C_i=1" src="latex207.png"></P></TD><TD><P><IMG alt="Q_i=4\leftrightarrow D_i=1" src="latex208.png"></P></TD></TR><TR valign="top"><TD><P><IMG alt="Q_i=5\leftrightarrow E_i=1" src="latex209.png"></P></TD></TR></TABLE><P> </P><P>The first question can now be expressed by means of five equivalences: </P><BLOCKQUOTE><P><IMG alt="\begin{array}{rcl}
A_1
&=&
B_2
\\
B_1
&=&
(B_3\land (B_2=0))
\\
C_1
&=&
(B_4\land (B_2+B_3=0))
\\
D_1
&=&
(B_5\land (B_2+B_3+B_4=0))
\\
E_1
&=&
(B_6\land (B_2+B_3+B_4+B_5=0))
\end{array}" src="latex210.png"></P></BLOCKQUOTE><P> These equivalences can be expressed by reifying the nested equality constraints. </P><P>The second question can be expressed with the following constraints: </P><BLOCKQUOTE><P><IMG alt="\begin{array}{rcl}
&
Q_1\neq Q_2,\quad
Q_7\neq Q_8,\quad
Q_8\neq Q_9,\quad
Q_9\neq Q_10
\\
&
A_2=(Q_2=Q_3),\quad
B_2=(Q_3=Q_4),\quad
C_2=(Q_4=Q_5)
\\
&
D_2=(Q_5=Q_6),\quad
E_2=(Q_6=Q_7)
\end{array}" src="latex211.png"></P></BLOCKQUOTE><P> </P><P>The third question can be expressed as follows: </P><BLOCKQUOTE><P><IMG alt="\begin{array}{rcl}
&
A_3=(Q_1=Q_3),\quad
B_3=(Q_2=Q_3),\quad
C_3=(Q_4=Q_3)
\\
&
D_3=(Q_7=Q_3),\quad
E_3=(Q_6=Q_3)
\end{array}" src="latex212.png"></P></BLOCKQUOTE><P> </P><P>The fourth question can be elegantly expressed with the constraint </P><BLOCKQUOTE><P><IMG alt="{\it element}(Q_4,\;(0,1,2,3,4)) =
\sum_{i=1}^{10}{A_i}" src="latex213.png"></P></BLOCKQUOTE><P> where the function <IMG alt="{\it element}(k,x)" src="latex214.png"> yields the <IMG alt="k" src="latex114.png">-th component of the tuple <IMG alt="x" src="latex42.png">. </P><P>We choose this formulation since Oz provides a propagator <CODE>FD<SPAN class="keyword">.</SPAN>element</CODE> for the constraint <IMG alt="{\it
element}(k,x)=y" src="latex215.png">. </P><P class="margin">reified membership constraints</P><P> The nineth question can be expressed with the following equations </P><BLOCKQUOTE><P><IMG alt="\begin{array}{rcl}
S
&=&
\sum_{i=1}^{10}{(B_i+C_i+D_i)}
\\
A_9
&=&
(S\in\{2,3,5,7\})
\\
B_9
&=&
(S\in\{1,2,6\})
\\
C_9
&=&
(S\in\{0,1,4,9\})
\\
D_9
&=&
(S\in\{0,1,8\})
\\
E_9
&=&
(S\in\{0,5,10\})
\end{array}" src="latex216.png"></P></BLOCKQUOTE><P> where <IMG alt="S" src="latex7.png"> is an existentially quantified auxiliary variable. This time we use reified membership constraints of the form <IMG alt="x\in D" src="latex16.png">.</P></DIV><DIV class="unnumbered"><H3><A name="label108">Distribution Strategy</A></H3><P>We distribute on the variables <IMG alt="Q_1,\,Q_2\,\ldots" src="latex217.png"> using the standard first-fail strategy. </P></DIV><DIV class="unnumbered"><H3><A name="label109">Script</A></H3><P></P><DIV id="progsrat"><HR><P><A name="progsrat"></A></P><DL class="anonymous"><DD class="code"><CODE><SPAN class="keyword">proc</SPAN><SPAN class="variablename"> </SPAN>{<SPAN class="functionname">SRAT</SPAN> Q}<BR> <SPAN class="keyword">proc</SPAN><SPAN class="variablename"> </SPAN>{<SPAN class="functionname">Vector</SPAN> V} % <SPAN class="comment">V is a 0/1-vector of length 10<BR></SPAN> {FD<SPAN class="keyword">.</SPAN>tuple v 10 0<SPAN class="keyword">#</SPAN>1 V} <BR> <SPAN class="keyword">end</SPAN> <BR> <SPAN class="keyword">proc</SPAN><SPAN class="variablename"> </SPAN>{<SPAN class="functionname">Sum</SPAN> V S} % <SPAN class="comment">S is the sum of the components of vector V<BR></SPAN> {FD<SPAN class="keyword">.</SPAN>decl S} {FD<SPAN class="keyword">.</SPAN>sum V <SPAN class="string">'=:'</SPAN> S} <BR> <SPAN class="keyword">end</SPAN> <BR> <SPAN class="keyword">proc</SPAN><SPAN class="variablename"> </SPAN>{<SPAN class="functionname">Assert</SPAN> I U V W X Y} <BR> A<SPAN class="keyword">.</SPAN>I=U B<SPAN class="keyword">.</SPAN>I=V C<SPAN class="keyword">.</SPAN>I=W D<SPAN class="keyword">.</SPAN>I=X E<SPAN class="keyword">.</SPAN>I=Y <BR> <SPAN class="keyword">end</SPAN> <BR> A = {Vector} B = {Vector}<BR> C = {Vector} D = {Vector} E = {Vector}<BR> SumA = {Sum A} SumB = {Sum B} SumC = {Sum C} <BR> SumD = {Sum D} SumE = {Sum E}<BR> SumAE = {Sum [SumA SumE]} SumBCD = {Sum [SumB SumC SumD]}<BR><SPAN class="keyword">in</SPAN> <BR> {FD<SPAN class="keyword">.</SPAN>tuple q 10 1<SPAN class="keyword">#</SPAN>5 Q}<BR> {For 1 10 1<BR> <SPAN class="keyword">proc</SPAN><SPAN class="variablename"> </SPAN>{<SPAN class="functionname">$</SPAN> I} {Assert I Q<SPAN class="keyword">.</SPAN>I<SPAN class="keyword">=:</SPAN>1 Q<SPAN class="keyword">.</SPAN>I<SPAN class="keyword">=:</SPAN>2 Q<SPAN class="keyword">.</SPAN>I<SPAN class="keyword">=:</SPAN>3 Q<SPAN class="keyword">.</SPAN>I<SPAN class="keyword">=:</SPAN>4 Q<SPAN class="keyword">.</SPAN>I<SPAN class="keyword">=:</SPAN>5} <SPAN class="keyword">end</SPAN>}<BR> %% <SPAN class="comment">1<BR></SPAN> {Assert 1 B<SPAN class="keyword">.</SPAN>2<BR> {FD<SPAN class="keyword">.</SPAN>conj B<SPAN class="keyword">.</SPAN>3 (B<SPAN class="keyword">.</SPAN>2<SPAN class="keyword">=:</SPAN>0)}<BR> {FD<SPAN class="keyword">.</SPAN>conj B<SPAN class="keyword">.</SPAN>4 (B<SPAN class="keyword">.</SPAN>2<SPAN class="keyword">+</SPAN>B<SPAN class="keyword">.</SPAN>3<SPAN class="keyword">=:</SPAN>0)}<BR> {FD<SPAN class="keyword">.</SPAN>conj B<SPAN class="keyword">.</SPAN>5 (B<SPAN class="keyword">.</SPAN>2<SPAN class="keyword">+</SPAN>B<SPAN class="keyword">.</SPAN>3<SPAN class="keyword">+</SPAN>B<SPAN class="keyword">.</SPAN>4<SPAN class="keyword">=:</SPAN>0)}<BR> {FD<SPAN class="keyword">.</SPAN>conj B<SPAN class="keyword">.</SPAN>6 (B<SPAN class="keyword">.</SPAN>2<SPAN class="keyword">+</SPAN>B<SPAN class="keyword">.</SPAN>3<SPAN class="keyword">+</SPAN>B<SPAN class="keyword">.</SPAN>4<SPAN class="keyword">+</SPAN>B<SPAN class="keyword">.</SPAN>5<SPAN class="keyword">=:</SPAN>0)}}<BR> %% <SPAN class="comment">2<BR></SPAN> {Assert 2 Q<SPAN class="keyword">.</SPAN>2<SPAN class="keyword">=:</SPAN>Q<SPAN class="keyword">.</SPAN>3 Q<SPAN class="keyword">.</SPAN>3<SPAN class="keyword">=:</SPAN>Q<SPAN class="keyword">.</SPAN>4 Q<SPAN class="keyword">.</SPAN>4<SPAN class="keyword">=:</SPAN>Q<SPAN class="keyword">.</SPAN>5 Q<SPAN class="keyword">.</SPAN>5<SPAN class="keyword">=:</SPAN>Q<SPAN class="keyword">.</SPAN>6 Q<SPAN class="keyword">.</SPAN>6<SPAN class="keyword">=:</SPAN>Q<SPAN class="keyword">.</SPAN>7}<BR> Q<SPAN class="keyword">.</SPAN>1<SPAN class="keyword">\=:</SPAN>Q<SPAN class="keyword">.</SPAN>2 Q<SPAN class="keyword">.</SPAN>7<SPAN class="keyword">\=:</SPAN>Q<SPAN class="keyword">.</SPAN>8 Q<SPAN class="keyword">.</SPAN>8<SPAN class="keyword">\=:</SPAN>Q<SPAN class="keyword">.</SPAN>9 Q<SPAN class="keyword">.</SPAN>9<SPAN class="keyword">\=:</SPAN>Q<SPAN class="keyword">.</SPAN>10<BR> %% <SPAN class="comment">3<BR></SPAN> {Assert 3 Q<SPAN class="keyword">.</SPAN>1<SPAN class="keyword">=:</SPAN>Q<SPAN class="keyword">.</SPAN>3 Q<SPAN class="keyword">.</SPAN>2<SPAN class="keyword">=:</SPAN>Q<SPAN class="keyword">.</SPAN>3 Q<SPAN class="keyword">.</SPAN>4<SPAN class="keyword">=:</SPAN>Q<SPAN class="keyword">.</SPAN>3 Q<SPAN class="keyword">.</SPAN>7<SPAN class="keyword">=:</SPAN>Q<SPAN class="keyword">.</SPAN>3 Q<SPAN class="keyword">.</SPAN>6<SPAN class="keyword">=:</SPAN>Q<SPAN class="keyword">.</SPAN>3}<BR> %% <SPAN class="comment">4<BR></SPAN> {FD<SPAN class="keyword">.</SPAN>element Q<SPAN class="keyword">.</SPAN>4 [0 1 2 3 4] SumA}<BR> %% <SPAN class="comment">5<BR></SPAN> {Assert 5 Q<SPAN class="keyword">.</SPAN>10<SPAN class="keyword">=:</SPAN>Q<SPAN class="keyword">.</SPAN>5 Q<SPAN class="keyword">.</SPAN>9<SPAN class="keyword">=:</SPAN>Q<SPAN class="keyword">.</SPAN>5 Q<SPAN class="keyword">.</SPAN>8<SPAN class="keyword">=:</SPAN>Q<SPAN class="keyword">.</SPAN>5 Q<SPAN class="keyword">.</SPAN>7<SPAN class="keyword">=:</SPAN>Q<SPAN class="keyword">.</SPAN>5 Q<SPAN class="keyword">.</SPAN>6<SPAN class="keyword">=:</SPAN>Q<SPAN class="keyword">.</SPAN>5}<BR> %% <SPAN class="comment">6<BR></SPAN> {Assert 6 SumA<SPAN class="keyword">=:</SPAN>SumB SumA<SPAN class="keyword">=:</SPAN>SumC SumA<SPAN class="keyword">=:</SPAN>SumD SumA<SPAN class="keyword">=:</SPAN>SumE _}<BR> %% <SPAN class="comment">7<BR></SPAN> {FD<SPAN class="keyword">.</SPAN>element Q<SPAN class="keyword">.</SPAN>7 [4 3 2 1 0] {FD<SPAN class="keyword">.</SPAN>decl}={FD<SPAN class="keyword">.</SPAN>distance Q<SPAN class="keyword">.</SPAN>7 Q<SPAN class="keyword">.</SPAN>8 <SPAN class="string">'=:'</SPAN>}}<BR> %% <SPAN class="comment">8<BR></SPAN> {FD<SPAN class="keyword">.</SPAN>element Q<SPAN class="keyword">.</SPAN>8 [2 3 4 5 6] SumAE}<BR> %% <SPAN class="comment">9<BR></SPAN> {Assert 9 SumBCD<SPAN class="keyword">::</SPAN>[2 3 5 7] SumBCD<SPAN class="keyword">::</SPAN>[1 2 6] <BR> SumBCD<SPAN class="keyword">::</SPAN>[0 1 4 9] SumBCD<SPAN class="keyword">::</SPAN>[0 1 8]<BR> SumBCD<SPAN class="keyword">::</SPAN>[0 5 10]}<BR> %% <SPAN class="comment">10<BR></SPAN> {FD<SPAN class="keyword">.</SPAN>distribute ff Q}<BR><SPAN class="keyword">end</SPAN></CODE></DD></DL><P class="caption"><STRONG>Figure 8.2:</STRONG> A script for the self-referential aptitude test.</P><HR></DIV><P> </P><DIV class="apropos"><P class="margin">elimination of common subconstraints</P><P> The script in <A href="node38.html#progsrat">Figure 8.2</A> implements the indexed variables <IMG alt="A_i" src="latex194.png">, <IMG alt="B_i" src="latex195.png">, <IMG alt="C_i" src="latex126.png">, <IMG alt="D_i" src="latex196.png">, <IMG alt="E_i" src="latex218.png">, and <IMG alt="Q_i" src="latex219.png"> as tuples with 10 components each. The three procedures <CODE>Vector</CODE>, <CODE>Sum</CODE>, and <CODE>Assert</CODE> make it more convenient to state the constraints. For each sum occurring in the questions an auxiliary variable is introduced so that the corresponding summation constraint needs to be posted only once. This elimination of common subconstraints provides for a compact formulation of the script and also improves its performance. </P></DIV><P>The procedure <CODE>{FD<SPAN class="keyword">.</SPAN>element </CODE><I>K</I><CODE> </CODE><I>V</I><CODE> </CODE><I>X</I><CODE>}</CODE> posts a propagator for the constraint saying that <I>X</I> is the <I>K</I>-th component of the vector <I>V</I>. </P><P>Note the use of <CODE>FD<SPAN class="keyword">.</SPAN>decl</CODE> in the definition of the procedure <CODE>Sum</CODE> and in the representation of the seventh question. Telling an initial domain constraint for the respective variables is necessary so that the propagators depending on these variables can start their work. </P></DIV><DIV class="unnumbered"><H3><A name="label110">Exercises</A></H3><DIV class="exercise" id="reified.ex.d"><P><B>Exercise 8.4</B> (<A href="answers.html#label185">See solution</A>)</P><BLOCKQUOTE><P>The script in <A href="node38.html#progsrat">Figure 8.2</A> uses the statement </P><BLOCKQUOTE class="code"><CODE>{FD<SPAN class="keyword">.</SPAN>element Q<SPAN class="keyword">.</SPAN>7 [4 3 2 1 0] <BR> {FD<SPAN class="keyword">.</SPAN>decl}={FD<SPAN class="keyword">.</SPAN>distance Q<SPAN class="keyword">.</SPAN>7 Q<SPAN class="keyword">.</SPAN>8 <SPAN class="string">'=:'</SPAN>}}</CODE></BLOCKQUOTE><P> to post the constraints for the seventh question. It avoids one auxiliary variable by nesting two equated procedure applications. Give an equivalent statement in which the auxiliary variable is introduced and the nested procedure applications are unfolded.</P></BLOCKQUOTE></DIV></DIV></DIV><TABLE align="center" border="0" cellpadding="6" cellspacing="6" class="nav"><TR bgcolor="#DDDDDD"><TD><A href="node37.html#section.reified.photo"><< Prev</A></TD><TD><A href="node35.html">- Up -</A></TD><TD><A href="node39.html#section.reified.bin">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 (20110908185330)</SPAN></ADDRESS></BODY></HTML>
|