Nontransitive dice, Ormat game, 17x17 challenge
Nontransitive dice
MiniZinc: nontransitive_dice.mznComet: nontransitive_dice.co
(Sidenote: This was triggered by a problem in Numberjack's Tutorial.)
Nontransitive dice is presented at Wikipedia as:
A set of nontransitive dice is a set of dice for which the relation "is more likely to roll a higher number" is not transitive. See also intransitivity. This situation is similar to that in the game Rock, Paper, Scissors, in which each element has an advantage over one choice and a disadvantage to the other.And then gives the following example:
Consider a set of three dice, A, B and C such thatHow easy is it to model such nontransitive dice in a high level constraint programming system such as MiniZinc or Comet? The basic MiniZinc model nontransitive_dice.mzn  with no bells and whistles  is this (somewhat edited):
* die A has sides {2,2,4,4,9,9},
* die B has sides {1,1,6,6,8,8}, and
* die C has sides {3,3,5,5,7,7}.
Then:
* the probability that A rolls a higher number than B is 5/9 (55.55 %),
* the probability that B rolls a higher number than C is 5/9, and
* the probability that C rolls a higher number than A is 5/9.
Thus A is more likely to roll a higher number than B, B is more likely to roll a higher number than C, and C is more likely to roll a higher number than A. This shows that the relation "is more likely to roll a higher number" is not transitive with these dice, and so we say this is a set of nontransitive dice.
int: m = 3; % number of dice int: n = 6; % number of sides of each die % the dice array[1..m, 1..n] of var 0..n*2: dice :: is_output; % the competitions: % The last wrap around is the one that breaks % the transitivity. array[0..m1, 1..2] of var 0..n*n: comp :: is_output; solve satisfy; constraint % order the number of each die forall(d in 1..m) ( increasing([dice[d,i]  i in 1..n]) ) ; % and now we roll... % Number of wins for [A vs B, B vs A] constraint forall(d in 0..m1) ( comp[d,1] = sum(r1, r2 in 1..n) ( bool2int(dice[1+(d mod m), r1] > dice[1+((d + 1) mod m), r2])) /\ comp[d,2] = sum(r1, r2 in 1..n) ( bool2int(dice[1+((d+1) mod m), r1] > dice[1+((d) mod m), r2])) ) ; % nontransitivity % All dice 1..m1 must beat the follower, % and die m must beat die 1 constraint forall(d in 0..m1) ( comp[d,1] > comp[d,2] ) ;The result of the
m
competitions is placed in the (m
x 2) matrix comp
where the winner is in comp[i,1]
and the loser in comp[i,2]
for the match i
. The last constraint section in the code above ensures that the winner is always in comp[i,1]
.
In the full model I have added the following:

max_val
: maximum value of the dice, to be minimized 
max_win
: maximum number of winnings, to be maximized 
gap
andgap_sum
: the difference of wins of a specific competition, to be maximized or minimized  the example setups from the Wikipedia page
import cotfd; int m = 3; // number of dice int n = 6; // number of sides of each die SolverThe full Comet model when minimzingcp(); // the dice var {int} dice[1..m, 1..n](cp, 1..n*2); // The competitions: var {int} comp[0..m1, 1..2](cp, 0..n*n); explore { // symmetry breaking: order the number of each die forall(d in 1..m) { forall(i in 2..n) { cp.post(dice[d,i1] <= dice[d,i]); } } // and now we roll... // Number of wins for [A vs B, B vs A] forall(d in 0..m1) { cp.post(comp[d,1] == sum(r1 in 1..n, r2 in 1..n) ( dice[1+(d % m), r1] > dice[1+((d + 1) % m), r2])); cp.post(comp[d,2] == sum(r1 in 1..n, r2 in 1..n) ( dice[1+((d+1) % m), r1] > dice[1+((d) % m), r2])); } forall(d in 0..m1) { cp.post(comp[d,1] > comp[d,2]); } } using { labelFF(dice); labelFF(comp); cout << "dice:" << endl; forall(i in 1..m) { forall(j in 1..n) { cout << dice[i,j] << " "; } cout << endl; } cout << endl; }
max_value
for 3 dice with 6 sides of each die (with domain 1..12), gives this result, i.e. the maximum value used in the dice is 4:
solution #1 dice: 1 1 1 2 4 4 1 1 1 3 3 3 1 2 2 2 2 2 comp: 1 vs 2: 15 (p:0.416667) 12 (p:0.333333) 2 vs 3: 18 (p:0.500000) 15 (p:0.416667) 3 vs 1: 15 (p:0.416667) 13 (p:0.361111) gap[3,3,2] max_val: 4 max_win: 18 gap_sum: 8Somewhat related is another dice problem: sicherman_dice.mzn.
17x17 challenge (not solved, though)
Last November, William Gasarch published a challenge in The 17x17 challenge. Worth $289.00. This is not a joke.. Also, see bitplayer's The 17×17 challenge, and O.R. by the Beach Let’s Join O.R. Forces to Crack the 17×17 Challenge.The objective is to create a 17x17 matrix where there are no colored subrectangles, i.e. no (sub)rectangles in the matrix can have the same color (number). Here's a solution of the 5x5x3 problem, i.e. 5 x 5 matrix and with 3 colors (1..3):
1 3 3 2 1 3 1 2 2 1 3 2 1 2 1 2 2 2 1 1 1 1 1 1 2When I first saw this problem in December, I tried some models but didn't pursued it further. However, when Karsten Konrad published some OPL models, I picked it up again. We also discussed this problem to see what a join force could do.
Here is my take in MiniZinc: 17_b.mzn. It is inspired (or rather a translation) of Karsten Konrad's OPL model from his blog post Let’s do real CP: forbiddenAssignment. Karsten earlier posted two OPL models:
 Improved Model for Coloring Problem which solve 17x17 with 5 colors without any sweat.
 17x17 challenge  not quite there
Here are three MiniZinc models with some different approaches. A Comet version is mentioned below.
17_b.mzn
This is a translation of Karsten Konrad's OPL model in Let’s do real CP: forbiddenAssignment, which uses a
forbiddenAssignments
constraint. However, MiniZinc don't has this constraint as a builtin so I had to roll my own, here called existential_conflict
. The forbidden
is an table of forbidden combinations in the matrix. For 4 colors it look like this:
1 1 1 1 2 2 2 2 3 3 3 3 4 4 4 4i.e. there can be no rectangle with has all the same values. (If you now start to think about
global cardinality constraint
, please read on.)
Here is the complete model:
int: NbColumns = 10; int: NbRows = 10; int: NbColors = 4; set of int: Columns = 1..NbColumns; set of int: Rows = 1..NbRows; set of int: Colors = 1..NbColors; array[Rows,Columns] of var Colors: space :: is_output; array[Colors, 1..4] of int: forbidden = array2d(Colors, 1..4,[ i  i in Colors, j in 1..4]); % The pattern x must not be in table table. predicate extensional_conflict(array[int, int] of var int: table, array[int] of var int: x) = not exists(pattern in index_set_1of2(table)) ( forall(j in index_set_2of2(table)) ( x[j] = table[pattern, j] ) ) ; solve :: int_search( [space[i,j]  i in Rows, j in Columns], first_fail, indomain_min, complete) satisfy; constraint space[1,1] = 1 /\ space[NbRows,NbColumns] = 2 /\ forall(r in Rows, r2 in 1..r1, c in Columns, c2 in 1..c1) ( extensional_conflict(forbidden, [space[r,c], space[r2,c], space[r,c2], space[r2,c2]]) )17_b2.mzn
This is almost exactly the same as the one above, except that it has another implementation of
existential_conflict
, a kind of MIP version:
predicate extensional_conflict(array[int, int] of var int: table, array[int] of var int: x) = forall(pattern in index_set_1of2(table)) ( sum(j in index_set_2of2(table)) ( bool2int(x[j] = table[pattern, j]) ) < 4 ) ;17_b3.mzn
This third version use the constraint
global cardinality constraint
instead of forbidden assignments/existential_conflict. We create a temporary array (gcc
), and then check that there is no value of 4 (i.e. the number of occurrences of each number must be less than 4). Also, I skipped the symmetry breaking of assigning the corner values in the matrix space
(commented below).
constraint forall(r in Rows, r2 in 1..r1, c in Columns, c2 in 1..c1) ( let { array[1..4] of var 0..4: gcc } in global_cardinality( [space[r,c], space[r2,c], space[r,c2], space[r2,c2]], gcc) /\ forall(i in 1..4) ( gcc[i] < 4 ) ) ;As you can see these are rather simple (a.k.a. naive) models. I suspect that there are better search strategies than the one I tested, for example Gecode's
size_afc_max
with indomain_random
which is one of the better:
solve :: int_search( [space[i,j]  i in Rows, j in Columns], size_afc_max, indomain_random, fail) satisfy;However, neither of these models could find any solution of the original 17x17x4 problem. The longest take was 36 hours on my new 8 core Linux (Ubuntu) and 12 Gb RAM, but no luck.
Here is a solution of the 17x17x5 (i.e. 5 colors), using the LazyFD solver (it took 1:19 minutes), c.f. Karsten's Improved Model for Coloring Problem.
1 5 1 5 1 5 3 2 5 5 4 4 2 3 1 3 2 5 1 4 3 5 5 2 3 2 2 3 2 4 1 4 4 4 3 2 2 2 1 3 2 4 1 3 5 3 4 4 2 5 5 2 2 3 3 5 4 4 2 5 4 4 1 3 1 1 1 5 4 4 5 3 1 4 1 1 3 5 2 2 5 3 2 5 3 5 1 3 1 1 3 3 2 2 1 4 1 5 4 2 4 5 4 2 4 3 5 3 5 1 2 4 2 5 2 4 1 2 1 2 4 2 4 1 5 4 3 4 2 5 3 4 1 5 2 3 4 3 5 2 1 3 4 3 5 2 5 5 3 3 4 1 2 1 5 3 1 2 1 4 1 3 2 3 5 2 4 2 5 4 2 1 3 5 2 1 5 3 2 3 5 4 5 2 4 1 1 5 3 5 4 3 4 3 2 1 3 3 2 1 2 1 2 4 4 3 3 4 4 1 5 5 1 5 4 1 2 2 5 3 3 5 4 4 1 3 2 1 4 2 5 4 5 3 5 3 1 3 2 4 1 3 4 2 1 5 1 3 1 4 5 5 2 4 1 3 3 5 2 4 2 5 4 3 1 1 2 1 5 3 1 4 1 5 2 3 4 2 1 5 4 4 5 1 1 2 3 3 2I also wrote a Comet model, 17_b.co, and experimented with different cardinality constraints (
cardinality
, atmost
, a decomposition of forbiddenAssignments
) and different labelings.
Ormat game
Ormat game is yet another grid problem. From bitplayer: The Ormat Game (where the nice pictures has been replace with 0/1 matrices below):Here’s the deal. I’m going to give you a square grid, with some of the cells colored and others possibly left blank. We’ll call this a template. Perhaps the grid will be one of these 3×3 templates:This is the first version in MiniZinc: ormat_game.mzn where the problem instances are included in the model file. As with the 17x17 problem above, this is  in concept, at least  quite simple. The model, sans the overlays, is shown below:1 0 0 1 1 1 1 1 1You have a supply of transparent plastic overlays that match the grid in size and shape and that also bear patterns of black dots:
0 1 1 1 1 1 1 1 1
0 1 1 1 1 1 1 1 0
(1) (2) (3)
1 0 0 1 0 0 0 1 0Note that each of these patterns has exactly three dots, with one dot in each row and each column. The six overlays shown are the only 3×3 grids that have this property.
0 1 0 0 0 1 1 0 0
0 0 1 0 1 0 0 0 1
(a) (b) (c)
0 0 1 0 1 0 0 0 1
1 0 0 0 0 1 0 1 0
0 1 0 1 0 0 1 0 0
(d) (e) (f)
Your task is to assemble a subset of the overlays and lay them on the template in such a way that dots cover all the colored squares but none of the blank squares. You are welcome to superimpose multiple dots on any colored square, but overall you want to use as few overlays as possible. To make things interesting, I’ll suggest a wager. I’ll pay you $3 for a correct covering of a 3×3 template, but you have to pay me $1 for each overlay you use. Is this a good bet?
include "globals.mzn"; % the number of overlays, n! int: f :: is_output = product([i  i in 1..n]); % Which overlay to use. array[1..f] of var 0..1: x :: is_output; % number of overlays used (to minimize) var 1..f: num_overlays :: is_output = sum(x); % There are n! possible overlays % They are in a separate .dzn file % ormat_game_n3.dzn etc array[1..f, 1..n,1..n] of 0..1: overlays; solve :: int_search( x, smallest, indomain_min, complete) minimize num_overlays; constraint % if problem has a black cell (=1) then there % must be a selected overlay that has a black cell forall(i,j in 1..n) ( ( problem[i,j] = 1 > exists(o in 1..f) ( x[o]*overlays[o,i,j] = 1 ) ) ) /\ % the inverse: wherever a selected overlay % has a black cell, problem must have % a black cell forall(o in 1..f) ( x[o] = 1 > forall(i,j in 1..n) ( overlays[o,i,j] = 1 > problem[i,j] = 1 ) ) ; % Problem grid 3 include "ormat_game_n3.dzn"; array[1..n, 1..n] of 0..1: problem = array2d(1..n, 1..n, [ 1,1,1, 1,1,1, 1,1,0 ]);The only constraints are:
 if the problem matrix has a black cell (1) then there at least one of the selected overlay matrices must have a 1 in this cell
 the converse: for all the black cells in the selected overlays the problem must has a black cell.
Problem: 111 111 110 Solution: x: [0, 1, 0, 1, 1, 1] num_overlays: 4 Overlay #2 100 001 010 Overlay #4 001 100 010 Overlay #5 010 001 100 Overlay #6 001 010 100Ideally, the overlays should be calculated in realtime, but it was much easier to generate overlay files for each size (using ormat_game_generate.mzn and some postprocessing in Perl). These must be included in the model as well. Note: there are n! overlay matrices for problems of size n x n.
 ormat_game_n3.dzn: For n = 3
 ormat_game_n4.dzn: For n = 4
 ormat_game_n5.dzn: For n = 5
 ormat_game_n6.dzn: For n = 6
 ormat_game_n7.dzn: For n = 7
 ormat_game_problem1.mzn: Problem 1 (3x3)
 ormat_game_problem2.mzn: Problem 2 (3x3)
 ormat_game_problem3.mzn: Problem 3 (3x3)
 ormat_game_problem4.mzn: Problem 4 (4x4)
 ormat_game_problem5.mzn: Problem 5 (5x5)
 ormat_game_problem6.mzn: Problem 6 (6x6)
 ormat_game_problem7.mzn: Problem 7 (7x7)
Other new models
Here are some other new models (or not mentioned earlier):Contiguity using regular
contiguity_regular.mzn: decomposition of the global constraintcontiguity
using regular
constraint.
Combinatorial auction
These two MiniZinc models implements a simple combinatorial auction problem (Wikipedia): combinatorial_auction.mzn, and a "talkative" MIP version combinatorial_auction_lp.mzn (which is translated from Numberjack's Tutorial)Compare with the Gecode version combinatorial_auction.cpp.