**Subsections**

##

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.

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:
- Betty wants to stand next to Gary and Mary.
- Chris wants to stand next to Betty and Gary.
- Fred wants to stand next to Mary and Donald.
- 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?

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*] 1 # 7 for every person p. Moreover, we
have
*pers*[*p*] *pers*[*q*] for every pair p,q of distinct persons. The model
has a variable *S*_{i} 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 *S* = 1)*S* 0#1

Finally, there is a variable
Satisfaction = *S*_{1} + ... + *S*_{8}

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*]

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.

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.

Andreas Rossberg
2006-08-28