2.1. Basic Modelling in MiniZinc
In this section we introduce the basic structure of a MiniZinc model using two simple examples.
2.1.1. Our First Example
As our first example, imagine that we wish to colour a map of Australia as shown in Fig. 2.1.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.
1% Colouring Australia using nc colours
2int: nc = 3;
3
4var 1..nc: wa; var 1..nc: nt; var 1..nc: sa; var 1..nc: q;
5var 1..nc: nsw; var 1..nc: v; var 1..nc: t;
6
7constraint wa != nt;
8constraint wa != sa;
9constraint nt != sa;
10constraint nt != q;
11constraint sa != q;
12constraint sa != nsw;
13constraint sa != v;
14constraint q != nsw;
15constraint nsw != v;
16solve satisfy;
17
18output ["wa=\(wa)\t nt=\(nt)\t sa=\(sa)\n",
19 "q=\(q)\t nsw=\(nsw)\t v=\(v)\n",
20 "t=", show(t), "\n"];
We can model this problem very easily in MiniZinc. The model is shown in Listing 2.1.1. 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 also has C-style block comments, which start with /* and end with */.
The next part of the model declares the variables in the model. The line
int: nc = 3;
specifies a parameter in the problem which is the
number of colours to be used.
Parameters are similar to (constant) 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, in that sense they are named constants. 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 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, \dots, 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 an alphabetic character. Thus myName_2 is a valid identifier. MiniZinc keywords are not allowed to be used as identifier names, they are listed in Identifiers. Neither are MiniZinc operators allowed to be used as identifier names; they are listed in Operators.
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.
Integer Variable Declarations
An integer parameter variable is declared as either:
int : <var-name>
<l> .. <u> : <var-name>
where <l>
and <u>
are fixed integer expressions.
An integer decision variable is declared as either:
var int : <var-name>
var <l>..<u> : <var-name>
where <l>
and <u>
are fixed integer expressions.
Formally the distinction between parameters and decision variables is called the instantiation 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 expressions 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;
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 and Strings
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(e)
where e
is a MiniZinc expression.
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"
MiniZinc supports
interpolated strings.
Expressions can be embedded directly in string literals,
where a sub string of the form "\(e)"
is replaced by the result of show(e)
.
For example "t=\(t)\n"
produces the same string as
"t=" ++ show(t) ++ "\n"
.
A model can contain multiple output statements. In that case, all outputs are concatenated in the order they appear in the model.
Additionally, output statements can be annotated using a string literal giving a section name. These section names can be then used to filter the output using the --only-sections and --not-sections options.
We can evaluate our model by clicking the Run button in the MiniZinc IDE, or by typing
$ minizinc --solver gecode 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 minizinc with the option --solver gecode uses the Gecode finite domain solver to evaluate our model. If you use the MiniZinc binary distribution, this solver is in fact the default, so you can just run minizinc aust.mzn instead.
When we run this we obtain the result:
wa=3 nt=2 sa=1
q=3 nsw=2 v=3
t=1
----------
The line of 10 dashes ---------- is automatically added by the MiniZinc output to indicate a solution has been found.
2.1.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 (WARNING: please don’t use these recipes at home). A banana cake which takes 250g of 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 Listing 2.1.2.
1% Baking cakes for the school fete
2
3var 0..100: b; % no. of banana cakes
4var 0..100: c; % no. of chocolate cakes
5
6% flour
7constraint 250*b + 200*c <= 4000;
8% bananas
9constraint 2*b <= 6;
10% sugar
11constraint 75*b + 150*c <= 2000;
12% butter
13constraint 100*b + 150*c <= 500;
14% cocoa
15constraint 75*c <= 500;
16
17% maximize our profit
18solve maximize 400*b + 450*c;
19
20output ["no. of banana cakes = \(b)\n",
21 "no. of chocolate cakes = \(c)\n"];
The first new feature is the use of arithmetic expressions.
Integer Arithmetic Operators
MiniZinc provides the standard integer arithmetic operators.
Addition (+),
subtraction (-),
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 function (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, 5, 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 keyword
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.1.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. MiniZinc (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).
1% Baking cakes for the school fete (with data file)
2
3int: flour; %no. grams of flour available
4int: banana; %no. of bananas available
5int: sugar; %no. grams of sugar available
6int: butter; %no. grams of butter available
7int: cocoa; %no. grams of cocoa available
8
9constraint assert(flour >= 0,"Invalid datafile: " ++
10 "Amount of flour should be non-negative");
11constraint assert(banana >= 0,"Invalid datafile: " ++
12 "Amount of banana should be non-negative");
13constraint assert(sugar >= 0,"Invalid datafile: " ++
14 "Amount of sugar should be non-negative");
15constraint assert(butter >= 0,"Invalid datafile: " ++
16 "Amount of butter should be non-negative");
17constraint assert(cocoa >= 0,"Invalid datafile: " ++
18 "Amount of cocoa should be non-negative");
19
20var 0..100: b; % no. of banana cakes
21var 0..100: c; % no. of chocolate cakes
22
23% flour
24constraint 250*b + 200*c <= flour;
25% bananas
26constraint 2*b <= banana;
27% sugar
28constraint 75*b + 150*c <= sugar;
29% butter
30constraint 100*b + 150*c <= butter;
31% cocoa
32constraint 75*c <= cocoa;
33
34% maximize our profit
35solve maximize 400*b + 450*c;
36
37output ["no. of banana cakes = \(b)\n",
38 "no. of chocolate cakes = \(c)\n"];
Our new model is shown in Listing 2.1.3. We can run it using the command
$ minizinc cakes2.mzn pantry.dzn
where the data file pantry.dzn is defined in Listing 2.1.4. This gives the same result as cakes.mzn. The output from running the command
$ minizinc cakes2.mzn pantry2.dzn
with an alternate data set defined in Listing 2.1.5 is
no. of banana cakes = 3
no. of chocolate cakes = 8
----------
==========
If we remove the output statement from cakes.mzn then MiniZinc will use a default output. In this case the resulting output will be
b = 3;
c = 8;
----------
==========
Default Output
A MiniZinc model with no output will output a line for each decision variable with its value, unless it is assigned an expression on its declaration. Note how the output is in the form of a correct datafile.
Declarations can be annotated as :: output or :: no_output to override the default behaviour.
1flour = 4000;
2banana = 6;
3sugar = 2000;
4butter = 500;
5cocoa = 500;
1flour = 8000;
2banana = 11;
3sugar = 3000;
4butter = 1500;
5cocoa = 800;
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
$ minizinc cakes2.mzn -D \
"flour=4000;banana=6;sugar=2000;butter=500;cocoa=500;"
will give identical results to
$ minizinc cakes2.mzn pantry.dzn
Data files can only contain assignment statements for decision variables and parameters in the model(s) for which they are intended.
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
B 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,"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.
2.1.4. Real Number Solving
MiniZinc also supports “real number” constraint solving using floating point variables and constraints. Consider 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 Listing 2.1.6. It uses a simple interest calculation to calculate the balance after each quarter.
1% variables
2var float: R; % quarterly repayment
3var float: P; % principal initially borrowed
4var 0.0 .. 10.0: I; % interest rate (per quarter)
5
6% intermediate variables
7var float: B1; % balance after one quarter
8var float: B2; % balance after two quarters
9var float: B3; % balance after three quarters
10var float: B4; % balance owing at end
11
12constraint B1 = P * (1.0 + I) - R;
13constraint B2 = B1 * (1.0 + I) - R;
14constraint B3 = B2 * (1.0 + I) - R;
15constraint B4 = B3 * (1.0 + I) - R;
16
17solve satisfy;
18
19output [
20 "Borrowing ", show_float(0, 2, P), " at ", show(I*100.0),
21 "% interest, and repaying ", show_float(0, 2, R),
22 "\nper quarter for 1 year leaves ", show_float(0, 2, B4), " owing\n"
23];
Note that we declare a float variable f
similar to an integer variable using the keyword float
instead of
int
.
We can use the same model to answer a number of different questions. The first question is: if I borrow $1000 at 4% quarterly interest 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 variables and constraint we need to use a solver
that supports this type of problem. While Gecode (the default solver in the MiniZinc bundled binary distribution) does support floating point variables, a mixed integer linear programming (MIP) solver may be better suited to this particular type of problem.
The MiniZinc distribution contains such a solver. We can invoke it by selecting COIN-BC from the solver configuration menu in the IDE, or on the command line using the command minizinc --solver cbc. Note: When solving this problem with the MiniZinc IDE, you will have to open the tab with the data file loan1.dzn and then click the Run button. If you just click Run in the original model file, the IDE won’t know that any data is missing (since all inputs were declared var
), and not pop up the dialog for selecting a data file.
$ minizinc --solver cbc 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
$ minizinc --solver cbc 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
$ minizinc --solver cbc 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
----------
I = 0.04;
P = 1000.0;
R = 260.0;
I = 0.04;
P = 1000.0;
B4 = 0.0;
I = 0.04;
R = 250.0;
B4 = 0.0;
Float Arithmetic Operators
MiniZinc provides the standard floating point arithmetic operators: addition (+), subtraction (-), multiplication (*) and floating point division (/). It also provides + and - as unary operators.
MiniZinc can automatically coerce integers to
floating point numbers. But to make the coercion explicit, the built-in function
int2float
can be used. Note that one consequence of the automatic coercion is that
an expression a / b
is always considered a floating point division. If
you need an integer division, make sure to use the div
operator!
MiniZinc provides in addition the following floating point functions: 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), arc-cosine (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.3E+5.
2.1.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 8 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 Listing 2.2.4.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. Parameters 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 parameters are fixed and decision variables are unfixed. The variable can be optionally assigned a value as part of the declaration. The form is:
<type inst expr>: <variable> [ = ] <expression>;
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 usingpar
for parameters andvar
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 arefloat
,int
,string
,bool
,ann
of which onlyfloat
,int
andbool
can be used for decision variables. The base typeann
is an annotation – we shall discuss annotations in Search. Integer range expressions can be used instead of the typeint
. Similarly float range expressions can be used instead of typefloat
. These are typically used to give the domain of a decision variable but can also be used to restrict the range of a parameter. Another use of variable declarations is to define enumerated types, which we discuss in Enumerated Types.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 at most one solve item. If it’s omitted, it is treated as
solve satisfy
.Output items are for nicely presenting the results of the model execution. They have the form:
output [ <string expression>, ..., <string expression> ];
If there is no output item, MiniZinc will by default print out the values of all the decision variables which are not optionally assigned a value in the format of assignment items. The output and no_output annotations can be used to control this on a per-variable basis.
Enumerated type declarations. We discuss these in Arrays and Sets and Enumerated Types.
Predicate, function and test items are for defining new constraints, functions and Boolean tests. We discuss these in Predicates and Functions.
The annotation item is used to define a new annotation. We discuss these in Search.