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:

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$ \in$ 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 $ \in$ 1# 5 for i$ \in$ 1 # 10 such that
Qi = 1 $ \leftrightarrow$ Ai = 1
Qi = 2 $ \leftrightarrow$ Bi = 1
Qi = 3 $ \leftrightarrow$ Ci = 1
Qi = 4 $ \leftrightarrow$ Di = 1
Qi = 5 $ \leftrightarrow$ Ei = 1
The first question can now be expressed by means of five equivalences:
A1 = B2
B1 = (B3$ \land$(B2 = 0))
C1 = (B4$ \land$(B2 + B3 = 0))
D1 = (B5$ \land$(B2 + B3 + B4 = 0))
E1 = (B6$ \land$(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 $ \neq$ Q2,    Q7 $ \neq$ Q8,     Q8 $ \neq$ Q9,    Q9 $ \neq$ 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)) = $ \sum_{{i=1}}^{{10}}$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 = $ \sum_{{i=1}}^{{10}}$(Bi+Ci+Di)
A9 = (S $ \in$ {2, 3, 5, 7})
B9 = (S $ \in$ {1, 2, 6})
C9 = (S $ \in$ {0, 1, 4, 9})
D9 = (S $ \in$ {0, 1, 8})
E9 = (S $ \in$ {0, 5, 10})
where S is an existentially quantified auxiliary variable. This time we use reified membership constraints of the form x$ \in$ 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