diff --git a/amaze/amaze3.mzn b/amaze/amaze3.mzn index 062a84f0d..7293b02c3 100644 --- a/amaze/amaze3.mzn +++ b/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 diff --git a/bacp/curriculum.mzn.model b/bacp/curriculum.mzn.model index 592e65050..f8b78168d 100644 --- a/bacp/curriculum.mzn.model +++ b/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), diff --git a/bibd/bibd.mzn b/bibd/bibd.mzn index a7587a2f9..2d066c9ed 100644 --- a/bibd/bibd.mzn +++ b/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) diff --git a/carpet-cutting/cc_base.mzn b/carpet-cutting/cc_base.mzn index 797d9f433..b210b52ff 100644 --- a/carpet-cutting/cc_base.mzn +++ b/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 diff --git a/carpet-cutting/cc_base.mzn-fixed b/carpet-cutting/cc_base.mzn-fixed index 23c7e7010..3f7bf1770 100644 --- a/carpet-cutting/cc_base.mzn-fixed +++ b/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 diff --git a/curriculum/curriculum.mzn.model b/curriculum/curriculum.mzn.model index b675fa074..00486fece 100644 --- a/curriculum/curriculum.mzn.model +++ b/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), diff --git a/cyclic-rcpsp/rcmsp.mzn b/cyclic-rcpsp/rcmsp.mzn index 806807257..b2112b69b 100644 --- a/cyclic-rcpsp/rcmsp.mzn +++ b/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. diff --git a/debruijn_binary/debruijn_binary.mzn b/debruijn_binary/debruijn_binary.mzn index 33843311f..9a0698df9 100644 --- a/debruijn_binary/debruijn_binary.mzn +++ b/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) ) % diff --git a/depot-placement/depot_placement.mzn b/depot-placement/depot_placement.mzn index 4d79b6b10..2219557d5 100644 --- a/depot-placement/depot_placement.mzn +++ b/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) ; diff --git a/elitserien/handball.mzn b/elitserien/handball.mzn index 814cf4436..d437c007a 100644 --- a/elitserien/handball.mzn +++ b/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 diff --git a/freepizza/freepizza.mzn b/freepizza/freepizza.mzn index e23398d5c..230eb76b5 100644 --- a/freepizza/freepizza.mzn +++ b/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)) +%); diff --git a/ghoulomb/ghoulomb.mzn b/ghoulomb/ghoulomb.mzn index 78223419a..40b141ccc 100644 --- a/ghoulomb/ghoulomb.mzn +++ b/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]) ); diff --git a/golfers/golfers1.mzn b/golfers/golfers1.mzn index 174f1e54b..e08de7067 100644 --- a/golfers/golfers1.mzn +++ b/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. % diff --git a/golfers/golfers1b.mzn b/golfers/golfers1b.mzn index 3d6ca574d..397de9638 100644 --- a/golfers/golfers1b.mzn +++ b/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. % diff --git a/golfers/golfers2.mzn b/golfers/golfers2.mzn index 14ebb35f4..08d767991 100644 --- a/golfers/golfers2.mzn +++ b/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. % diff --git a/golfers/golfers3.mzn b/golfers/golfers3.mzn index 76b08363f..d8bbf4ad5 100644 --- a/golfers/golfers3.mzn +++ b/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. % diff --git a/golomb/golomb.mzn b/golomb/golomb.mzn index 7574965ae..55ddc049b 100644 --- a/golomb/golomb.mzn +++ b/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]; diff --git a/is/model.mzn b/is/model.mzn index e7f56d0bf..c919ff48c 100644 --- a/is/model.mzn +++ b/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 diff --git a/knights/knights.mzn b/knights/knights.mzn index 5d91313eb..e15563654 100644 --- a/knights/knights.mzn +++ b/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. % diff --git a/linear-to-program/linear-to-program.mzn b/linear-to-program/linear-to-program.mzn index 92ea3cf39..6275530a2 100644 --- a/linear-to-program/linear-to-program.mzn +++ b/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 +); diff --git a/mqueens/mqueens2.mzn b/mqueens/mqueens2.mzn index 43068f919..d41cfe16d 100644 --- a/mqueens/mqueens2.mzn +++ b/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 diff --git a/mspsp/mspsp.mzn b/mspsp/mspsp.mzn index c26bd5e3f..b941fd960 100644 --- a/mspsp/mspsp.mzn +++ b/mspsp/mspsp.mzn @@ -90,7 +90,7 @@ constraint % Redundant non-overlapping constraints for the workers % -constraint +constraint redundant_constraint( forall ( j in Workers ) ( let { @@ -110,11 +110,12 @@ constraint true endif ) - ); + ) +); % Redundant non-overlapping constraints % -constraint +constraint redundant_constraint( forall ( i, j in Tasks where @@ -128,11 +129,12 @@ constraint else true endif - ); + ) +); - % Redudant cumulative resource constraints + % Redundant cumulative resource constraints % -constraint +constraint redundant_constraint( forall ( k in Skills ) ( let { @@ -150,7 +152,8 @@ constraint true endif ) - ); + ) +); % Makespan constraints % diff --git a/pattern-set-mining/pattern_set_mining.mzn b/pattern-set-mining/pattern_set_mining.mzn index eaffbe36e..3765fc44a 100644 --- a/pattern-set-mining/pattern_set_mining.mzn +++ b/pattern-set-mining/pattern_set_mining.mzn @@ -55,13 +55,14 @@ constraint % closed on positives: an Item is in, iff all Trans_pos where the Ite ); % Canonical form (breaking symmetry) -constraint % lexicographic ordering of the trans +constraint symmetry_breaking_constraint(% lexicographic ordering of the trans forall(d in 1..K-1) ( lex_less([TransP[d,t]|t in 1..NrT_pos], [TransP[d+1,t]|t in 1..NrT_pos]) /\ lex_less([TransN[d,t]|t in 1..NrT_neg], [TransN[d+1,t]|t in 1..NrT_neg]) - ); + ) +); % Joint coverage constraint % covered when OR of any pattern diff --git a/photo/photo.mzn b/photo/photo.mzn index f0ce96e50..416dbed8b 100644 --- a/photo/photo.mzn +++ b/photo/photo.mzn @@ -46,8 +46,9 @@ constraint alldifferent(pos); % Break some symmetry -constraint - pos[0] < pos[1]; +constraint symmetry_breaking_constraint( + pos[0] < pos[1] +); solve :: int_search(pos, first_fail, indomain, complete) maximize satisfies; diff --git a/quickcheck.sh b/quickcheck.sh new file mode 100755 index 000000000..333c72801 --- /dev/null +++ b/quickcheck.sh @@ -0,0 +1,25 @@ +#!/bin/bash +# For each problem, tries to compile the "smallest" instance. + +for PROBLEM_DIR in $(find . -mindepth 1 -maxdepth 1 -type d ! -name .git) +do + OUTPUT_DIR=/tmp/minizinc-benchmarks/$PROBLEM_DIR + mkdir -p $OUTPUT_DIR + cd $PROBLEM_DIR + MODEL_FILES=$(find . -type f -iname '*.mzn') + DATA_FILES=$(find . -type f -iname '*.dzn') + if [ -n "$DATA_FILES" ] + then + SMALLEST_DATA_FILE=$(ls -Sr $DATA_FILES | head -n 1) + for MODEL_FILE in $MODEL_FILES + do + echo "Instantiating $MODEL_FILE with $SMALLEST_DATA_FILE" + mzn2fzn --output-base $OUTPUT_DIR/$(basename -s .dzn $SMALLEST_DATA_FILE) $MODEL_FILE $SMALLEST_DATA_FILE + done + else + SMALLEST_MODEL_FILE=$(ls -Sr $MODEL_FILES | head -n 1) + echo "Compiling $SMALLEST_MODEL_FILE" + mzn2fzn --output-base $OUTPUT_DIR/$(basename -s .mzn $SMALLEST_MODEL_FILE) $SMALLEST_MODEL_FILE + fi + cd .. +done diff --git a/rcpsp-max/rcpsp_max.mzn b/rcpsp-max/rcpsp_max.mzn index 6c885319d..36458565b 100644 --- a/rcpsp-max/rcpsp_max.mzn +++ b/rcpsp-max/rcpsp_max.mzn @@ -78,7 +78,7 @@ constraint ); % Redundant non-overlapping (dijunctive) constraints -constraint +constraint redundant_constraint( forall (i, j in Tasks where i < j) ( if exists(res in Res where rr[res, i] + rr[res, j] > rcap[res])(true) then % Activities i, and j cannot run in parallel @@ -112,7 +112,8 @@ constraint else true endif - ); + ) +); % Cumulative resource constraints constraint diff --git a/rcpsp/rcpsp.mzn b/rcpsp/rcpsp.mzn index d7d2a1a9a..c3d2134a1 100644 --- a/rcpsp/rcpsp.mzn +++ b/rcpsp/rcpsp.mzn @@ -61,7 +61,7 @@ constraint % Redundant non-overlapping constraints % -constraint +constraint redundant_constraint( forall ( i, j in Tasks where i < j ) ( if exists(r in Res)(rr[r, i] + rr[r, j] > rc[r]) then @@ -69,7 +69,8 @@ constraint else true endif - ); + ) +); % Cumulative resource constraints % diff --git a/rectangle-packing/rect_packing.mzn b/rectangle-packing/rect_packing.mzn index 54d009c1e..24bc36d52 100644 --- a/rectangle-packing/rect_packing.mzn +++ b/rectangle-packing/rect_packing.mzn @@ -137,9 +137,10 @@ constraint % Model improvements. % % Symmetry breaking rules -constraint +constraint symmetry_breaking_constraint( 2 * X[n] <= (Width - n) - /\ 2 * Y[n] <= (Height - n); + /\ 2 * Y[n] <= (Height - n) +); % Empty Strip Dominance Criterion % NOTE: Here only an adaption of it from H. Simonis, B. O'Sullivan, "Search @@ -154,7 +155,7 @@ array [1..45] of int: fgaps = [0, 2, 3, 2, 3, 3, 3, 3, 4, 4, 9, 9, 9, 9, 10]; % Forbidden gaps for the x-origin -constraint +constraint redundant_constraint( forall( i in Squares where consider_square(i) ) ( if 2 * fgaps[i] + 2 <= max_width - i then let { @@ -175,10 +176,11 @@ constraint /\ ( not( b_left ) -> X[i] >= Width - i ) ) endif - ); + ) +); % Forbidden gaps for the y-origin -constraint +constraint redundant_constraint( forall( i in Squares where consider_square(i) ) ( if 2 * fgaps[i] + 2 <= max_height - i then let { @@ -199,7 +201,8 @@ constraint /\ ( not( b_left ) -> Y[i] >= Height - i ) ) endif - ); + ) +); %-----------------------------------------------------------------------------% % Objective. diff --git a/rectangle-packing/rect_packing_mznc2014.mzn b/rectangle-packing/rect_packing_mznc2014.mzn index c59e59164..76ab7b213 100644 --- a/rectangle-packing/rect_packing_mznc2014.mzn +++ b/rectangle-packing/rect_packing_mznc2014.mzn @@ -181,9 +181,10 @@ constraint % Model improvements. % % Symmetry breaking rules -constraint +constraint symmetry_breaking_constraint( 2 * X[n] <= (Width - n) - /\ 2 * Y[n] <= (Height - n); + /\ 2 * Y[n] <= (Height - n) +); % Empty Strip Dominance Criterion % NOTE: Here only an adaption of it from H. Simonis, B. O'Sullivan, "Search @@ -198,7 +199,7 @@ array [1..45] of int: fgaps = [0, 2, 3, 2, 3, 3, 3, 3, 4, 4, 9, 9, 9, 9, 10]; % Forbidden gaps for the x-origin -constraint +constraint redundant_constraint( forall( i in Squares where consider_square(i) ) ( if 2 * fgaps[i] + 2 <= max_width - i then let { @@ -219,10 +220,11 @@ constraint /\ ( not( b_left ) -> X[i] >= Width - i ) ) endif - ); + ) +); % Forbidden gaps for the y-origin -constraint +constraint redundant_constraint( forall( i in Squares where consider_square(i) ) ( if 2 * fgaps[i] + 2 <= max_height - i then let { @@ -243,7 +245,8 @@ constraint /\ ( not( b_left ) -> Y[i] >= Height - i ) ) endif - ); + ) +); %-----------------------------------------------------------------------------% % Objective. diff --git a/rectangle-packing/rect_packing_opt.mzn b/rectangle-packing/rect_packing_opt.mzn index 54a67bc58..965676e5c 100644 --- a/rectangle-packing/rect_packing_opt.mzn +++ b/rectangle-packing/rect_packing_opt.mzn @@ -137,9 +137,10 @@ constraint % Model improvements. % % Symmetry breaking rules -constraint +constraint symmetry_breaking_constraint( 2 * X[n] <= (Width - n) - /\ 2 * Y[n] <= (Height - n); + /\ 2 * Y[n] <= (Height - n) +); % Empty Strip Dominance Criterion % NOTE: Here only an adaption of it from H. Simonis, B. O'Sullivan, "Search @@ -154,7 +155,7 @@ array [1..45] of int: fgaps = [0, 2, 3, 2, 3, 3, 3, 3, 4, 4, 9, 9, 9, 9, 10]; % Forbidden gaps for the x-origin -constraint +constraint redundant_constraint( forall( i in Squares where consider_square(i) ) ( if 2 * fgaps[i] + 2 <= max_width - i then let { @@ -175,10 +176,11 @@ constraint /\ ( not( b_left ) -> X[i] >= Width - i ) ) endif - ); + ) +); % Forbidden gaps for the y-origin -constraint +constraint redundant_constraint( forall( i in Squares where consider_square(i) ) ( if 2 * fgaps[i] + 2 <= max_height - i then let { @@ -199,7 +201,8 @@ constraint /\ ( not( b_left ) -> Y[i] >= Height - i ) ) endif - ); + ) +); %-----------------------------------------------------------------------------% % Objective. diff --git a/roster/roster_model.old b/roster/roster_model.old index 76ad6abcd..b4601244b 100644 --- a/roster/roster_model.old +++ b/roster/roster_model.old @@ -283,8 +283,9 @@ constraint % We can simply choose week1 to be any week (since the roster is cyclic). % Let's arbitrarily choose a week which starts with a rest day % This avoids searching among similar rosters. -constraint - roster[1,1] = Rest ; +constraint symmetry_breaking_constraint( + roster[1,1] = Rest +); %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/smelt/smelt.mzn b/smelt/smelt.mzn index 0386be8ae..ac9d6c7f7 100644 --- a/smelt/smelt.mzn +++ b/smelt/smelt.mzn @@ -56,7 +56,7 @@ constraint ); %% redundant lines constraint -constraint cumulative(start, duration, [1| i in 1..r], nl); +constraint redundant_constraint(cumulative(start, duration, [1| i in 1..r], nl)); %% Each line only has one product at a time constraint forall(i in 1..nl)( diff --git a/steiner-triples/steiner-triples.mzn b/steiner-triples/steiner-triples.mzn index 88f1532e1..c10036061 100644 --- a/steiner-triples/steiner-triples.mzn +++ b/steiner-triples/steiner-triples.mzn @@ -24,7 +24,7 @@ constraint forall(i in 1..nb, j in i+1..nb) ( card(sets[i] intersect sets[j]) <= 1 ); % Symmetry breaking: -constraint forall(i in 1..nb-1) ( sets[i] >= sets[i+1] ); +constraint symmetry_breaking_constraint(forall(i in 1..nb-1) ( sets[i] >= sets[i+1] )); solve :: set_search(sets, input_order, indomain_min, complete) satisfy; diff --git a/still-life-wastage/still-life.mzn b/still-life-wastage/still-life.mzn index 417d789ef..937813db8 100644 --- a/still-life-wastage/still-life.mzn +++ b/still-life-wastage/still-life.mzn @@ -72,7 +72,7 @@ constraint 4*OBJECTIVE = 2*n*n + 4*n - wastage_sum[n+1]; % redundant constraints using results from Chu et al. (2012). -constraint forall (i in 0..n) (wastage_sum[n+1] >= wastage_sum[i] + 2*((n-i) div 3) + n div 3); +constraint redundant_constraint(forall (i in 0..n) (wastage_sum[n+1] >= wastage_sum[i] + 2*((n-i) div 3) + n div 3)); % solve goal diff --git a/talent_scheduling/talent_scheduling.mzn b/talent_scheduling/talent_scheduling.mzn index eb77000ec..f7b77a625 100644 --- a/talent_scheduling/talent_scheduling.mzn +++ b/talent_scheduling/talent_scheduling.mzn @@ -55,7 +55,7 @@ constraint cost = sum(i in Scenes)( ); %-- symmetry breaking constraint -constraint s[1] < s[numScenes]; +constraint symmetry_breaking_constraint(s[1] < s[numScenes]); %-- Solving objective and solution output ------------------------------------- diff --git a/talent_scheduling/talent_scheduling_alt.mzn b/talent_scheduling/talent_scheduling_alt.mzn index 4af5c1411..5a1d27a0f 100644 --- a/talent_scheduling/talent_scheduling_alt.mzn +++ b/talent_scheduling/talent_scheduling_alt.mzn @@ -70,13 +70,18 @@ constraint forall(j in Actors)( %-- Redundant Constraints ----------------------------------------------------- %% implied constraint from Barbara Smith: cost on waiting time -constraint forall(j in Actors)( +constraint + redundant_constraint( + forall(j in Actors)( wait[j] >= lastSlot[j] - firstSlot[j] - card({ i | i in Scenes where ia[j,i] == 1 }) - ); + ) + ); % implied constraints on ordering of scenes -constraint forall(i,j in Scenes where a[i] superset a[j])( +constraint + redundant_constraint( + forall(i,j in Scenes where a[i] superset a[j])( let { set of Actors: diffn = a[i] diff a[j] } in @@ -91,7 +96,8 @@ constraint forall(i,j in Scenes where a[i] superset a[j])( else true endif endif - ); + ) + ); %-- calculating the objective function @@ -103,7 +109,7 @@ constraint cost = sum(j in Actors)( ); %-- symmetry breaking constraint -constraint s[1] < s[numScenes]; +constraint symmetry_breaking_constraint(s[1] < s[numScenes]); %-- Solving objective and solution output ------------------------------------- diff --git a/template_design/template_design.mzn b/template_design/template_design.mzn index a178c67c4..c80a60066 100644 --- a/template_design/template_design.mzn +++ b/template_design/template_design.mzn @@ -51,7 +51,7 @@ constraint % Symmetry constraints. % Variations with the same demand are symmetric. -constraint +constraint symmetry_breaking_constraint( forall(i in 1..n-1) ( if d[i] == d[i+1] then lex_lesseq([p[i, j] | j in 1..t], @@ -59,10 +59,11 @@ constraint else true endif - ); + ) +); % pseudo symmetry -constraint +constraint symmetry_breaking_constraint( forall(i in 1..n-1) ( if d[i] < d[i+1] then sum (j in 1..t) (p[i,j]*R[j]) @@ -70,7 +71,8 @@ constraint else true endif - ); + ) +); % implied constraints on the surplus @@ -79,32 +81,37 @@ constraint % sum(R[i]) constraint would produce the same amount of propagation % Set up surplus, which is bounded as production is bounded. -constraint - Surplus = Production*S - sum(i in 1..n)(d[i]); +constraint redundant_constraint( + Surplus = Production*S - sum(i in 1..n)(d[i]) +); % The surplus of each variation is also limited by the surplus. -constraint +constraint redundant_constraint( forall(k in 1..n) - (sum(j in 1..t)(p[k,j]*R[j]-d[k]) <= Surplus); + (sum(j in 1..t)(p[k,j]*R[j]-d[k]) <= Surplus) +); % The surplus of the first k variations is limited by the surplus. -constraint +constraint redundant_constraint( forall(k in 2..n-1) - (sum(j in 1..t, m in 1..k)( p[m,j]*R[j]-d[m] ) <= Surplus); + (sum(j in 1..t, m in 1..k)( p[m,j]*R[j]-d[m] ) <= Surplus) +); % Implied constraints on the run length. -constraint +constraint redundant_constraint( if t=2 then ( R[1] <= Production div 2 /\ R[2] >= Production div 2 - ) else true endif; + ) else true endif +); -constraint +constraint redundant_constraint( if t=3 then ( R[1] <= Production div 3 /\ R[2] <= Production div 2 /\ R[3] >= Production div 3 - ) else true endif; + ) else true endif +); % Minimize the production. solve :: int_search(array1d(1..n*t,p) ++ R, input_order, indomain_min, complete) diff --git a/train/train.mzn b/train/train.mzn index 3c23893be..0637ed46f 100644 --- a/train/train.mzn +++ b/train/train.mzn @@ -137,8 +137,11 @@ constraint forall (i in 1..n, j in 2..m) (((capacity-load[i,j-1] < 100) -> (collect[i,j] <= dwell[i,j]*20)) /\ ((capacity-load[i,j-1] >= 100) -> (collect[i,j] <= dwell[i,j]*50))); % (Redundant for j>=2 (but necessary for j=1)) -constraint forall (i in 1..n, j in 1..m) - (collect[i,j] <= (departure[i,j]-arrival[i,j])*50); +constraint forall (i in 1..n, j in 2..m) + (if j == 1 + then collect[i,j] <= (departure[i,j]-arrival[i,j])*50 + else redundant_constraint(collect[i,j] <= (departure[i,j]-arrival[i,j])*50) + endif); array [1..n, 1..m] of var 0..maxTime : dwell; constraint forall (i in 1..n, j in 1..m) (dwell[i,j] = departure[i,j] - arrival[i,j]); diff --git a/traveling-tppv/ttppv.mzn b/traveling-tppv/ttppv.mzn index 946c72f7b..0e0177c58 100644 --- a/traveling-tppv/ttppv.mzn +++ b/traveling-tppv/ttppv.mzn @@ -50,7 +50,7 @@ constraint forall (i in Teams, k in Rounds) (opponent[opponent[i,k],k] = i); constraint forall (i in Teams) (alldifferent([opponent[i,k] | k in Rounds])); % for each round k, all opponents are different (implied constraint) -constraint forall (k in Rounds) (alldifferent([opponent[i,k] | i in Teams])); +constraint redundant_constraint(forall (k in Rounds) (alldifferent([opponent[i,k] | i in Teams]))); % for each team i, there can be at most 3 consecutive home games and at most 3 consecutive away games int: nbStates = 7; @@ -66,7 +66,7 @@ array[States,1..2] of int: delta = constraint forall (i in Teams) (regular( [venue[i,k] | k in Rounds], nbStates, 2, delta, 1, States)); % symmetry breaking: distances are symmetric so reversing the rounds yields a schedule of same cost -constraint (opponent[1,1] < opponent[1,nbRounds]); +constraint symmetry_breaking_constraint(opponent[1,1] < opponent[1,nbRounds]); % define travel variables wrt venues of current- and next-round games constraint forall (i in Teams) (