diff --git a/predicates/tableseating/table_seating.mzn b/predicates/tableseating/table_seating.mzn index ca0ebe0..f678d71 100644 --- a/predicates/tableseating/table_seating.mzn +++ b/predicates/tableseating/table_seating.mzn @@ -2,47 +2,60 @@ enum SCHOLAR; array[SCHOLAR] of int: reputation; int: maxreputation = max(reputation); -int: T; +int: T; % number of tables set of int: TABLE = 1..T; -int: S; % tables size +int: S; % common table size array[int,1..2] of SCHOLAR: enemies; array[int,1..2] of SCHOLAR: friends; array[TABLE] of var set of SCHOLAR: table; -constraint forall(t in TABLE)(card(table[t]) != 1); - predicate not_same_table(SCHOLAR: p1, SCHOLAR: p2) = forall(t in TABLE)(not ({p1,p2} subset table[t])); +% No table occupied by a a scholar all by his lonesome +% and no table occupied beyond its capacity +constraint forall(t in TABLE)(card(table[t]) != 1); constraint forall(t in TABLE)(card(table[t]) <= S); +% Every scholar is sitting on at least 1 table constraint forall(p in SCHOLAR)(exists(t in TABLE)(p in table[t])); + +% A scholar can only sit at at most 1 table ("two different +% tables cannot seat the same scholar") constraint forall(t1, t2 in TABLE where t1 < t2) (table[t1] intersect table[t2] = {}); -% enemies not on same table +% Enemies not on same table constraint forall(c in index_set_1of2(enemies)) (not_same_table(enemies[c,1],enemies[c,2])); -% friends on same table +% Friends on same table constraint forall(c in index_set_1of2(friends)) (not(not_same_table(friends[c,1],friends[c,2]))); -% important persons (reputation 10) not on same table +% Important persons (reputation 10) not on same table constraint forall(p1,p2 in SCHOLAR where p1 < p2 /\ reputation[p1] = 10 /\ reputation[p2] = 10) (not_same_table(p1,p2)); -% Use as few tables as possible +% Primary objective: use as few tables as possible var int: obj1; constraint obj1 = sum(t in TABLE)(card(table[t]) != 0); +% Secondary objective: minimize the difference in reputation over all tables var int: obj2; constraint obj2 = sum(t in TABLE) (let {var int: minRep = min([reputation[p]*(p in table[t]) + maxreputation*(1-(p in table[t])) | p in SCHOLAR]); var int: maxRep = max([reputation[p]*(p in table[t]) | p in SCHOLAR]); } in if minRep = maxreputation then 0 else maxRep - minRep endif); +% Hierarchy of objectives: +% obj1(sol1) < obj1(sol2) -> obj(sol1) < obj(sol2) +% obj1(sol1) = obj1(sol2) -> (obj2(sol1) < obj2(sol2) -> obj(sol1) < obj(sol2)) + +% var obj = (obj1*(obj2_range+1) + obj2); +% int: obj2_range = S * (maxreputation - minreputation) = 5 * 9 = 45; % choose 100 + solve minimize (obj1*100 + obj2); output ["Table \(t): \(table[t])\n" | t in TABLE] ++ ["Obj1: \(obj1) and Obj2: \(obj2)\n"]; diff --git a/predicates/tableseating/table_seating_imp.mzn b/predicates/tableseating/table_seating_imp.mzn index 435a593..fedf6e3 100644 --- a/predicates/tableseating/table_seating_imp.mzn +++ b/predicates/tableseating/table_seating_imp.mzn @@ -6,49 +6,64 @@ int: maxreputation = max(reputation); int: T; % number of tables set of int: TABLE = 1..T; -int: S; % tables size +int: S; % common table size array[int,1..2] of SCHOLAR: enemies; array[int,1..2] of SCHOLAR: friends; array[TABLE] of var set of SCHOLAR: table; array[SCHOLAR] of var TABLE: seat; -% No for lonely table -constraint forall(t in TABLE)(card(table[t]) != 1); - -% value symmetry breaking -constraint value_precede_chain([t | t in 1..T], seat); - predicate not_same_table(SCHOLAR: p1, SCHOLAR: p2) = seat[p1] != seat[p2]; +% The scholar->table "seat" mapping is dual to the table->{scholar} "table" subsetting +constraint forall(t in TABLE, p in SCHOLAR)(p in table[t] <-> seat[p] = t); + +% No table occupied by a a scholar all by his lonesome +constraint forall(t in TABLE)(card(table[t]) != 1); + +% Each table seats between 0 and 5 scholars +% (p.292 of the handbook) constraint global_cardinality_low_up(seat, [t|t in TABLE], [0|t in TABLE], [S|t in TABLE]); -% enemies not on same table +% Enemies not on same table constraint forall(c in index_set_1of2(enemies)) (not_same_table(enemies[c,1],enemies[c,2])); -% friends on same table +% Friends on same table constraint forall(c in index_set_1of2(friends)) (not(not_same_table(friends[c,1],friends[c,2]))); -% important persons (reputation 10) not on same table +% Important persons (reputation 10) not on same table constraint forall(p1,p2 in SCHOLAR where p1 < p2 /\ reputation[p1] = 10 /\ reputation[p2] = 10) (not_same_table(p1,p2)); -% Use as few tables as possible +% Value symmetry breaking. +% (p.298 of the handbook) +% If seat[scholar_high] = t[i+1] then +% there is at least one scholar_low < scholar_high such that +% seat[scholar_low] = t[i] +constraint value_precede_chain([t | t in 1..T], seat); + +% Primary objective: use as few tables as possible var int: obj1; constraint obj1 = sum(t in TABLE)(card(table[t]) != 0); -% minimize the difference in reputation in each table +% Secondary objective: minimize the difference in reputation over all tables var int: obj2; constraint obj2 = sum(t in TABLE) (let {var int: minRep = min([reputation[p]*(seat[p] = t) + maxreputation*(seat[p] != t) | p in SCHOLAR]); var int: maxRep = max([reputation[p]*(seat[p] = t) | p in SCHOLAR]); } in if minRep = maxreputation then 0 else maxRep - minRep endif); -constraint forall(t in TABLE, p in SCHOLAR)(p in table[t] <-> seat[p] = t); +% Hierarchy of objectives: +% obj1(sol1) < obj1(sol2) -> obj(sol1) < obj(sol2) +% obj1(sol1) = obj1(sol2) -> obj2(sol1) < obj2(sol2) -> obj(sol1) < obj(sol2) + +% var obj = (obj1*(obj2_range+1) + obj2); +% int: obj2_range = S * (maxreputation - minreputation) = 5 * 9 = 45; % choose 100 solve minimize (obj1*100 + obj2); output ["Table \(t): \(table[t])\n" | t in TABLE] ++ ["Obj1: \(obj1) and Obj2: \(obj2)\n"]; +