Example: Aligning for a Photo

We will now see an overconstrained problem for which it is impossible to satisfy all constraints. The problem specification will distinguish between primary and secondary constraints, and the goal is to find a solution that satisfies all primary constraints and as many of the secondary constraints as possible.

Problem Specification

Betty, Chris, Donald, Fred, Gary, Mary, and Paul want to align in one row for taking a photo. Some of them have preferences next to whom they want to stand:

1. Betty wants to stand next to Gary and Mary.
2. Chris wants to stand next to Betty and Gary.
3. Fred wants to stand next to Mary and Donald.
4. Paul wants to stand next to Fred and Donald.

Obviously, it is impossible to satisfy all preferences. Can you find an alignment that maximizes the number of satisfied preferences?

Viewpoint and Constraints

The model has a variable pers[p] for every person, where pers[p] stands for the position i takes in the alignment. Since there are exactly 7 persons, we have pers[p] $\in$ 1 # 7 for every person p. Moreover, we have pers[p] $\neq$ pers[q] for every pair p,q of distinct persons. The model has a variable S_i $\in$ 0 # 1 for each of the 8 preferences, where S_i = 1 if and only if the i-th preference is satisfied. To express this constraint, we constrain the control variable S of a preference ``person p wants to stand next to person q'' by means of the reified constraint

(| pers[p] - pers[q]| = 1 $\leftrightarrow$ S = 1)$\land$S $\in$ 0#1

Finally, there is a variable

Satisfaction = S₁ + ... + S₈

denoting the number of satisfied preferences. We want to find a solution that maximizes the value of Satisfaction.

The experienced constraint programmer will note that we can eliminate a symmetry by picking two persons p and q and imposing the order constraint

pers[p] < pers[q]

Branching Strategy

To maximize Satisfaction, we employ a two-dimensional branching strategy, which first branches on Satisfaction, trying the values 8,7,... ,1 in this order. Once Satisfaction is determined, we branch on the variables pers using a first-fail strategy that splits the domain of the selected variable.

Script

fun photo space =
   let 
       val pers as #[b,c,d,f,g,m,p]= FD.rangeVec(space,7,(1,7))
      (* si is 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))
   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,#[satisfaction],FD.B_NONE,FD.B_MAX);
       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}  
  end

The statement Explorer.exploreOne(photo) will run the script until a first solution is found. The first solution satisfies 6 preferences and looks as follows:

{Betty = intvar{|5 |}, Chris = intvar{|6 |},
Donald = intvar{|1 |}, Fred = intvar{|3 |},
Gary = intvar{|7 |}, Mary = intvar{|4 |},
Paul = intvar{|2 |}, satisfaction = intvar{|6 |}}

By construction of the script, this is the maximal number of preferences that can be satisfied simultaneously.