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.

2 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.. 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.

3 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. 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 .

4 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.

5 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.

6 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. 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.

7 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.

8 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 (!)

9 =), strictly lessthan (<strictly greater than (>, less than or equal to (<=), and greater than or equal to(>=).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.)

10 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. 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.