程序代写代做代考 database data structure GAGA

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