Annotated redundant constraints

amaze/amaze3.mzn

@@ -86,9 +86,9 @@ constraint
  endif
  );
 
- % Some redudant constraints
+ % Some redundant constraints
  %
-constraint
+constraint redundant_constraint(
  forall(i in Pairs)(
  let {
  int: x1 = min(end_points_start_x[i], end_points_end_x[i]),
@@ -111,7 +111,8 @@ constraint
  true
  endif
  )
- );
+ )
+);
 
 %------------------------------------------------------------------------------%
 % Search

bacp/curriculum.mzn.model

@@ -57,13 +57,15 @@ predicate prerequisite(courses: a, courses: b) =
 
 % add some redundant linear constraints
 
-constraint forall(p in 0..n_periods-1) (
+constraint redundant_constraint(
+ forall(p in 0..n_periods-1) (
  let {
  var 0..max_course_load: l = sum(c in courses) (bool2int(course_period[c] > p) * course_load[c])
  } in 
  l >= (n_periods-p) * load_per_period_lb /\
  l <= (n_periods-p) * objective
- );
+ )
+);
 
 solve :: seq_search([
  int_search([x[i,j] | i in periods, j in courses], input_order, indomain_max, complete),

bibd/bibd.mzn

@@ -44,15 +44,19 @@ constraint
 
  % Break row symmetry in the incidence matrix.
  %
-constraint forall(i in rows diff {max(rows)})(
+constraint symmetry_breaking_constraint(
+ forall(i in rows diff {max(rows)})(
  lex_lesseq([m[i, j] | j in cols], [m[i+1, j] | j in cols])
- );
+ )
+);
 
  % Break column symmetry in the incidence matrix.
  %
-constraint forall(j in cols diff {max(cols)})(
+constraint symmetry_breaking_constraint(
+ forall(j in cols diff {max(cols)})(
  lex_lesseq([m[i, j] | i in rows], [m[i, j+1] | i in rows])
- );
+ )
+);
 
 solve :: bool_search([m[i, j] | i in rows, j in cols],
  input_order, indomain_min, complete)

carpet-cutting/cc_base.mzn

@@ -191,7 +191,7 @@ constraint
  );
 
  % Symmetry breaking constraints between steps of a stair carpet
-constraint
+constraint symmetry_breaking_constraint(
  forall(i in Stairs, j1 in st_rec_ids[i] where (j1 + 1) in st_rec_ids[i])(
  let {
  int: j2 = j1 + 1
@@ -201,7 +201,8 @@ constraint
  -> st_rec_x[j1] + st_rec_len[j1] <= st_rec_x[j2]
  )
  )
- );
+ )
+);
 
  % Minimal steps and maximal breaks constraints
 constraint

carpet-cutting/cc_base.mzn-fixed

@@ -199,7 +199,7 @@ constraint
  );
 
  % Symmetry breaking constraints between steps of a stair carpet
-constraint
+constraint symmetry_breaking_constraint(
  forall(i in Stairs, j1 in st_rec_ids[i] where (j1 + 1) in st_rec_ids[i])(
  let {
  int: j2 = j1 + 1
@@ -209,7 +209,8 @@ constraint
  -> st_rec_x[j1] + st_rec_len[j1] <= st_rec_x[j2]
  )
  )
- );
+ )
+);
 
  % Minimal steps and maximal breaks constraints
 constraint

curriculum/curriculum.mzn.model

@@ -56,11 +56,13 @@ predicate prerequisite(courses: a, courses: b) =
 
 % add some redundant linear constraints
 
