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 A_i, B_i, C_i, andD_i for i$\in$ 1# 10 such that:

1. A_i + B_i + C_i + D_i + E_i = 1
2. A_i = 1 iff the answer to Question i is a
3. B_i = 1 iff the answer to Question i is b
4. C_i = 1 iff the answer to Question i is c
5. D_i = 1 iff the answer to Question i is d
6. E_i = 1 iff the answer to Question i is e

To obtain a compact representation of the questions, we also have variables Q_i $\in$ 1# 5 for i$\in$ 1 # 10 such that

Q_i = 1 $\leftrightarrow$ A_i = 1
Q_i = 2 $\leftrightarrow$ B_i = 1
Q_i = 3 $\leftrightarrow$ C_i = 1
Q_i = 4 $\leftrightarrow$ D_i = 1
Q_i = 5 $\leftrightarrow$ E_i = 1

The first question can now be expressed by means of five equivalences:

A₁ = B₂
B₁ = (B₃$\land$(B₂ = 0))
C₁ = (B₄$\land$(B₂ + B₃ = 0))
D₁ = (B₅$\land$(B₂ + B₃ + B₄ = 0))
E₁ = (B₆$\land$(B₂ + B₃ + B₄ + B₅ = 0))

These equivalences can be expressed by reifying the nested equality constraints.

The second question can be expressed with the following constraints:

Q₁ $\neq$ Q₂,    Q₇ $\neq$ Q₈,     Q₈ $\neq$ Q₉,    Q₉ $\neq$ Q₁0
A₂ = (Q₂ = Q₃),    B₂ = (Q₃ = Q₄),    C₂ = (Q₄ = Q₅)
D₂ = (Q₅ = Q₆),    E₂ = (Q₆ = Q₇)

The third question can be expressed as follows:

A₃ = (Q₁ = Q₃),    B₃ = (Q₂ = Q₃),    C₃ = (Q₄ = Q₃)
D₃ = (Q₇ = Q₃),    E₃ = (Q₆ = Q₃)

The fourth question can be elegantly expressed with the constraint

element(Q₄,(0,1,2,3,4)) = $\sum_{{i=1}}^{{10}}$A_i

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}}$(B_i+C_i+D_i)
A₉ = (S $\in$ {2, 3, 5, 7})
B₉ = (S $\in$ {1, 2, 6})
C₉ = (S $\in$ {0, 1, 4, 9})
D₉ = (S $\in$ {0, 1, 8})
E₉ = (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 Q₁, Q₂,... 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