From c42e57e25198f75437fb516b68192aa691a29e71 Mon Sep 17 00:00:00 2001 From: David Tonhofer Date: Thu, 22 Jul 2021 14:45:38 +0200 Subject: [PATCH 1/4] Added comments & de-symmetrizer Added some comments and a desymmetrizer (the latter however causes a different solution to be found) --- predicates/tableseating/table_seating.mzn | 29 ++++++++++++++++++----- 1 file changed, 23 insertions(+), 6 deletions(-) diff --git a/predicates/tableseating/table_seating.mzn b/predicates/tableseating/table_seating.mzn index ca0ebe0..0e79a74 100644 --- a/predicates/tableseating/table_seating.mzn +++ b/predicates/tableseating/table_seating.mzn @@ -10,39 +10,56 @@ 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 +% An arbitrary de-symmetrizer based on the integer label of a scholar +constraint forall(t1, t2 in TABLE where t1 < t2) + (sum([p*(p in table[t1]) | p in SCHOLAR]) >= sum([p*(p in table[t2]) | p in SCHOLAR])); + +% Primary objective: use as few tables as possible var int: obj1; constraint obj1 = sum(t in TABLE)(card(table[t]) != 0); +% Secondary objective: keep the sum of the reputation spread of each table small 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"]; From 29c5a154b907cf7c96b89305f923af15be066e56 Mon Sep 17 00:00:00 2001 From: David Tonhofer Date: Thu, 22 Jul 2021 15:38:41 +0200 Subject: [PATCH 2/4] Getting rif of the symmetry breaking (which is for later) --- predicates/tableseating/table_seating.mzn | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/predicates/tableseating/table_seating.mzn b/predicates/tableseating/table_seating.mzn index 0e79a74..bd228b6 100644 --- a/predicates/tableseating/table_seating.mzn +++ b/predicates/tableseating/table_seating.mzn @@ -2,9 +2,9 @@ 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; @@ -38,10 +38,6 @@ constraint forall(c in index_set_1of2(friends)) constraint forall(p1,p2 in SCHOLAR where p1 < p2 /\ reputation[p1] = 10 /\ reputation[p2] = 10) (not_same_table(p1,p2)); -% An arbitrary de-symmetrizer based on the integer label of a scholar -constraint forall(t1, t2 in TABLE where t1 < t2) - (sum([p*(p in table[t1]) | p in SCHOLAR]) >= sum([p*(p in table[t2]) | p in SCHOLAR])); - % Primary objective: use as few tables as possible var int: obj1; constraint obj1 = sum(t in TABLE)(card(table[t]) != 0); From a802217602a5a230ae00fd8afdb29c8c83b39c9e Mon Sep 17 00:00:00 2001 From: David Tonhofer Date: Thu, 22 Jul 2021 15:43:19 +0200 Subject: [PATCH 3/4] Added more comments for easier reading --- predicates/tableseating/table_seating_imp.mzn | 41 +++++++++++++------ 1 file changed, 28 insertions(+), 13 deletions(-) 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"]; + From d1838ae60bdbc27efe41e8556863f6c481009783 Mon Sep 17 00:00:00 2001 From: David Tonhofer Date: Thu, 22 Jul 2021 15:43:56 +0200 Subject: [PATCH 4/4] Comment fix --- predicates/tableseating/table_seating.mzn | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/predicates/tableseating/table_seating.mzn b/predicates/tableseating/table_seating.mzn index bd228b6..f678d71 100644 --- a/predicates/tableseating/table_seating.mzn +++ b/predicates/tableseating/table_seating.mzn @@ -42,7 +42,7 @@ constraint forall(p1,p2 in SCHOLAR where p1 < p2 /\ reputation[p1] = 10 /\ reput var int: obj1; constraint obj1 = sum(t in TABLE)(card(table[t]) != 0); -% Secondary objective: keep the sum of the reputation spread of each table small +% 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]);