A first look at G12 Zinc: Basic learning models etc
There is a separate page for the new Zinc models: My Zinc page.
For about week ago the version 1.0.0 of NICTA G12 - Constraint Programming Platform was relased, which include Zinc version 1.0.0. I have looked forward to this day since I first learned (early 2008) about the G12 solvers (Zinc/MiniZinc).
In Some exiting news today I just had the time to collect some links etc. Later that day I started to learn more about Zinc, and the best way of learning a new constraint programming system is - for me at least - to implement my "learning problems" (a collection of "about 17 different models").
Here I will not go through all features of Zinc or all the differences between MiniZinc and Zinc. Both these are described in Specification of Zinc and MiniZinc (there is also a PDF version). The appendix C contains an overview of the differences.
That said, some of the most significant differences between MiniZinc and Zinc is that Zinc supports the following:
I have collected all these Zinc models in a separate page: My Zinc page.
Zinc model: least_diff.zinc
This model use a type synonym:
Zinc model: diet1.zinc
This is just about the same as the MiniZinc version.
Zinc model: send_more_money.zinc
Zinc model: send_more_money2.zinc (with enums)
This is the classic alphametic puzzle: SEND + MORE = MONEY.
The changes in the Zinc model send_more_money.zinc are about the same as in the least_diff problem mentioned above, i.e type definition of the domain. Here we use two different types: one for the range 0..9, and for the letter S and the letter M we use the range 1..9:
Also, see the general alphametic solver below.
Zinc model: seseman.zinc
This is just the same as the MiniZinc version, apart some correcting some typos.
Zinc model: coins_grid.zinc
This is a problem that the plain constraint programming solvers has some problem with, but is a cinch for MIP solvers.
Here the declaration of the variables and constraints are about the same. However, the search strategy changed so Zinc use the MIP solver which solves the problem very fast:
Zinc model: debruijn_binary.zinc
There are no big differences between the MiniZinc model and the Zinc model, just these:
Zinc model: alldifferent_except_0.zinc
This Zinc version don't have any built-in support for the constraint
Zinc model: furniture_moving.zinc
Zinc model: furniture_moving2.zinc, defining the tasks as
The Zinc version use an
Originally, I planned to use these Tasks as indices of the arrays (e.g.
A variant, furniture_moving2.zinc, use a record for defining the tasks. Note that the constraint which calculates
Printing the
A drawback with this method is that if
The (slightly modified) version furniture_moving2b.zinc and furniture_moving2b-zinc.dzn examplifies this:
Zinc model: minesweeper.zinc
Zinc model: minesweeper_model.zinc (general model)
There are no changes in the Zinc model.
Problem instances. They include minesweeper_model.zinc
Zinc model: quasigroup_completion.zinc
Zinc model: quasigroup_completion_model.zinc (general model)
Changes:
Zinc model: survo_puzzle.zinc
The Zinc model is almost the same, except that the output use
Zinc model: young_tableaux.zinc
Slightly better output which is not really Zinc specific.
Zinc model: send_more_money_any_base.zinc
Changes:
Zinc model: map.zinc
Changes:
Here is the complete model:
Zinc model: nonogram_create_automaton2.zinc
Data file: nonogram_p200-zinc.dzn
Note: This is the only model where I got serious problems when translating to Zinc or running a MiniZinc model with Zinc. It triggered a translation bug in the Zinc compiler mentioned in the Mantis tracker here.
Zinc model: xkcd.zinc
Changes:1, 2, 3, .. as we are used to in MiniZinc. As a consequence of this, the prices must use these indices as well:
Zinc model: crossword2.zinc
The Zinc model use enum for the letters, which is used to get a better output:
Zinc model: word_square.zinc
Just as with the crosswords2.zinc this use enum for the letters which makes the model and output neater than the MiniZinc model.
However it is very slow. Even for the trivial 2x2 problem, the Zinc model took 1 min 30 seconds (with solve satisfy). I have not found any faster labeling...
Zinc model: who_killed_agatha.zinc
The only change compared to the MiniZinc model is that the persons is defined as an enum (not int:s).
Zinc model: conference.base.zinc
The Zinc model itself is about the same as the MiniZinc model except for two things: First the output is sligtly more elaborate. Second, I experiment with different backends for solving the problem by using separate configurations files:
Zinc model: labeled_dice.zinc
Zinc model: labeled_dice2.zinc (general method)
Zinc model: coloring_blocks.model.zinc (more general model)
The Zinc model use enums instead of explicit assign each letter to an int.
labeled_dice2.zinc is a more general version which use the same tuple and lookup method as in alphametic.zinc (see above).
coloring_blocks_building_blocks.zinc is an even more general solution which solves both labeled_dice problem and the similar building_blocks (see the MiniZinc model building_blocks.mzn)
Note: There is one additional quirk in this general model which I didn't notice before when there was two separate MiniZinc models. There are not 24 distinct letters in the building blocks problem, just 23 (the letter "F" is not in any of the listed word). So I had to add a special variable
Problem instances:
This is a general alphametic solver, i.e. solves puzzles such as
The words must be stated letter for letter since Zinc has not support for accessing the characters in a string.
This is a new MiniZinc/Zinc model for calculating Dudeney Numbers:
Running this model with Zinc and generate all the solutions:
For about week ago the version 1.0.0 of NICTA G12 - Constraint Programming Platform was relased, which include Zinc version 1.0.0. I have looked forward to this day since I first learned (early 2008) about the G12 solvers (Zinc/MiniZinc).
In Some exiting news today I just had the time to collect some links etc. Later that day I started to learn more about Zinc, and the best way of learning a new constraint programming system is - for me at least - to implement my "learning problems" (a collection of "about 17 different models").
Here I will not go through all features of Zinc or all the differences between MiniZinc and Zinc. Both these are described in Specification of Zinc and MiniZinc (there is also a PDF version). The appendix C contains an overview of the differences.
That said, some of the most significant differences between MiniZinc and Zinc is that Zinc supports the following:
- functions
- tuples
- records
- enums
- type synonyms (including constraints). See furniture_moving2.zinc for an example of types with constraints
- type-inst variables ($T) for creating polymorphic functions/predicates.
- sets can contain arbitrary objects
- arrays can be indexed with enums etc
- implicit type conversion, e.g. int-to-float, set-to-array
- compiling the model+data to an executable program
- Different support for solvers and annotations. (I have not fully looked into this.)
- The following built-in functions: powerset, cartesian_product, concat, head, last, tail, condense, condense_int_index, show_float, first, second, fst, snd, foldl, foldr
- the compilation to executable file is not blazingly fast. For most Zinc models compilation took about 6-10 seconds (on my 64-bit Linux Ubuntu 10.4 with 8 cores and 12Gb RAM).
- running the model can be slower since there is much more happening in a Zinc program.
- for some Zinc models (with some problem instances), the memory usage can be very high (compared to the MiniZinc variant) and in some rare cases I had to stop the execution since it claimed all the RAM. This happened in the Zinc version of the 17x17 problem (for sizes 15x15x4).
- unsurprisingly, there are bugs (some are mentioned below)
- the support for data files (.dzn files) is more restricted than in MiniZinc, and one may hav to either change the data file, or compile it in the Zinc program. For an example of this, see Survo puzzle below. However, I'm not sure if this restrictedness is going to be lifted in later version.
$ zinc minizinc_model.mzn $ ./minizinc_modelWell, at least if the model is runnable by the tools from G12 MiniZinc distribution. Added functionality, such as definitions added by an "external" solver, e.g. Gecode, JaCoP, SICStus Prolog, ECLiPSe, SMT, etc may not work (or at least I have not get these to work). Also, I have not checked that all my MiniZinc models can be compiled and run with Zinc.
Functions and foldr
Besides predicates, Zinc has support for functions which is real nice. Some examples are shown in the models, e.g. in the General alphametic solver (see below). Here are some other examples:
function var int: mysum(array[$T] of var int: a) = foldr('+', 0, a);
function var int: scalar_product(array[$T] of var int: a, array[$T] of var int: b) =
sum(i in index_set(a)) ( a[i]*b[i] );
function var int: myplus(var int: a, var int: b) = a + b;
function var int: mysum2(array[int] of var int: a) = foldr(myplus, 0, a);
It may be interesting to know that the two standard accumulators forall and exists are predicates defined with foldr (in the file g12-1.0.0/lib/zinc/stdlib.zinc):
predicate forall(array[$T] of var bool: xs) = foldr('/\', true, xs);
predicate exists(array[$T] of var bool: xs) = foldr('\/', false, xs);
The Zinc models
Here are my Zinc models so far. Apart from the Nonogram model (that triggered some bugs), all "about 17 learning models" has been translated to Zinc. Some of these has very little changes compared to the MiniZinc model and could be compiled as a MiniZinc (.mzn) model. However I wanted to list them all here with the .zinc suffix.I have collected all these Zinc models in a separate page: My Zinc page.
Least difference
MiniZinc model: least_diff.mznZinc model: least_diff.zinc
This model use a type synonym:
type digits = var 0..9;Instead of the traditional (MiniZinc) way of declaring decision variables:
set of 0..9: digits = 0..9; var digits: A; var digits: B; % ...we now can write:
type digits = var 0..9; digits: A; digits: B; % ...Another usage of type declarations is to add a constraint of the variable directly. Instead of first declaring a decision variable and add the constraint that it is
>=0 in a constraint
section we can combine this in Zinc:
% define a constrained type definition for positive numbers type varintp = (var int: i where i >= 0); varintp: X;This model also use a Zinc specific search annotation:
solve :: backend_fdic(g12_fd, none, none) minimize difference;Note: Zinc also support the MiniZinc annotation form (and converts it to the Zinc way):
solve :: int_search(FD, first_fail, indomain, complete) minimize difference;Note: Since the MiniZinc language is a subset of the Zinc languages, the Zinc solver can run any MiniZinc model.
Simple diet problem
MiniZinc model: diet1.mznZinc model: diet1.zinc
This is just about the same as the MiniZinc version.
SEND + MORE = MONEY
MiniZinc model: send_more_money.mznZinc model: send_more_money.zinc
Zinc model: send_more_money2.zinc (with enums)
This is the classic alphametic puzzle: SEND + MORE = MONEY.
The changes in the Zinc model send_more_money.zinc are about the same as in the least_diff problem mentioned above, i.e type definition of the domain. Here we use two different types: one for the range 0..9, and for the letter S and the letter M we use the range 1..9:
type digits0_9 = var 0..9;
type digits1_9 = var 1..9;
digits1_9: S; % S > 0
digits0_9: E;
digits0_9: N;
digits0_9: D;
digits1_9: M; % M > 0
digits0_9: O;
digits0_9: R;
digits0_9: Y;
constraint
all_different(fd) /\
1000*S + 100*E + 10*N + D +
1000*M + 100*O + 10*R + E =
10000*M + 1000*O + 100*N + 10*E + Y
% /\ S > 0 % not needed
% /\ M > 0 % not needed
;
The variant send_more_money2.zinc, use another new feature in Zinc: enum digits for declaring the names of the variables, and also use an array of decision variables (of range 0..9) with the enum digits as indices.
enum digits = {S,E,N,D,M,O,R,Y};
array[digits] of var 0..9: x;
constraint
alldifferent(x) /\
1000*x[S] + 100*x[E] + 10*x[N] + x[D] +
1000*x[M] + 100*x[O] + 10*x[R] + x[E] =
10000*x[M] + 1000*x[O] + 100*x[N] + 10*x[E] + x[Y]
/\
x[S] > 0 /\ x[M] > 0
It may be a matter of taste which version one would use for these small (toy) problem.
I tend to prefer the first version (where the decision variables are used directly),
but for larger problems the second version is probably better.
Also, see the general alphametic solver below.
Seseman Convent problem
MiniZinc model: seseman.mznZinc model: seseman.zinc
This is just the same as the MiniZinc version, apart some correcting some typos.
Coins Grid (Hurlimann)
MiniZinc model: coins_grid.mznZinc model: coins_grid.zinc
This is a problem that the plain constraint programming solvers has some problem with, but is a cinch for MIP solvers.
Here the declaration of the variables and constraints are about the same. However, the search strategy changed so Zinc use the MIP solver which solves the problem very fast:
solve :: backend_mip(osi_cbc) minimize z;Using the fdic (finite domain solver) is much slower:
solve :: backend_fdic(g12_fd, g12_ic, osi_cbc) minimize z;However, with the above solve annotation (fdic), there is another way of using the MIP solver: as an option when compiling the model:
$ zinc -b mip coins_grid.zincI have not yet fully tested all the features of the new search annotations. It is explained in the Zinc Manual (as PDF).
de Bruijn sequence
MiniZinc model: debruijn_binary.mznZinc model: debruijn_binary.zinc
There are no big differences between the MiniZinc model and the Zinc model, just these:
- it use data files for the problem instances
-
pow(base, n)is used instead converting forth and back to floats. There have been some problems with integer version ofpowin earlier MiniZinc version, but it has been fixed now. - skipped the gcc-part
alldifferent_except_0
MiniZinc model: alldifferent_except_0.mznZinc model: alldifferent_except_0.zinc
This Zinc version don't have any built-in support for the constraint
increasing, which is just used as symmetry breaking the the example. However - since MiniZinc is a subset of Zinc - the MiniZinc version in increasing.mzn can be used instead:
include "increasing.mzn";
Furniture moving (scheduling)
MiniZinc model: furniture_moving.mznZinc model: furniture_moving.zinc
Zinc model: furniture_moving2.zinc, defining the tasks as
recordThe Zinc version use an
enum for defining the tasks:
% declaration
enum Task;
% ....
%
% data instance:
enum Tasks = {piano, chair, bed, table};
(I was somewhat surprised that enum is also needed when stating the data instances.)
Originally, I planned to use these Tasks as indices of the arrays (e.g.
array[Tasks] of var 0..upperLimit: Starts) but this don't work in Zinc version 1.0.0 due to a bug (which will be hopefully be fixed in the next release).
A variant, furniture_moving2.zinc, use a record for defining the tasks. Note that the constraint which calculates
t.end from t.start = t.duration.
type Task = (record(string: desc,
var 0..upper_limit: start,
int: duration,
int: resource,
var 0..upper_limit*2: end):
t where t.end = t.start + t.duration);
And then tasks is defined as
tasks = [
("piano", _, 30, 3, _) ,
("chair", _, 10, 1, _),
("bed" , _, 15, 3, _),
("table", _, 15, 2, _)
];
Here we use the anonym value (_) for the decision variables.
Printing the
tasks array, we now can see all
fields in the record, including the decision variables (start and end):
(desc:"piano", start:30, duration:30, resource:3, end:60) (desc:"chair", start:0, duration:10, resource:1, end:10) (desc:"bed", start:15, duration:15, resource:3, end:30) (desc:"table", start:0, duration:15, resource:2, end:15)This is much clearer comparing to the traditional output of just the contents of the decision variables arrays.
A drawback with this method is that if
tasks is put in a separate data file, this data file must be compiled with the model.
The (slightly modified) version furniture_moving2b.zinc and furniture_moving2b-zinc.dzn examplifies this:
$ zinc furniture_moving2b.zinc furniture_moving2b-zinc.dzn $ ./furniture_moving2b
Minesweeper
MiniZinc model: minesweeper.mznZinc model: minesweeper.zinc
Zinc model: minesweeper_model.zinc (general model)
There are no changes in the Zinc model.
Problem instances. They include minesweeper_model.zinc
- minesweeper_0.zinc
- minesweeper_1.zinc
- minesweeper_2.zinc
- minesweeper_3.zinc
- minesweeper_4.zinc
- minesweeper_5.zinc
- minesweeper_6.zinc
- minesweeper_7.zinc
- minesweeper_8.zinc
- minesweeper_9.zinc
- minesweeper_basic3.zinc
- minesweeper_basic4x4.zinc
- minesweeper_basic4.zinc
- minesweeper_config_page2.zinc
- minesweeper_config_page3.zinc
- minesweeper_german_Lakshtanov.zinc
- minesweeper_splitter.zinc
- minesweeper_wire.zinc
Quasigroup completion
MiniZinc model: quasigroup_completion.mznZinc model: quasigroup_completion.zinc
Zinc model: quasigroup_completion_model.zinc (general model)
Changes:
- using
show_array2d(). - In Zinc the global constraint alldifferent is spelled
alldifferent. In MiniZinc there is an alias to the predicate nameall_different
- quasigroup_completion_gomes_demo1.zinc
- quasigroup_completion_gomes_demo2.zinc
- quasigroup_completion_gomes_demo3.zinc
- quasigroup_completion_gomes_demo4.zinc
- quasigroup_completion_gomes_demo5.zinc
- quasigroup_completion_gomes_shmoys_p3.zinc
- quasigroup_completion_gomes_shmoys_p7.zinc
- quasigroup_completion_martin_lynce.zinc
Survo puzzle
MiniZinc model: survo_puzzle.mznZinc model: survo_puzzle.zinc
The Zinc model is almost the same, except that the output use
output [ show_array2d(x) ];instead of the traditional
output [
if j = 1 then "\n" else " " endif ++
show(x[i,j])
| i in 1..r, j in 1..c
] ++ ["\n"];
Zinc is more restricted with regards to the datafile that is to be included via command line, such as:
$ zinc survo_puzzle.zinc $ ./survo_puzzle survo_puzzle1.dznThe following don't work (in the current version 1.0.0 at least):
r = 3;
c = 4;
matrix = array2d(1..r, 1..c,
[
0, 6, 0, 0,
8, 0, 0, 0,
0, 0, 3, 0
]);
Instead, one has to explicitly state the dimension of the matrix:
r = 3;
c = 4;
matrix = array2d(1..3, 1..4,
[
0, 6, 0, 0,
8, 0, 0, 0,
0, 0, 3, 0
]);
However, if the data file is included in compile time, the variables
r and c can be used to state the dimensions.
$ zinc survo_puzzle.zinc survo_puzzle1.dznData files:
- survo_puzzle1.dzn
- survo_puzzle2.dzn
- survo_puzzle3.dzn
- survo_puzzle4.dzn
- survo_puzzle5.dzn
- survo_puzzle6.dzn
Young Tableaux
MiniZinc model: young_tableaux.mznZinc model: young_tableaux.zinc
Slightly better output which is not really Zinc specific.
SEND + MORE = MONEY in any base
MiniZinc model: send_more_money_any_base.mznZinc model: send_more_money_any_base.zinc
Changes:
-
type digits = var 0..base-1; - using
pow(base,n)instead ofbase*base*base(for n=2..4)
Simple map coloring
MiniZinc model: map.mznZinc model: map.zinc
Changes:
- using enum and tuple
- using data files with tuples of neighbours
enum country = {belgium, denmark, france, germany, netherlands, luxembourg};
neighbors = {
(france, belgium),
(france, luxembourg),
(france, germany),
(luxembourg, germany),
(luxembourg, belgium),
(netherlands, belgium),
(germany, belgium),
(germany, netherlands),
(germany, denmark)
};
The constraint of stating that two neighbours must have different colors use the
special notation for tuples: nn.1 for the first element in the tuple,
and nn.2 for the second element.
Here is the complete model:
int: num_colors;
enum country;
set of tuple(country, country): neighbors;
array[country] of var 1..num_colors: colors;
constraint
forall(nn in neighbors) (
colors[nn.1] != colors[nn.2]
)
/\ % symmetry breaking
colors[country[1]] = 1
;
solve satisfy;
output [
show(colors) ++ "\n"
];
Data files:
Nonogram
MiniZinc model: nonogram_create_automaton2.mznZinc model: nonogram_create_automaton2.zinc
Data file: nonogram_p200-zinc.dzn
Note: This is the only model where I got serious problems when translating to Zinc or running a MiniZinc model with Zinc. It triggered a translation bug in the Zinc compiler mentioned in the Mantis tracker here.
xkcd knapsack problem
MiniZinc model: xkcd.mznZinc model: xkcd.zinc
Changes:
- enum as indices and presentation
- using
show_floatto show the real prices with 2 decimals
enum products = {mixed_fruit, french_fries, side_salad, host_wings, mozzarella_sticks, samples_place};
This means that the indices of the products are mixed_fruit, french_fries, ..., not
price = [mixed_fruit:215, french_fries:275, side_salad:335,
host_wings:355, mozzarella_sticks:420, samples_place:580];
(It is a type error if one try to define the price array as [215, 275, 335, 355, 420, 580].)
There are two solutions to the problem.
[ mixed_fruit:1, french_fries:0, side_salad:0, host_wings:2, mozzarella_sticks:0, samples_place:1 ] 1 of mixed_fruit price: 2.15 (= 2.15) 2 of host_wings price: 3.55 (= 7.10) 1 of samples_place price: 5.80 (= 5.80) -- [ mixed_fruit:7, french_fries:0, side_salad:0, host_wings:0, mozzarella_sticks:0, samples_place:0 ] 7 of mixed_fruit price: 2.15 (= 15.05)
Simple crossword problem
MiniZinc model: crossword2.mznZinc model: crossword2.zinc
The Zinc model use enum for the letters, which is used to get a better output:
E1: 1 = hoses
E2: 3 = sails
E3: 5 = steer
E4: 7 = hike
E5: 8 = keel
E6: 12 = ale
E7: 14 = lee
E8: 2 = laser
Word square
MiniZinc model: word_square.mznZinc model: word_square.zinc
Just as with the crosswords2.zinc this use enum for the letters which makes the model and output neater than the MiniZinc model.
However it is very slow. Even for the trivial 2x2 problem, the Zinc model took 1 min 30 seconds (with solve satisfy). I have not found any faster labeling...
Who killed Agatha
MiniZinc model: who_killed_agatha.mznZinc model: who_killed_agatha.zinc
The only change compared to the MiniZinc model is that the persons is defined as an enum (not int:s).
Conference scheduling
MiniZinc model: conference.mznZinc model: conference.base.zinc
The Zinc model itself is about the same as the MiniZinc model except for two things: First the output is sligtly more elaborate. Second, I experiment with different backends for solving the problem by using separate configurations files:
- conference.fd.zinc
This use thefdsolver:include "conference.base.zinc"; backend = backend_fdic(default, default, default); search = tree_search(sessions, in_order, min_assign);
- conference.fdx.zinc
Thefdxis the Lazy solver:include "conference.base.zinc"; backend = backend_fdic(g12_fdx, default, default); search = tree_search(sessions, in_order, min_assign);
- conference.mip.zinc
MIP solverinclude "conference.base.zinc"; backend = backend_mip(default); % search = null; % search = tree_search(sessions, in_order, min_assign); search = tree_search(sessions, min_domsize, min_assign);
Labeled dice, Building blocks
MiniZinc model: labeled_dice.mznZinc model: labeled_dice.zinc
Zinc model: labeled_dice2.zinc (general method)
Zinc model: coloring_blocks.model.zinc (more general model)
The Zinc model use enums instead of explicit assign each letter to an int.
labeled_dice2.zinc is a more general version which use the same tuple and lookup method as in alphametic.zinc (see above).
coloring_blocks_building_blocks.zinc is an even more general solution which solves both labeled_dice problem and the similar building_blocks (see the MiniZinc model building_blocks.mzn)
Note: There is one additional quirk in this general model which I didn't notice before when there was two separate MiniZinc models. There are not 24 distinct letters in the building blocks problem, just 23 (the letter "F" is not in any of the listed word). So I had to add a special variable
additional which contains "F" and is
union:ed which letter for this problem instance. And I'm not very
happy about this solution. (I tried to to do a union with all the letters from "a" to "z" but this didn't work.)
Problem instances:
New Zinc models
I have also done some new models (i.e. not just translated MiniZinc models).alphametic.zinc A general alphametic solver
Zinc model: alphametic.zincThis is a general alphametic solver, i.e. solves puzzles such as
SEND + MORE = MONEY, SEND+MOST = MONEY.
This may have been possible to do in MiniZinc but using Zinc's tuple as a lookup table makes it quite easy.
The words must be stated letter for letter since Zinc has not support for accessing the characters in a string.
base = 10; num_words = 3; num_letters = 5; words = array2d(1..3, 1..5, [ "", "s","e","n","d", % + "", "m","o","r","e", % = "m","o","n","e","y"]);Here are some of features of this model:
- The distinct letters used in the problem are put into a set (code>letters which is used to create the lookup table
letters2using a tuple (string, int):set of string: letters = {""} union {words[i,j] | i in 1..num_words, j in 1..num_letters}; array[1..card(letters)] of tuple(string, int): letters2 = [(letters[i],i) | i in 1..card(letters)];We have to do a union with the set of the character {""} (empty string) since all strings must be of the same length in the problem matrix (words). - Notice how it calculates the first letter in each word (which must be > 0):
set of string: non_zeros = { words[i, min([j | j in 1..num_letters where words[i,j] != ""])] | i in 1..num_words }; - using the operation
string_intersperse(cf. join("", array) in other programming languages) - The function
lookup/2is a mapping between a letter and its index in the array of decision variablesx:function int: lookup($T: c, % the key (here a character) array[int] of tuple($T, int): h) = % take the first (and only) value in the list head([k.2 | k in h where k.1 = c]) ;Here is an example how it is used for stating that some of the letters must be > 0.% ... constraint % .... forall(z in non_zeros) ( x[lookup(z,letters2)] > 0 )
- alphametic_send_most_money.dzn
- alphametic_send_more_money.dzn
- alphametic_vingt_cinq_cinq_trente.dzn
- alphametic_ein_ein_ein_ein_vier.dzn
- alphametic_donald_gerald_robert.dzn
- alphametic_saturn_uranus_neptune_pluto_planets.dzn
- alphametic_wrong_wrong_right.dzn
Dudeney numbers
MiniZinc/Zinc model: dudeney_numbers.mznThis is a new MiniZinc/Zinc model for calculating Dudeney Numbers:
A Dudeney number is a positive integer that is a perfect cube such that the sum of its decimal digits is equal to the cube root of the number. There are exactly six such integers.Pierre Schaus wrote about this problem some days ago in Dudeney number, and showed an or-tools (Operations Research Tools developed at Google, a.k.a. Google CP Solver) model for solving this using Python. (Note: I will check out the Google CP Solver more later.)
Running this model with Zinc and generate all the solutions:
$ zinc dudeney_numbers.mzn $ dudeney_numbers -s allgives the following output. Note that the indices are here explicitly stated in the array
x.
s: 1 nb: 1 x: [ 1:0, 2:0, 3:0, 4:0, 5:0, 6:1 ] -- s: 17 nb: 4913 x: [ 1:0, 2:0, 3:4, 4:9, 5:1, 6:3 ] -- s: 18 nb: 5832 x: [ 1:0, 2:0, 3:5, 4:8, 5:3, 6:2 ] -- s: 26 nb: 17576 x: [ 1:0, 2:1, 3:7, 4:5, 5:7, 6:6 ] -- s: 27 nb: 19683 x: [ 1:0, 2:1, 3:9, 4:6, 5:8, 6:3 ] -- s: 8 nb: 512 x: [ 1:0, 2:0, 3:0, 4:5, 5:1, 6:2 ]Note: In the current Zinc version there are only two options for the number of solutions:
first or all. I hope that there soon will be options for a given number of solutions, at least two solutions since it can be interesting to know if a solution is unique or not.
More info about G12 system/Zinc
Here are some information about G12 and Zinc:- Nicta G12 Project
- Downloads
- Zinc
- Documents
- IDE
- Run Zinc
- Run MiniZinc
- MiniZinc. For more info about MiniZinc: see MiniZinc and FlatZinc and MiniZinc Wiki, and - of course - my MiniZinc page.