Example: Aligning for a Photo, Revisited

In Section 9.2 we have searched for a solution of the alignment problem which satisfies the maximal number of preferences. To this aim we have introduced a variable which counts the number of satisfied preferences. By branching this variable with its maximal value first, we have guaranteed that the first solution found is indeed the optimal one.

In this section we replace this ad-hoc approach by branch and bound. We first restate the script for the problem by omitting the branching code for the variable summing up the satisfied preferences. The resulting script is shown in Listing 20.

Script

fun revisedphoto space =
    let 
        val pers as #[b,c,d,f,g,m,p]= 
                      FD.rangeVec(space,7,(1,7))
       (* si as a vector of boolean variables where s_i is 1 
          if the i-th preference is satisfied *)
        val si as #[s1,s2,s3,s4,s5,s6,s7,s8] = 
                           FD.boolvarVec(space,8)
       (* constraints is a vector of pairs (x,y) such that x wants to
          stand next to y *)
        val constraints = #[(b,g),(b,m),(c,b),(c,g),
                            (f,m),(f,d),(p,f),(p,d)]
       (* satisfaction is the sum of all s_i *)
        val satisfaction = FD.range(space,(0,8))
       (* satisfy posts the reified constraints:|x-y| = 1 <-> z *)
        fun satisfy(sp,constr,bools)= 
            Vector.app(fn ((x,y),z) => 
              let
                 val tmp1 = FD.boolvar sp
                 val tmp2 = FD.boolvar sp
              in
                (FD.Reified.linear(sp,#[(1,x),(~1,y)],FD.EQ,1,
                                      tmp1,FD.DEF);
                 FD.Reified.linear(sp,#[(1,x),(~1,y)],FD.EQ,~1,
                                      tmp2,FD.DEF);
                 FD.disjV(sp,#[tmp2,tmp1],z))
              end)
                 (VectorPair.zip(constr,bools))
       (* photoorder ensures that the overall sum of satisfied
          preferences in an alternative solution must be strictly 
          greater than the corresponding sum in a previous solution *)
        fun photoorder(current,last)=
            post (current, FD(satisfaction) `> 
                  `(FD.Reflect.value(last,satisfaction)),FD.BND)                   
    in
        FD.distinct(space,pers,FD.DOM);
        satisfy(space,constraints,si);
        let 
           val si' = Vector.map(fn x => (FD.boolvar2intvar x))si
        in
           post(space,SUMV(si') `= FD(satisfaction),FD.DOM)
        end;
        FD.rel(space,f,FD.LE,b);
           
        FD.branch(space,pers,FD.B_SIZE_MIN,FD.B_SPLIT_MIN);
      ({Betty = b, Chris = c, Donald = d, Fred = f,
       Gary = g, Mary = m, Paul = p,satisfaction},photoorder)
   end

Next we define an ordering procedure which states that the overall sum of satisfied preferences in an alternative solution must be strictly greater than the corresponding sum in a previous solution:

fun photoorder(current,last)=
               post (current, FD(satisfaction)`> 
            `(FD.Reflect.value(last,satisfaction)),FD.BND)

Here the procedure FD.Reflect.value from the FD.Reflect library structure is used. It returns the value satisfaction takes in the space last and throws NotAssigned if satisfaction is not determined.

The optimal solution can be found with the statement

Explorer.exploreBest revisedphoto

Note that the type of the script has changed to:

FD.space ->
      {Betty : FD.intvar, Chris : FD.intvar, Donald : FD.intvar,
       Fred : FD.intvar, Gary : FD.intvar, Mary : FD.intvar, Paul : FD.intvar,
       satisfaction : FD.intvar} * (Modeling.space * FD.space -> unit)

We obtain the same solution as in 9.2. But now only 319 choice nodes are needed to find the optimal solution whereas 477 choice nodes were needed in Section 9.2. Furthermore, branch and bound allows us to prove in an efficient way that the last solution found is really the optimal one. The full search tree (including the proof of optimality) contains 639 choice nodes. If we inspect the solutions, we observe that the first solution satisfies only a single preference. By imposition of the ordering procedure by the search engine, the next found solution must satisfy more preferences. Indeed, the second solution satisfies two preferences. Following this approach we finally arrive at the optimal solution with six satisfied preferences.