-constraint forall(p in 0..n_periods-1) (
+constraint redundant_constraint(
+ forall(p in 0..n_periods-1) (
  let {var int: l = sum(c in courses) (bool2int(course_period[c] > p) * course_load[c])} in 
  l >= (n_periods-p) * load_per_period_lb /\
  l <= (n_periods-p) * objective
- );
+ )
+);
 
 solve :: seq_search([
  int_search([objective], input_order, indomain_min, complete),

cyclic-rcpsp/rcmsp.mzn

@@ -97,14 +97,15 @@ constraint
 
  % Redundant non-overlapping constraints
  %
-constraint
+constraint redundant_constraint(
  forall(i, j in Tasks where i < j)(
  if exists(r in Res)(rreq[i, r] + rreq[j, r] > rcap[r]) then
  s[i] + d[i] <= s[j] \/ s[j] + d[j] <= s[i] 
  else
  true
  endif
- );
+ )
+);
 
  % Cumulative resource constraints
  %
@@ -140,8 +141,9 @@ constraint
 
  % Symmetry breaking constraint
  %
-constraint
- s[1] = 0 /\ k[1] = 0;
+constraint symmetry_breaking_constraint(
+ s[1] = 0 /\ k[1] = 0
+);
 
 %-----------------------------------------------------------------------------%
 % Objective.

debruijn_binary/debruijn_binary.mzn

@@ -72,7 +72,7 @@ constraint alldifferent(x) ;
 
 % Symmetry breaking: the minimum element should be the first element.
 %
-constraint minimum(x[1], x);
+constraint symmetry_breaking_constraint(minimum(x[1], x));
 
 % Converts x <-> binary (for all_different(x) )
 %

depot-placement/depot_placement.mzn

@@ -148,8 +148,8 @@ constraint
 % Actually, because of the previous constraint, this is REDUNDANT for minimising
 % distance - as the data satisfies the triangle inequality
 %
-constraint alldifferent([TourALoc[N]|N in 2..ASize]) ;
-constraint alldifferent([TourBLoc[N]|N in 2..BSize]) ;
+constraint redundant_constraint(alldifferent([TourALoc[N]|N in 2..ASize])) ;
+constraint redundant_constraint(alldifferent([TourBLoc[N]|N in 2..BSize])) ;
 
 % The warehouse must be visited first
 %
@@ -158,11 +158,11 @@ constraint TourALoc[1] = AWHouse ;
 % REDUNDANT constraint - don't come back to the Warehouse until all the
 % deliveries are done!
 %
-constraint forall (N in 3..ASize) (TourALoc[N] != AWHouse) ;
+constraint redundant_constraint(forall (N in 3..ASize) (TourALoc[N] != AWHouse)) ;
 
 % REDUNDANT constraint.
 %
-constraint forall (N in 1..ASize) (TourALoc[N] != BWHouse) ;
+constraint redundant_constraint(forall (N in 1..ASize) (TourALoc[N] != BWHouse)) ;
 
 constraint TourBLoc[1] = BWHouse ;
 constraint forall (N in 3..BSize) (TourBLoc[N] != BWHouse) ;

elitserien/handball.mzn

@@ -284,44 +284,51 @@ constraint
 %% IMPLIED CONSTRAINTS
 
 % channel contestant <---> hap (3)
-constraint
+constraint redundant_constraint(
  forall(t in teams, p in period)(
  contestant[t,p]=t <-> hap[t,p]=B
- );
+ )
+);
 
 % exactly six aligned breaks per division (10)
-constraint
+constraint redundant_constraint(
  sum(t in north_teams )(bool2int(break[t]>0)) = 6 /\
- sum(t in south_teams)(bool2int(break[t]>0)) = 6;
+ sum(t in south_teams)(bool2int(break[t]>0)) = 6
+);
 
 % The byes that each division has in Part~I occur in different weeks -- (11)
-% constraint
+% constraint redundant_constraint(
 % let {array[1..14] of var 1..14: bye} in (
 % forall(t in 1.. 7)(hap[t,bye[t]] = B) /\
 % forall(t in 8..14)(hap[t,bye[t]-7] = B) /\
 % alldifferent(bye) :: domain
-% );
+% )
+% );
 
 % exactly two occurrences of every break period (12)
-constraint
- global_cardinality_closed(break, [0,9,11,13,15,17,19], [2,2,2,2,2,2,2]);
+constraint redundant_constraint(
+ global_cardinality_closed(break, [0,9,11,13,15,17,19], [2,2,2,2,2,2,2])
+);
 
 %% SYMMETRY-BREAKING CONSTAINTS
 
 % SYMMETRY: global home/away (13)
-% constraint
-% hap[1,2] = H /\ hap[2,1] = A;
+% constraint symmetry_breaking_constraint(
+% hap[1,2] = H /\ hap[2,1] = A
+% );
 
 % SYMMETRY: North/South division (14)
-% constraint
-% lex_greater([break[i] | i in 1..2], [break[i] | i in 8..9]);
+% constraint symmetry_breaking_constraint(
+% lex_greater([break[i] | i in 1..2], [break[i] | i in 8..9])
+% );
 
 % SYMMETRY: fix bye period (15)
-constraint
+constraint symmetry_breaking_constraint(
  forall(t in north_teams)(
  hap[t,t] = B /\ 
  hap[t+divsize,t] = B
- );
+ )
+);
 
 % each division must have 3 pairs of complementary schedules (16)
 % - only 1/2, 2/3, 3/4, 4/5, 5/6, 6/7 can be complementary

freepizza/freepizza.mzn

@@ -34,9 +34,11 @@ constraint forall(p1, p2 in PIZZA)((how[p1] < how[p2] /\ how[p1] = -how[p2])
 
 
 % symmetry breaking
-%constraint forall(v1, v2 in VOUCHER where v1 < v2 /\ buy[v1] = buy[v2] /\ free[v1] = free[v2])
+%constraint symmetry_breaking_constraint(
+% forall(v1, v2 in VOUCHER where v1 < v2 /\ buy[v1] = buy[v2] /\ free[v1] = free[v2])
 % (forall(p1, p2 in PIZZA where price[p1] < price[p2])
-% (how[p1] = -v2 -> how[p2] != -v1));
+% (how[p1] = -v2 -> how[p2] != -v1))
+%);
 
 
 

ghoulomb/ghoulomb.mzn

@@ -51,7 +51,7 @@ predicate ghoulomb(array[int] of var int: mark,
  /\ forall ( i in 1..m-1) ( mark[i] < mark[i+1] )
  /\ distinct(differences) :: bounds
  % Symmetry breaking
- /\ differences[1] < differences[(m*(m-1)) div 2]
+ /\ symmetry_breaking_constraint(differences[1] < differences[(m*(m-1)) div 2])
  );
 
 

