A MiniZinc Tutorial

1 A MiniZinc TutorialKim Marriott and Peter J. Stuckeywith contributions from Leslie De Koninck and Horst SamulowitzContents1 Introduction22 Basic Modelling in Our First Example.. An Arithmetic Optimisation Example.. Datafiles and Assertions.. Real Number Solving.. Basic structure of a model.. 123 More Complex Arrays and Sets.. Global Constraints.. Conditional Expressions.. Complex Constraints.. Set Constraints.. Enumerated Types.. 364 Global Constraints.. Alldifferent.. Cumulative.. Table.. Regular.. Defining Predicates.. Reflection Functions.. Local Variables.. Domain Reflection Functions.. Scope.. 515 Finite Domain Search.. Search Annotations.. Annotations.. 566 Effective Modelling Practices in Variable Bounds.. Unconstrained Variables.. Effective Generators.. Redundant Constraints.. Modelling Choices.. Multiple Modelling and Channels.. 657 Boolean Satisfiability Modelling in Modelling Integers.

2 Modelling Disequality.. Modelling Cardinality.. 69A MiniZinc Keywords77B MiniZinc Operators77C MiniZinc Functions7721 IntroductionMiniZinc 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 theproblem although the model can contain annotations which are used to guide the 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 consistof variable declaration and constraint definitions as well as adefinition of the objective func-tion if the problem is an optimization problem. The translation from MiniZinc to FlatZincis specializable to individual backend solvers, so they can control what form constraints endup in. In particular, MiniZinc allows the specification of global constraints by Basic Modelling in MiniZincIn this section we introduce the basic structure of a MiniZinc model using two simple Our First ExampleFigure 1: Australian our first example, imagine that we wish to colour a map of Australia as shown inFigure 1.

3 It is made up of seven different states and territories each ofwhich must be givena colour so that adjacent regions have different can model this problem very easily in MiniZinc . The model is shown inFigure 2. Thefirst line in the model is a comment. A comment starts with a % which indicates that therest 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 line3 AUST [DOWNLOAD]% Colouring Australia using nc coloursint: nc = 3; : wa; : nt; : sa; : q; : nsw; : v; : t;constraintwa != nt;constraintwa != sa;constraintnt != sa;constraintnt != q;constraintsa != q;constraintsa != nsw;constraintsa != v;constraintq != nsw;constraintnsw != v;solvesatisfy;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 colouring the states and territories in : nc = 3;specifies aparameterin the problem which is the number of colours to be used.

4 Parametersare similar to variables in most programming languages. They must be declared and given atype. In this case the type isint. They are given a value by anassignment. MiniZinc allowsthe assignment to be included as part of the declaration (as in the line above) or to be aseparate assignment statement. Thus the following is equivalent to the single line aboveint: nc;nc = 3;Unlike variables in many programming languages a parameter can only begiven asinglevalue. It is an error for a parameter to occur in more than one basic parameter types are integers (int), floating point numbers (float), Booleans(bool) and strings (string). Arrays and sets are also models can also contain another kind of variable called adecision variables are variables in the sense of mathematical orlogical variables. Unlikeparameters and variables in a standard programming language, the modeller does not need4to give them a value. Rather the value of a decision variable is unknown and it is only whenthe MiniZinc model is executed that the solving system determines if the decision variablecan be assigned a value that satisfies the constraints in the modeland if so what this our example model we associate adecision variablewith each region,wa,nt,sa,q,nsw,vandt, which stands for the (unknown) colour to be used to fill the each decision variable we need to give the set of possible values the variable can is called the variable sdomain.

5 This can be given as part of the variable declaration andthe type of the decision variable is inferred from the type of the values in the MiniZinc decision variables can be Booleans, integers, floating point numbers, or supported are arrays whose elements are decision variables. In our MiniZinc model weuse integers to model the different colours. Thus each of our decision variables is declared tohave the is an integer range expression indicating the set{1,2,..,nc}using thevardeclaration. The type of the values is integer so all of the variables in themodel are integer decision which are used to name parameters and variables are sequences of lower anduppercase alphabetic characters, digits and the underscore _ character. They must startwith a alphabetic character. ThusmyName_2is a valid identifier. MiniZinc (and Zinc)keywordsare not allowed to be used as identifier names, they are listed inAppendix ANeither are MiniZincoperatorsallowed to be used as identifier names; they are listed inAppendix carefully distinguishes between the two kinds of model variables: parametersand decision variables.

