GAGA
A MiniZinc Tutorial
Kim Marriott and Peter J. Stuckey
with contributions from Leslie De Koninck and Horst Samulowitz
Contents
1 Introduction 2
2 Basic Modelling in MiniZinc 2
2.1 Our First Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
2.2 An Arithmetic Optimisation Example . . . . . . . . . . . . . . . . . . . . . . . . . . 5
2.3 Datafiles and Assertions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2.4 Real Number Solving . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
2.5 Basic structure of a model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
3 More Complex Models 14
3.1 Arrays and Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
3.2 Global Constraints . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
3.3 Conditional Expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
3.4 Complex Constraints . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
1
3.5 Set Constraints . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
3.6 Enumerated Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
4 Predicates 38
4.1 Global Constraints . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
4.1.1 Alldifferent . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
4.1.2 Cumulative . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
4.1.3 Table . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
4.1.4 Regular . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
4.2 Defining Predicates . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
4.3 Reflection Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
4.4 Local Variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
4.5 Domain Reflection Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
4.6 Scope . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
5 Search 51
5.1 Finite Domain Search . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
5.2 Search Annotations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
5.3 Annotations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
6 Effective Modelling Practices in MiniZinc 58
6.1 Variable Bounds . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
6.2 Unconstrained Variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60
6.3 Effective Generators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
6.4 Redundant Constraints . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
6.5 Modelling Choices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
6.6 Multiple Modelling and Channels . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
7 Boolean Satisfiability Modelling in MiniZinc 67
7.1 Modelling Integers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
7.2 Modelling Disequality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
7.3 Modelling Cardinality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69
A MiniZinc Keywords 77
B MiniZinc Operators 77
C MiniZinc Functions 77
2
1 Introduction
MiniZinc is a language designed for specifying constrained optimization and decision prob-
lems over integers and real numbers. A MiniZinc model does not dictate how to solve the
problem although the model can contain annotations which are used to guide the underlying
solver.
MiniZinc is designed to interface easily to different backend solvers. It does this by trans-
forming an input MiniZinc model and data file into a FlatZinc model. FlatZinc models consist
of variable declaration and constraint definitions as well as a definition of the objective func-
tion if the problem is an optimization problem. The translation from MiniZinc to FlatZinc
is specializable to individual backend solvers, so they can control what form constraints end
up in. In particular, MiniZinc allows the specification of global constraints by decomposition.
2 Basic Modelling in MiniZinc
In this section we introduce the basic structure of a MiniZinc model using two simple exam-
ples.
2.1 Our First Example
Figure 1: Australian states.
As our first example, imagine that we wish to colour a map of Australia as shown in
Figure 1. It is made up of seven different states and territories each of which must be given
a colour so that adjacent regions have different colours.
We can model this problem very easily in MiniZinc. The model is shown in Figure 2. The
first line in the model is a comment. A comment starts with a ‘%’ which indicates that the
rest of the line is a comment. MiniZinc has no begin/end comment symbols (such as C’s /*
and */ comments).
The next part of the model declares the variables in the model. The line
3
AUST ≡ [DOWNLOAD]
% Colouring Australia using nc colours
int: nc = 3;
var 1..nc: wa; var 1..nc: nt; var 1..nc: sa; var 1..nc: q;
var 1..nc: nsw; var 1..nc: v; var 1..nc: t;
constraint wa != nt;
constraint wa != sa;
constraint nt != sa;
constraint nt != q;
constraint sa != q;
constraint sa != nsw;
constraint sa != v;
constraint q != nsw;
constraint nsw != v;
solve satisfy;
output [“wa=”, show(wa), “\t nt=”, show(nt),
“\t sa=”, show(sa), “\n”, “q=”, show(q),
“\t nsw=”, show(nsw), “\t v=”, show(v), “\n”,
“t=”, show(t), “\n”];
Figure 2: A MiniZinc model aust.mzn for colouring the states and territories in Australia.
int: nc = 3;
specifies a parameter in the problem which is the number of colours to be used. Parameters
are similar to variables in most programming languages. They must be declared and given a
type. In this case the type is int. They are given a value by an assignment. MiniZinc allows
the assignment to be included as part of the declaration (as in the line above) or to be a
separate assignment statement. Thus the following is equivalent to the single line above
int: nc;
nc = 3;
Unlike variables in many programming languages a parameter can only be given a single
value. It is an error for a parameter to occur in more than one assignment.
The basic parameter types are integers (int), floating point numbers (float), Booleans
(bool) and strings (string). Arrays and sets are also supported.
MiniZinc models can also contain another kind of variable called a decision variable.
Decision variables are variables in the sense of mathematical or logical variables. Unlike
parameters and variables in a standard programming language, the modeller does not need
4
http://www.minizinc.org/downloads/tutorial-examples-latest/aust.mzn
to give them a value. Rather the value of a decision variable is unknown and it is only when
the MiniZinc model is executed that the solving system determines if the decision variable
can be assigned a value that satisfies the constraints in the model and if so what this is.
In our example model we associate a decision variable with each region, wa, nt, sa, q,
nsw, v and t, which stands for the (unknown) colour to be used to fill the region.
For each decision variable we need to give the set of possible values the variable can take.
This is called the variable’s domain. This can be given as part of the variable declaration and
the type of the decision variable is inferred from the type of the values in the domain.
In MiniZinc decision variables can be Booleans, integers, floating point numbers, or sets.
Also supported are arrays whose elements are decision variables. In our MiniZinc model we
use integers to model the different colours. Thus each of our decision variables is declared to
have the domain 1..nc which is an integer range expression indicating the set {1, 2, …, nc}
using the var declaration. The type of the values is integer so all of the variables in the
model are integer decision variables.
Identifiers
Identifiers which are used to name parameters and variables are sequences of lower and
uppercase alphabetic characters, digits and the underscore ‘_’ character. They must start
with a alphabetic character. Thus myName_2 is a valid identifier. MiniZinc (and Zinc)
keywords are not allowed to be used as identifier names, they are listed in Appendix A
Neither are MiniZinc operators allowed to be used as identifier names; they are listed in
Appendix B.
MiniZinc carefully distinguishes between the two kinds of model variables: parameters
and decision variables. The kinds of expressions that can be constructed using decision
variables are more restricted than those that can be built from parameters. However, in any
place that a decision variable can be used, so can a parameter of the same type.
Formally the distinction between parameters and decision variables is called the instanti-
ation of the variable. The combination of variable instantiation and type is called a type-inst.
As you start to use MiniZinc you will undoubtedly see examples of type-inst errors.
The next component of the model are the constraints. These specify the Boolean expres-
sions that the decision variables must satisfy to be a valid solution to the model. In this case
we have a number of not equal constraints between the decision variables enforcing that if
two states are adjacent then they must have different colours.
Relational Operators
MiniZinc provides the relational operators: equal (= or ==), not equal (!=), strictly less
than (< strictly greater than (>, less than or equal to (<=), and greater than or equal to (>=).
The next line in the model:
solve satisfy;
5
Indicates the kind of problem it is. In this case it is a satisfaction problem: we wish to find a
value for the decision variables that satisfies the constraints but we do not care which one.
The final part of the model is the output statement. This tells MiniZinc what to print
when the model has been run and a solution is found.
Output
An output statement is followed by a list of strings. These are typically either string
literals which are written between double quotes and use a C like notation for special
characters, or an expression of the form show(X) where X is the name of a decision
variable or parameter. In the example \n represents the newline character and \t a tab.
There are also formatted varieties of show for numbers: show_int(n,X) outputs the value
of integer X in at least |n| characters, right justified if n> 0 and left justified otherwise;
show_float(n,d,X) outputs the value of float X in at least |n| characters, right justified if
n> 0 and left justified otherwise, with d characters after the decimal point.
String literals must fit on a single line. Longer string literals can be split across multiple
lines using the string concatenation operator ++ For example, the string literal “Invalid
datafile: Amount of flour is non-negative” is equivalent to the string literal
expression “Invalid datafile: ” ++
“Amount of flour is non-negative”.
A model can contain at most one output statement.
With the G12 implementation of MiniZinc we can evaluate our model by typing
$ mzn-g12fd aust.mzn
where aust.mzn is the name of the file containing our MiniZinc model. We must use the
file extension “.mzn” to indicate a MiniZinc model. The command mzn-g12fd uses the G12
finite domain solver to evaluate our model.
When we run this we obtain the result:
wa=1 nt=3 sa=2
q=1 nsw=3 v=1
t=1
———-
The line of 10 dashes ———- is output automatically added by the MiniZinc output to
indicate a solution has been found.
2.2 An Arithmetic Optimisation Example
Our second example is motivated by the need to bake some cakes for a fete at our local
school. We know how to make two sorts of cakes.1 A banana cake which takes 250g of
1WARNING: please don’t use these recipes at home
6
CAKES ≡ [DOWNLOAD]
% Baking cakes for the school fete
var 0..100: b; % no. of banana cakes
var 0..100: c; % no. of chocolate cakes
% flour
constraint 250*b + 200*c <= 4000; % bananas constraint 2*b <= 6; % sugar constraint 75*b + 150*c <= 2000; % butter constraint 100*b + 150*c <= 500; % cocoa constraint 75*c <= 500; % maximize our profit solve maximize 400*b + 450*c; output ["no. of banana cakes = ", show(b), "\n", "no. of chocolate cakes = ", show(c), "\n"]; Figure 3: Model for determining how many banana and chocolate cakes to bake for the school fete. self-raising flour, 2 mashed bananas, 75g sugar and 100g of butter, and a chocolate cake which takes 200g of self-raising flour, 75g of cocoa, 150g sugar and 150g of butter. We can sell a chocolate cake for $4.50 and a banana cake for $4.00. And we have 4kg self-raising flour, 6 bananas, 2kg of sugar, 500g of butter and 500g of cocoa. The question is how many of each sort of cake should we bake for the fete to maximise the profit. A possible MiniZinc model is shown in Figure 3. The first new feature is the use of arithmetic expressions. 7 http://www.minizinc.org/downloads/tutorial-examples-latest/cakes.mzn Integer arithmetic Operators MiniZinc provides the standard integer arithmetic operators. Addition (+), subtrac- tion (-), multiplication (*), integer division (div) and integer modulus (mod). It also provides + and - as unary operators. Integer modulus is defined to give a result (a mod b) that has the same sign as the dividend a. Integer division is defined so that a= b*(a div b) + (a mod b). MiniZinc provides standard integer functions for absolute value (abs) and power func- tion (pow). For example abs(-4) and pow(2,5) evaluate to 4 and 32 respectively. The syntax for arithmetic literals is reasonably standard. Integer literals can be decimal, hexadecimal or octal. For instance 0, 005, 123, 0x1b7, 0o777. The second new feature shown in the example is optimisation. The line solve maximize 400 * b + 450 * c; specifies that we want to find a solution that maximises the expression in the solve statement called the objective. The objective can be any kind of arithmetic expression. One can replace the key word maximize by minimize to specify a minimisation problem. When we run this we obtain the result: no. of banana cakes = 2 no. of chocolate cakes = 2 ---------- ========== The line ========== is output automatically for optimisation problems when the system has proved that a solution is optimal. 2.3 Datafiles and Assertions A drawback of this model is that if we wish to solve a similar problem the next time we need to bake cakes for the school (which is often) we need to modify the constraints in the model to reflect the ingredients that we have in the pantry. If we want to reuse the model then we would be better off to make the amount of each ingredient a parameter of the model and then set their values at the top of the model. Even better would be to set the value of these parameters in a separate data file. MiniZ- inc (like most other modelling languages) allows the use of data files to set the value of parameters declared in the original model. This allows the same model to be easily used with different data by running it with different data files. Data files must have the file extension “.dzn” to indicate a MiniZinc data file and a model can be run with any number of data files (though a variable/parameter can only be assigned a value in one file. Our new model is shown in Figure 4. We can run it using the command $ mzn-g12fd cakes2.mzn pantry.dzn 8 CAKES2 ≡ [DOWNLOAD] % Baking cakes for the school fete (with data file) int: flour; %no. grams of flour available int: banana; %no. of bananas available int: sugar; %no. grams of sugar available int: butter; %no. grams of butter available int: cocoa; %no. grams of cocoa available constraint assert(flour >= 0,”Invalid datafile: ” ++
“Amount of flour is non-negative”);
constraint assert(banana >= 0,”Invalid datafile: ” ++
“Amount of banana is non-negative”);
constraint assert(sugar >= 0,”Invalid datafile: ” ++
“Amount of sugar is non-negative”);
constraint assert(butter >= 0,”Invalid datafile: ” ++
“Amount of butter is non-negative”);
constraint assert(cocoa >= 0,”Invalid datafile: ” ++
“Amount of cocoa is non-negative”);
var 0..100: b; % no. of banana cakes
var 0..100: c; % no. of chocolate cakes
% flour
constraint 250*b + 200*c <= flour; % bananas constraint 2*b <= banana; % sugar constraint 75*b + 150*c <= sugar; % butter constraint 100*b + 150*c <= butter; % cocoa constraint 75*c <= cocoa; % maximize our profit solve maximize 400*b + 450*c; output ["no. of banana cakes = ", show(b), "\n", "no. of chocolate cakes = ", show(c), "\n"]; Figure 4: Data-independent model for determining how many banana and chocolate cakes to bake for the school fete. 9 http://www.minizinc.org/downloads/tutorial-examples-latest/cakes2.mzn PANTRY ≡ [DOWNLOAD] flour = 4000; banana = 6; sugar = 2000; butter = 500; cocoa = 500; PANTRY2 ≡ [DOWNLOAD] flour = 8000; banana = 11; sugar = 3000; butter = 1500; cocoa = 800; Figure 5: Example data files for cakes2.mzn where the data file pantry.dzn is defined in Figure 7 gives the same result as cakes.mzn. The output from running the command $ mzn-g12fd cakes2.mzn pantry2.dzn with an alternate data set defined in Figure 7 is no. of banana cakes = 3 no. of chocolate cakes = 8 Small data files can be entered without directly creating a .dzn file, using the command line flag -D string, where string is the contents of the data file. For example the command $ mzn-g12fd cakes2.mzn -D \ "flour=4000;banana=6;sugar=2000;butter=500;cocoa=500;" will give identical results to $ mzn-g12fd cakes2.mzn pantry.dzn Data files can only contain assignment statements which should be to variables and pa- rameters in a model. Defensive programming suggests that we should check that the values in the data file are reasonable. For our example it is sensible to check that the quantity of all ingredients is non-negative and generate a run-time error if this is not true. MiniZinc provides a built- in Boolean operator for checking parameter values. The form is assert(B,S). The Boolean expression s is evaluated and if it is false execution aborts and the string expression S is evaluated and printed as an error message. To check and generate an appropriate error message if the amount of flour is negative we can simply add the line constraint assert(flour >= 0.0,”Amount of flour is non-negative”);
to our model. Notice that the assert expression is a Boolean expression and so is regarded
as a type of constraint. We can add similar lines to check that the quantity of the other
ingredients is non-negative.
10
http://www.minizinc.org/downloads/tutorial-examples-latest/pantry.dzn
http://www.minizinc.org/downloads/tutorial-examples-latest/pantry2.dzn
LOAN ≡ [DOWNLOAD]
% variables
var float: R; % quarterly repayment
var float: P; % principal initially borrowed
var 0.0 .. 10.0: I; % interest rate
% intermediate variables
var float: B1; % balance after one quarter
var float: B2; % balance after two quarters
var float: B3; % balance after three quarters
var float: B4; % balance owing at end
constraint B1 = P * (1.0 + I) – R;
constraint B2 = B1 * (1.0 + I) – R;
constraint B3 = B2 * (1.0 + I) – R;
constraint B4 = B3 * (1.0 + I) – R;
solve satisfy;
output [
“Borrowing “, show_float(0, 2, P), ” at “, show(I*100.0),
“% interest, and repaying “, show_float(0, 2, R),
“\nper quarter for 1 year leaves “, show_float(0, 2, B4), ” owing\n”
];
Figure 6: Model for determining relationships between a 1 year loan repaying every quarter.
2.4 Real Number Solving
MiniZinc also supports “real number” constraint solving using floating point solving. Con-
sider a problem of taking out a short loan for one year to be repaid in 4 quarterly instalments.
A model for this is shown in Figure 6. It uses a simple interest calculation to calculate the
balance after each quarter.
Note that we declare a float variable f using var float: f , and we can declare a float
variable f in a fixed range l to u with a declaration of the form var l .. u: f , where l and
u are floating point expressions.
We can use the same model to answer a number of different questions. The first question
is: if I borrow $1000 at 4% and repay $260 per quarter, how much do I end up owing? This
question is encoded by the data file loan1.dzn.
Since we wish to use real number solving we need to use a different solver than the
finite domain solver used by mzn-g12fd. A suitable solver would be one that supports mixed
integer linear programming. The MiniZinc distribution contains such a solver. We can invoke
11
http://www.minizinc.org/downloads/tutorial-examples-latest/loan.mzn
LOAN1 ≡ [DOWNLOAD]
I = 0.04;
P = 1000.0;
R = 260.0;
LOAN2 ≡ [DOWNLOAD]
I = 0.04;
P = 1000.0;
B4 = 0.0;
LOAN3 ≡ [DOWNLOAD]
I = 0.04;
R = 250.0;
B4 = 0.0;
Figure 7: Example data files for loan.mzn
it using the command mzn-g12mip
$ mzn-g12mip loan.mzn loan1.dzn
The output is
Borrowing 1000.00 at 4.0% interest, and repaying 260.00
per quarter for 1 year leaves 65.78 owing
———-
The second question is if I want to borrow $1000 at 4% and owe nothing at the end,
how much do I need to repay? This question is encoded by the data file loan2.dzn. The
output from running the command
$ mzn-g12mip loan.mzn loan2.dzn
is
Borrowing 1000.00 at 4.0\% interest, and repaying 275.49
per quarter for 1 year leaves 0.00 owing
———-
The third question is if I can repay $250 a quarter, how much can I borrow at 4% to end
up owing nothing? This question is encoded by the data file loan3.dzn. The output from
running the command
$ mzn-g12mip loan.mzn loan3.dzn
is
Borrowing 907.47 at 4.0\% interest, and repaying 250.00
per quarter for 1 year leaves 0.00 owing
———-
12
http://www.minizinc.org/downloads/tutorial-examples-latest/loan1.dzn
http://www.minizinc.org/downloads/tutorial-examples-latest/loan2.dzn
http://www.minizinc.org/downloads/tutorial-examples-latest/loan3.dzn
Floating point arithmetic Operators
MiniZinc provides the standard floating point arithmetic operators. Addition (+), sub-
traction (-), multiplication (*) and floating point division (/). It also provides + and –
as unary operators.
MiniZinc does not automatically coerce integers to floating point numbers. The built-in
function int2float can be used for this purpose.
MiniZinc also includes the floating point functions for absolute value (abs), square root
(sqrt), natural logarithm (ln), logarithm base 2 (log2), logarithm base 10 (log10),
exponentiation of e (exp), sine (sin), cosine (cos), tangent (tan), arcsine (asin), ar-
ccosine (acos), arctangent (atan), hyperbolic sine (sinh), hyperbolic cosine (cosh),
hyperbolic tangent (tanh), hyperbolic arcsine (asinh), hyperbolic arccosine (acosh),
hyperbolic arctangent (atanh), and power (pow) which is the only binary function, the
rest are unary.
The syntax for arithmetic literals is reasonably standard. Example float literals are 1.05,
1.3e-5 and 1.3+E5.
2.5 Basic structure of a model
We are now in a position to summarise the basic structure of a MiniZinc model. It consists
of multiple items each of which has a semicolon ‘;’ at its end. Items can occur in any order.
For example, identifiers need not be declared before they are used.
There are 7 kinds of items.
• Include items allow the contents of another file to be inserted into the model. They
have the form:
include 〈filename〉;
where filename is a string literal. They allow large models to be split into smaller sub-
models and also the inclusion of constraints defined in library files. We shall see an
example in Figure 11.
• Variable declarations declare new variables. Such variables are global variables and
can be referred to from anywhere in the model. Variables come in two kinds. Pa-
rameters which are assigned a fixed value in the model or in a data file and decision
variables whose value is found only when the model is solved. We say that parame-
ters are fixed and decision variables unfixed. The variable can be optionally assigned a
value as part of the declaration. The form is:
〈type inst expr〉: 〈variable〉 [ = 〈expression〉];
13
The type-inst expr gives the instantiation and type of the variable. These are one of
the more complex aspects of MiniZinc. Instantiations are declared using par for pa-
rameters and var for decision variables. If there is no explicit instantiation declaration
then the variable is a parameter. The type can be a base type, an integer or float range
or an array or a set. The base types are float, int, string, bool, ann of which only
float, int and bool can be used for decision variables. The base type ann is an an-
notation— we shall discuss annotations in section 5. Integer range expressions can be
used instead of the type int. Similarly float range expressions can be used instead of
type float. These are typically used to give the domain of an integer decision variable
but can also be used to restrict the range of an integer parameter.
• Assignment items assign a value to a variable. They have the form:
〈variable〉 = 〈expression〉;
Values can be assigned to decision variables in which case the assignment is equivalent
to writing constraint 〈variable〉 = 〈expression〉;
• Constraint items form the heart of the model. They have the form:
constraint 〈Boolean expression〉;
We have already seen examples of simple constraints using arithmetic comparison and
the built-in assert operator. In the next section we shall see examples of more complex
constraints.
• Solve items specify exactly what kind of solution is being looked for. As we have seen
they have one of three forms:
solve satisfy;
solve maximize 〈arithmetic expression〉;
solve minimize 〈arithmetic expression〉;
A model is required to have exactly one solve item.
• Output items are for nicely presenting the results of the model execution. They have
the form:
output [ 〈string expression〉, · · · , 〈string expression〉 ];
• Predicate and test items are for defining new constraints and Boolean tests. We discuss
these in section 4.
• The annotation item is used to define a new annotation. We discuss these in section 5.
14
3 More Complex Models
In the last section we introduced the basic structure of a MiniZinc model. In this section we
introduce the array and set data structures and more complex constraints.
3.1 Arrays and Sets
Almost always we are interested in building models where the number of constraints and
variables is dependent on the input data. In order to do so we will usually use arrays.
Consider a simple finite element model for modelling temperatures on a rectangular
sheet of metal. We approximate the temperatures across the sheet by breaking the sheet into
a finite number of elements in a 2 dimensional matrix. A model is shown in Figure 8. It
declares the width w and height h of the finite element model. The declaration
ARRAYDEC ≡
array[0..w,0..h] of var float: t; % temperature at point (i,j)
declares a two dimensional array of float variables t with rows numbered 0 to w and columns
0 to h, to represent the temperatures at each point in the metal plate. We can access the
element of the array in the i th row and j th column using an expression t[ i , j ].
Laplace’s equation states that when the plate reaches a steady state the temperature at
each internal point is the average of its orthogonal neighbours. The constraint
EQUATION ≡
% Laplace equation: each internal temp. is average of its neighbours
constraint forall(i in 1..w-1, j in 1..h-1)(
4.0*t[i,j] = t[i-1,j] + t[i,j-1] + t[i+1,j] + t[i,j+1]);
ensures each internal point (i, j) to the average of its four orthogonal neighbours. The
constraints
SIDES ≡
% edge constraints
constraint forall(i in 1..w-1)(t[i,0] = left);
constraint forall(i in 1..w-1)(t[i,h] = right);
constraint forall(j in 1..h-1)(t[0,j] = top);
constraint forall(j in 1..h-1)(t[w,j] = bottom);
constrains the temperatures on each edge to be equal, and gives these temperatures names:
left, right, top and bottom. While the constraints
CORNERS ≡
% corner constraints
constraint t[0,0]=0.0;
constraint t[0,h]=0.0;
constraint t[w,0]=0.0;
constraint t[w,h]=0.0;
15
LAPLACE ≡ [DOWNLOAD]
int: w = 4;
int: h = 4;
◮ ARRAYDEC
var float: left; % left edge temperature
var float: right; % right edge temperature
var float: top; % top edge temperature
var float: bottom; % bottom edge temperature
◮ EQUATION
◮ SIDES
◮ CORNERS
left = 0.0;
right = 0.0;
top = 100.0;
bottom = 0.0;
solve satisfy;
output [ show_float(6, 2, t[i,j]) ++
if j == h then “\n” else ” ” endif |
i in 0..w, j in 0..h
];
Figure 8: Finite element plate model for determining steady state temperatures
(laplace.mzn).
ensure that the corners (which are irrelevant) are set to 0.0. We can determine the temper-
atures in a plate broken into 5 × 5 elements with left, right and bottom temperature 0 and
top temperature 100 with the model shown in Figure 8.
Running the command
$ mzn-g12mip laplace.mzn
gives the output
0.00 100.00 100.00 100.00 0.00
0.00 42.86 52.68 42.86 0.00
0.00 18.75 25.00 18.75 0.00
0.00 7.14 9.82 7.14 0.00
0.00 0.00 0.00 0.00 0.00
———-
16
http://www.minizinc.org/downloads/tutorial-examples-latest/laplace.mzn
Our cake baking problem is an example of a very simple kind