golfers/golfers1.mzn

@@ -35,13 +35,14 @@ constraint
 
  % Break some symmetry by strictly ordering each group in each round.
  %
-constraint
+constraint symmetry_breaking_constraint(
  forall (r in rounds, p in places) (
  if p mod n_per_group != 0
  then round_place_golfer[r, p] < round_place_golfer[r, p + 1]
  else true
  endif
- );
+ )
+);
 
  % Each pair can play together at most once.
  %

golfers/golfers1b.mzn

@@ -35,20 +35,22 @@ constraint
 
  % Break some symmetry by strictly ordering each group in each round.
  %
-constraint
+constraint symmetry_breaking_constraint(
  forall (r in rounds, p in places) (
  if p mod n_per_group != 0
  then round_place_golfer[r, p] < round_place_golfer[r, p + 1]
  else true
  endif
- );
+ )
+);
 
  % Break some more symmetry by strictly ordering the groups in each round.
  %
-constraint
+constraint symmetry_breaking_constraint(
  forall (r in rounds, g in [1 + i * n_per_group | i in 0..n_groups-2]) (
  round_place_golfer[r, g] < round_place_golfer[r, g+n_per_group]
- );
+ )
+);
 
  % Each pair can play together at most once.
  %

golfers/golfers2.mzn

@@ -36,10 +36,11 @@ constraint
  % We also break some symmetry
  % here by strictly ordering each group.
  %
-constraint
+constraint symmetry_breaking_constraint(
  forall (r in rounds, g in groups, i in group where i < n_per_group) (
  round_group_i_golfer[r, g, i] < round_group_i_golfer[r, g, i + 1]
- );
+ )
+);
 
  % Each pair can play together at most once.
  %

golfers/golfers3.mzn

@@ -42,10 +42,11 @@ constraint
 
  % Symmetry breaking.
  %
-% constraint
+% constraint symmetry_breaking_constraint(
 % forall (r in rounds, g in groups where g < n_groups) (
 % round_group_golfers[r, g] < round_group_golfers[r, g + 1]
-% );
+% )
+%);
 
  % Each pair may play together at most once.
  %

golomb/golomb.mzn

@@ -29,7 +29,7 @@ constraint forall ( i in 1..m-1 ) ( mark[i] < mark[i+1] );
 constraint alldifferent(differences);
 
  % Symmetry breaking
-constraint differences[1] < differences[(m*(m-1)) div 2];
+constraint symmetry_breaking_constraint(differences[1] < differences[(m*(m-1)) div 2]);
 
 solve :: int_search(mark, input_order, indomain, complete)
  minimize mark[m];

is/model.mzn

@@ -417,7 +417,7 @@ constraint redundant_constraint(
 );
 
 % Ad hoc: detect symmetry among location values 1..31
-constraint redundant_constraint (
+constraint symmetry_breaking_constraint (
  forall(i in index_set_1of2(funLocDomain))(
  let {int: lo = funLocDomain[i,2],
  int: hi = funLocDomain[i,3]} in

knights/knights.mzn

@@ -19,10 +19,10 @@ constraint alldifferent([n * r[i] + c[i] | i in 1..m]);
 
  % Break some symmetries by forcing the first moves.
  %
-constraint r[1] = 1;
-constraint c[1] = 1;
-constraint r[2] = 2;
-constraint c[2] = 3;
+constraint symmetry_breaking_constraint(r[1] = 1);
+constraint symmetry_breaking_constraint(c[1] = 1);
+constraint symmetry_breaking_constraint(r[2] = 2);
+constraint symmetry_breaking_constraint(c[2] = 3);
 
  % There is only one place for the last move.
  %

linear-to-program/linear-to-program.mzn

@@ -66,10 +66,11 @@ constraint alldifferent(line_o);
 constraint forall(i in R, j in Ii[i]) (line_i[j] < line_o[i]);
 
 %symmetry breaking of the program
-constraint 
+constraint symmetry_breaking_constraint(
  forall(i in M..M+Np-2) (line_o[i] < line_o[i+1]) % all plus are equivalent
  /\ forall(i in M+Np..M+N-2)(line_o[i] < line_o[i+1]) % all minus are equivalent
- /\ forall(i in M..M+Np-1)(line_i[min(Ii[i])] <= line_i[min(Ii[i])+1]); % plus is commutative
+ /\ forall(i in M..M+Np-1)(line_i[min(Ii[i])] <= line_i[min(Ii[i])+1]) % plus is commutative
+);
 
 
 

mqueens/mqueens2.mzn

@@ -69,7 +69,7 @@ constraint forall(i in 1..n)(
 
 constraint objective = sum(i in 1..n)(bool2int(q[i] > 0));
 
-constraint rot_sqr_sym(f); 
+constraint symmetry_breaking_constraint(rot_sqr_sym(f));
 
 %------------------------------------------------------------------------------%
 % Search