6 The kinds of expressions that can be constructed using decisionvariables are more restricted than those that can be built fromparameters. However, in anyplace that a decision variable can be used, so can a parameter ofthe same the distinction between parameters and decision variables is called theinstanti-ationof the variable. The combination of variable instantiation andtype is called you start to use MiniZinc you will undoubtedly see next component of the model are theconstraints. These specify the Boolean expres-sions that the decision variables must satisfy to be a valid solution to the model. In this casewe have a number of not equal constraints between the decision variables enforcing that iftwo states are adjacent then they must have different OperatorsMiniZinc provides the relational operators: equal (=or==), not equal (!=), strictly lessthan (<strictly greater than (>, less than or equal to (<=), and greater than or equal to(>=).))

7 The next line in the model:solvesatisfy;5 Indicates the kind of problem it is. In this case it is asatisfactionproblem: we wish to find avalue for the decision variables that satisfies the constraintsbut we do not care which final part of the model is theoutputstatement. This tells MiniZinc what to printwhen the model has been run and a solution is output statement is followed by alistof strings. These are typically either stringliterals which are written between double quotes and use a C like notation for specialcharacters, or an expression of the formshow(X)whereXis the name of a decisionvariable or parameter. In the example\nrepresents the newline character and\ta are also formatted varieties ofshowfor numbers:show_int(n,X)outputs the valueof integerXin at least|n|characters, right justified ifn>0 and left justified otherwise;show_float(n,d,X)outputs the value of floatXin at least|n|characters, right justified ifn>0 and left justified otherwise, withdcharacters after the decimal literals must fit on a single line.

8 Longer string literals can be split across multiplelines using the string concatenation operator++For example, the string literal"Invaliddatafile: Amount of flour is non-negative"is equivalent to the string literalexpression"Invalid datafile: " ++"Amount of flour is non-negative".A model can contain at most one output the G12 implementation of MiniZinc we can evaluate our model bytyping$ mzn-g12fd the name of the file containing our MiniZinc model. We must use thefile extension .mzn to indicate a MiniZinc model. The commandmzn-g12fduses the G12finite domain solver to evaluate our we run this we obtain the result:wa=1 nt=3 sa=2q=1 nsw=3 v=1t=1----------The line of 10 dashes----------is output automatically added by the MiniZinc output toindicate a solution has been An Arithmetic Optimisation ExampleOur second example is motivated by the need to bake some cakes for afete at our localschool. We know how to make two sorts of banana cake which takes 250g of1 WARNING: please don t use these recipes at home6 CAKES [DOWNLOAD]% Baking cakes for the school : b; % : c; % cakes% flourconstraint250*b + 200*c <= 4000;% bananasconstraint2*b <= 6;% sugarconstraint75*b + 150*c <= 2000;% butterconstraint100*b + 150*c <= 500;% cocoaconstraint75*c <= 500;%maximizeour profitsolve maximize400*b + 450*c;output["no.]

9 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 theschool flour, 2 mashed bananas, 75g sugar and 100g of butter, and a chocolate cakewhich takes 200g of self-raising flour, 75g of cocoa, 150g sugar and 150g of butter. We cansell a chocolate cake for $ and a banana cake for $ And we have 4kg self-raisingflour, 6 bananas, 2kg of sugar, 500g of butter and 500g of cocoa. The question is how manyof each sort of cake should we bake for the fete to maximise the profit. A possible MiniZincmodel is shown inFigure first new feature is the use ofarithmetic arithmetic OperatorsMiniZinc provides the standard integer arithmetic (+), subtrac-tion (-), multiplication (*), integer division (div) and integer modulus (mod). It alsoprovides+and-as unary modulus is defined to give a result(amodb)that has the same sign as thedividenda. Integer division is defined so thata=b*(adivb)+(amodb).

10 MiniZinc provides standard integer functions for absolute value (abs) and power func-tion (pow). For exampleabs(-4)andpow(2,5)evaluate to 4 and 32 syntax for arithmetic literals is reasonably standard. Integer literals can be decimal,hexadecimal or octal. For instance0,005,123,0x1b7, second new feature shown in the example is optimisation. The linesolve maximize400*b + 450*c;specifies that we want to find a solution that maximises the expression in the solve statementcalled theobjective. The objective can be any kind of arithmetic expression. One can replacethe key wordmaximizebyminimizeto specify a minimisation we run this we obtain the cakes = cakes = 2----------==========The line==========is output automatically for optimisation problems when the systemhas proved that a solution is Datafiles and AssertionsA drawback of this model is that if we wish to solve a similar problem the next time we needto bake cakes for the school (which is often) we need to modify the constraints in the modelto reflect the ingredients that we have in the pantry.