Subsections

## Example: Self-referential Aptitude Test

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 FD.element.

### Problem Specification

The self-referential aptitude test (which is taken from [10]) 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:

• The first question whose answer is b is question (a) 2; (b) 3; (c) 4; (d) 5; (e) 6.
• 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.
• The answer to this question is the same as the answer to question (a) 1; (b) 2; (c) 4; (d) 7; (e) 6.
• The number of questions with the answer a is (a) 0; (b) 1; (c) 2; (d) 3; (e) 4.
• The answer to this question is the same as the answer to question (a) 10; (b) 9; (c) 8; (d) 7; (e) 6.
• 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.
• 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.
• The number of questions whose answers are vowels is (a) 2; (b) 3; (c) 4; (d) 5; (e) 6.
• 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.
• The answer to this question is (a) a; (b) b; (c) c; (d) d; (e) e.
To understand the test, verify that
1:c 2:d 3:e 4:b 5:e
6:e 7:d 8:c 9:b 10:a
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.

### Viewpoint and Constraints

Our model has 0/1 - variables Ai, Bi, Ci, andDi for i 1# 10 such that:
1. Ai + Bi + Ci + Di + Ei = 1
2. Ai = 1 iff the answer to Question i is a
3. Bi = 1 iff the answer to Question i is b
4. Ci = 1 iff the answer to Question i is c
5. Di = 1 iff the answer to Question i is d
6. Ei = 1 iff the answer to Question i is e
To obtain a compact representation of the questions, we also have variables Qi 1# 5 for i 1 # 10 such that
Qi = 1 Ai = 1
Qi = 2 Bi = 1
Qi = 3 Ci = 1
Qi = 4 Di = 1
Qi = 5 Ei = 1
The first question can now be expressed by means of five equivalences:
A1 = B2
B1 = (B3(B2 = 0))
C1 = (B4(B2 + B3 = 0))
D1 = (B5(B2 + B3 + B4 = 0))
E1 = (B6(B2 + B3 + B4 + B5 = 0))
These equivalences can be expressed by reifying the nested equality constraints.

The second question can be expressed with the following constraints:

Q1 Q2,    Q7 Q8,     Q8 Q9,    Q9 Q10
A2 = (Q2 = Q3),    B2 = (Q3 = Q4),    C2 = (Q4 = Q5)
D2 = (Q5 = Q6),    E2 = (Q6 = Q7)

The third question can be expressed as follows:

A3 = (Q1 = Q3),    B3 = (Q2 = Q3),    C3 = (Q4 = Q3)
D3 = (Q7 = Q3),    E3 = (Q6 = Q3)

The fourth question can be elegantly expressed with the constraint

element(Q4,(0,1,2,3,4)) = Ai
where the function element(k,x) yields the k-th component of the tuple x.

We choose this formulation since Alice provides a propagator FD.element for the constraint element(k,x)= y.

### Reified Membership Constraints

The nineth question can be expressed with the following equations
S = (Bi+Ci+Di)
A9 = (S {2, 3, 5, 7})
B9 = (S {1, 2, 6})
C9 = (S {0, 1, 4, 9})
D9 = (S {0, 1, 8})
E9 = (S {0, 5, 10})
where S is an existentially quantified auxiliary variable. This time we use reified membership constraints of the form x D.

### Branching Strategy

We branch on the variables Q1, Q2,... using the standard first-fail strategy.

### Script

(* bsum ensures that the sum of the boolean vector
boolvec is equal s(:intvar) *)
fun bsum(space,boolvec,s)=
let
val tmp = Vector.map(fn x =>
(FD.boolvar2intvar x))boolvec
in
post(space,SUMV(tmp) = FD(s),FD.DOM)
end

(* bsumI ensures that the sum of the boolean vector
boolvec is equal s(:int) *)
fun bsumI(space,boolvec,s)=
let
val tmp = Vector.map(fn x =>
(FD.boolvar2intvar x))boolvec
in
post(space,SUMV(tmp) = s,FD.DOM)
end

fun srat space =
let
val a as #[a0,a1,a2,a3,a4,a5,a6,a7,a8,a9] =
FD.boolvarVec(space,10)
val b as #[b0,b1,b2,b3,b4,b5,b6,b7,b8,b9]=
FD.boolvarVec(space,10)
val c as #[c0,c1,c2,c3,c4,c5,c6,c7,c8,c9]=
FD.boolvarVec(space,10)
val d as #[d0,d1,d2,d3,d4,d5,d6,d7,d8,d9]=
FD.boolvarVec(space,10)
val e as #[e0,e1,e2,e3,e4,e5,e6,e7,e8,e9]=
FD.boolvarVec(space,10)
val questions as #[q0,q1,q2,q3,q4,q5,q6,q7,q8,q9] =
FD.rangeVec(space,10,(1,5))
val suma = FD.range(space,(0,10))
val sumb = FD.range(space,(0,10))
val sumc = FD.range(space,(0,10))
val sumd = FD.range(space,(0,10))
val sume = FD.range(space,(0,10))
val sumae =FD.range(space,(0,20))
val sumbcd = FD.range(space,(0,30))
(* assert ensures that q_i = nb <-> boolvec[i]= 1  *)
fun asrt(boolvec,nb)= Vector.appi(fn(i,x)=>
FD.Reified.relI(space,Vector.sub(questions,i),
FD.EQ,nb,x))(boolvec)
in
Vector.app(fn(x,y)=> bsum(space,x,y))
(#[(a,suma),(b,sumb),(c,sumc),(d,sumd),(e,sume)]);
post(space,FD(suma) + FD(sume) = FD(sumae),FD.DOM);
post(space,FD(sumb) + FD(sumc) + FD(sumd)
= FD(sumbcd),FD.DOM);

(* ensures that a_i + b_i + .. + e_i = 1 *)
Vector.app(fn(i) =>
let
val tmp = Vector.map(fn y =>Vector.sub(y,i))
(#[a,b,c,d,e])
in
bsumI(space,tmp,1)
end)
(Vector.tabulate(10,fn x => x));

(*  to obtain a compact representation of the questions
(see Model) *)
Vector.appi(fn(i,x)=> asrt(x,i+1))(#[a,b,c,d,e]);

(* first question *)
Vector.appi(fn(i,(x,y))=>
let
val tmp1 = Vector.sub(x,0)
val tmp2 = Vector.sub(b,i+1)
val tmp3 = FD.boolvar(space)
val tmp4 = FD.boolvar(space)
val tmp5 = FD.boolvar(space)
in
if(Vector.length(y)>0)
then
(FD.Reified.linear(space,Vector.map(fn x=>
(1,FD.boolvar2intvar x))y,FD.EQ,0,tmp3,FD.DOM);
FD.conj(space,tmp4,tmp3,tmp2);
FD.conj(space,tmp5,tmp4,tmp1);
FD.Reified.relI(space,Vector.sub(questions,0),
FD.EQ,i+1,tmp5))
else
(FD.conj(space,tmp3,tmp1,tmp2);
FD.Reified.relI(space,Vector.sub(questions,0),
FD.EQ,1,tmp3))
end)
(#[(a,#[]),(b,#[b1]),(c,#[b1,b2]),(d,#[b1,b2,b3]),
(e,#[b1,b2,b3,b4])]);

(* second and third question*)
Vector.app(fn(x,y)=>FD.rel(space,x,FD.NQ,y))
(#[(q0,q1),(q6,q7),(q7,q8),(q8,q9)]);
Vector.app(fn(x,y,z) => FD.Reified.rel(space,y,FD.EQ,z,x))
(#[(a1,q1,q2),(b1,q2,q3),(c1,q3,q4),(d1,q4,q5),
(e1,q5,q6),(a2,q0,q2),(b2,q1,q2),(c2,q3,q2),
(d2,q6,q2),(e2,q5,q2)]);

(* fourth question *)
let
val tmp = FD.range(space,(1,5))
in
post(space,FD(tmp) = FD(q3) - 1,FD.DOM);
FD.elementI(space,#[0,1,2,3,4],tmp,suma)
end;

(* fifth question *)
Vector.app(fn(x,y) => FD.Reified.rel(space,y,FD.EQ,q4,x))
(#[(a4,q9),(b4,q8),(c4,q7),(d4,q6),(e4,q5)]);

(* sixth question *)
Vector.app(fn(x,y)=>FD.Reified.rel(space,suma,FD.EQ,x,y))
(#[(sumb,a5),(sumc,b5),(sumd,c5),(sume,d5)]);
FD.Reified.linear(space,Vector.map(fn x =>
(1,FD.boolvar2intvar x))(#[a5,b5,c5,d5]),
FD.EQ,0,e5,FD.DOM);

(* seventh question *)
FD.Reified.relI(space,q7,FD.EQ,1,c6);
FD.Reified.relI(space,q7,FD.EQ,3,d6);

(* eighth question *)
let
val tmp = FD.range(space,(1,5))
in
post(space,FD(tmp) = FD(q7) - 1,FD.DOM);
FD.elementI(space,#[2,3,4,5,6],tmp,sumae)
end;

(* nineth question *)
Vector.app(fn(x,y)=>FD.Reified.dom(space,sumbcd,y,x))
(#[(a8,#[(2,3),(5,5),(7,7)]),(b8,#[(1,2),(6,6)]),
(c8,#[(0,1),(4,4),(9,9)]),(d8,#[(0,1),(8,8)]),
(e8,#[(0,0),(5,5),(10,10)]) ]);

(* last question is entailed in the compact representation
constraint above*)

FD.branch(space,questions,FD.B_SIZE_MIN,FD.B_MIN);
{q1 = q0, q2 = q1, q3 = q2, q4 = q3, q5 = q4, q6 = q5,
q7 = q6, q8 = q7, q9 = q8, q10 = q9}
end


Andreas Rossberg 2006-08-28