MiniZinc allows us to directly describe and solve discrete optimization problems. MiniZinc is a modeling language, you can throw the problem at different solvers. Instead of using a specific solver directly, the benefit of using a modeling language is that the user can try different solvers easily to find the one that works best for their problem.
Grammar Basics
Types in MiniZinc are rather restricted: int, float, bool, string (only fixed strings), array and set.
Variables
MiniZinc has two kinds of variables: parameters and decision variables
| Parameters | Input – fixed information used to describe the problem[par] <type>: <var-name> [= <expression>];The assignment gives a value to a parameter. int: m; m = n * 3;Like variables in any standard programming language: Must be declared with a type int, float or bool (or a range l..u or a set {...})Must be assigned a value (but only once) May be prefixed with par (but this is optional) |
| Decision variables | Output – the decisions we wish to make to solve the problemvar <type>: <var-name> [= <expression>];The assignment defines a decision variable name for an expression. var int: d; d = abs(x-y);The variable that solver is going to work out the value to. Declared with var and a type (or a range l..u or a set {...})Can be assigned once with a fix value expression The following are logically equivalent: var int: i; constraint i >= 0; constraint i <= 4;We can use decision variables as part of index expression in array. |
Comments are anything in a line after %, or anything between /* and */.
Enumerated Types
Enumerated types enum define a finite set of named objects. Parameters, decision variables, array indices and sets may be enum.
% declaration
enum <enum-name>;
% enums are defined as a set of identifiers
<enum-name> = {id1, ..., idn};
% then declare variables and parameters using the enum type
var <enum-name>: <var-name>;
par <enum-name>: <par-name>;Built-in functions to manipulate enumerate types are enum_next, enum_prev, to_enum.
Boolean
Boolean expression can appear in constraints, where conditions, if-then-else-endif conditions, and boolean variables. The simplest way of course is to write in one of the built-in constraints like greater than > or less than or equal to <=.
bool: b = x > 0;
int: z = sum(i in 1..4 where a[i] != 0) (y[i]);
int: t = if b /\ z < 7 then x else z endif;
bool: c = x > 0 /\ t > 0 -> z < 0;You can also build boolean expression of more complicated forms:
| Conjunction | b1 /\ b2 |
| Disjunction | b1 \/ b2 |
| Implication | b1 -> b2 |
| Bi-implication | b1 <-> b2 |
| Negation | not b1 |
The forall function is very commonly used to define large collections of constraints, it maps a list of boolean expression to a conjunction:
forall(i in range)([b1, b2, ..., bn])
% produces
b1 /\ b2 /\ ... /\ bn The exists function maps a list of boolean expressions to a disjunction. exists is less used than forall, since we should try to avoid disjunction in our models when possible.
exists(i in range)([b1, b2, ..., bn])
% produces
b1 \/ b2 \/ ... \/ bn Note empty set [], exists([]) = true, and forall([]) = false.
Constraints
Constraints in MiniZinc are written in the form:
constraint <constraint-expression>;There are situations that listing all constraints are too tedious and long, for example, when all variables all have different values. We can use a global constraint, which technically is any constraint that can take an unbounded number of variables as input. Global constraints make models smaller and solving easier. The example below is effectively saying “everything in the list has to be different”:
include "alldifferent.mzn";
constraint alldifferent([var1, var2, ...]);Reification
The underlying constraint solvers take basically a set of variables and a conjunction of constraints on these variables. When complex boolean expressions are used, they need to be mapped to conjunctions. This process is called flattening, the key trick it uses is what is called reification, which is basically giving names to all of the boolean sub-expressions. For example:
constraint x > 0 \/ y > 0;
% is flattened to
var bool: b1;
constraint b1 = x > 0; % reified
var bool: b2;
constraint b2 = y > 0; % reified
constraint b1 \/ b2Top level conjunction does not cause problem for flattening, the underlying solver can handle them. Note when conjunction is used inside something else, i.e.not at the top level, then we have to reify.
constraint b -> x > 0 /\ y > 0;
% top level is b -> ...
% second level is ... /\ ... which needs to reifyModels are likely to be more efficient if disjunction and negation are not used, since both of them are going to be flattened using reification. Also we usually can not use global constraints except at the top level conjunction.
constraint b \/ alldifferent(...);
% this is a disjuction which is likely to lead to errorStrings and Output
Strings are principally provided for output, but also in debugging constructs such as assertions and tracing. Outputs are written in the form below, the string literals are enclosed in ". Backslash is used for special characters \n, \t, etc. Note outputs can not extend across more than one line. If you don’t declare an output statement, then MiniZinc will output all the declared variables in your model which are not assigned to an expression.
output <list-of-strings>;There are a few built-in functions for string:
show(v)displays the value ofvas a string\(v)displaysvinside a string literal++is used to concatenate two strings
All expressions in output statements not wrapped in show() must be fixed. This is because the output statement runs after the solver. In order to ensure a variable expression is fixed, we use the fix(expression) function, which will abort if the expression does not have a fixed value, otherwise returns a fixed value.
Sets
Sets can be used as types. You may define sets of integers, enums, floats, or booleans. Set literals are of form {e1, ..., en}. Integer or float ranges l..u are also sets. Range is defined as l..u. If l and u are int, l..u is equivalent to a set of integer {l, l+1, ..., u}.
To define a set, use this syntax:
set of <type>: <set-name> = <fixed-set>;
e.g.:
set of int: ROW = 1..6;
set of int: PRIME = {2,3,5,7};
set of float: RAN = 3.0 .. 5.0;
set of float: NUM = {2.87, 3.14};
set of bool: TRUE = {true};Built-in set operators are in, union, intersect, subset, superset, diff, symdiff, card.
Set Comprehensions
MiniZinc provides comprehensions, a set comprehension has form:
{expression | generator1, generator2, ... where bool-expression}
% generator is in the form
% <var-name> in <set-expression>
% e.g. i, j in 1..10Arrays
Array can be multidimensional, each dimension is a range, or an enumerated type, or a fixed set. To lookup an array, uses index of each range. Elements of an array can be anything but another array. The built-in function length() returns the length of a 1-dimensional array.
% array declaration
array[index-set1, index-set2, ...] of <type>: <array-name>
% array lookup
array-name[index1, index2, ...]For instance here we associate with each DISH a satisfaction rating and with each DISH a size and with each DISH an amount.
enum DISH; % range
array[DISH] of int: rating; % parameter array
array[DISH] of int: size; % parameter array
array[DISH] of var int: amount % decision variable array1-dimensional arrays are initialized using a list:
array-1d = [400, 6, 2000, 60, 50];2-dimensional arrays are initialized using a special syntax, the array starts with [|, end with |], for each separates rows | is used.
array-2d = [| 0,9,3,4
| 4,5,6,7
| 8,2,4,5 |];Arrays on any dimension (<= 6) can be initialized using the arraynd()family of functions which turns an 1-dimensional array into an n-dimensional array:
% first dimension is size 5, second dimension is size 4
array-2d = array2d(1..5, 1..4,
[1,2,3,4,5,
6,7,8,9,0,
0,9,8,7,6,
5,4,3,2,1,
1,2,3,4,5]);Concatenation ++ can be used with 1-dimensinal arrays, e.g. profit = [...] ++ [...].
Iteration
MiniZinc provides a variety of built-in functions for operating over a list of a set:
- Lists of numbers:
sum,product,min,max - Lists of constraints:
forall,exists
forall(i in range)(boolean-expression) and sum(i in range)(expression) are usually used together with array lookups, for instance, we have two constraints:
% apply the constraint to each item in the array
constraint forall(i in DISH) (amount[i] >= 0);
% summing up over all items in the array, and apply the constraint
constraint sum(i in DISH) (size[i] * amount[i]) <= capacity;forall() is special because it can be equivalently expressed in the form of array comprehension:
forall(i, j in 1..10 where i < j) (a[i] != a[j]);
= forall( [ a[i] != a[j] | i, j in 1..10 where i < j ] )Array Comprehensions
MiniZinc provides array comprehensions like many other languages:
[expression | generator1, generator2, ... where bool-expression]
% generator is in the form
% <var-name> in <set-expression>
e.g. [i + j | i, j in 1..4 where i < j]
= [1+2, 1+3, 1+4, 2+3, 2+4, 3+4]
= [3,4,5,5,6,7]We can use array comprehension to flatten an n-dimensional array into an 1-dimensional array:
array[1..20] of int: list = array-2d[i,j] | i in 1..5, j in 1..4];Option Types
Many models involve decisions that are only meaningful if other decisions are made in a particular way. In particular we want to make sure that if these optional decisions aren’t meaningful, if they don’t have any meaning, then they can’t constrain any other part of the problem.
Option types basically extend the base types by adding on extra value <> (called opt). Option type variables:
- Act like a normal variable if they take a value different from
<>. - Act as if they were not part of the constraint if they take the value
<>.
For instance, alldifferent([3, <>, 6, 1, <>, <>, 8, 7, 5]) holds. Option types is every where. When you iterate over variable sets, you are actually implicitly using option types:
var set of 1..n: x;
sum(i in x) (size[i]) <= cap;
% is syntactic sugar for
sum(i in 1..n)
(if i in x then size[i] else <> endif) <= cap;
% The <> acts like 0 in a sum since it is +.Option types variables in expressions will act like an identity if one exists in that position:
<> + 3 = 3;
2 - <> = 2;
<> * <> = 1;Option types variables in expressions will propagate <> if there is no identity in that position:
<> - 2 = <>;
<> / 4 = <>;If you use option types in user defined predicates and functions, you need to define the behavior.
Similarly, the same thing happens if i have a variable where clause:
var set of 1..n: x;
sum(i in 1..n where i in x)(size[i]) <= cap;
% is also a syntactic sugar for
sum(i in 1..n)
(if i in x then size[i] else <> endif) <= cap;Take an example, given n workers and 2m tasks (arranged in two rows): 1 .. m and m+1 .. 2m, assign workers to tasks to maximize profit, but where workers assigned to two adjacent tasks must be compatible.
int: n;
set of int: W = 1..n; % workers
int: m;
set of int: T = 1..2*m; % tasks
% parameters
array[W,T] of int: profit;
array[W,W] of bool: compatible;
% decision variables
array[W] of var T: task; % task assignment to a worker
% constraint
alldifferent(task);
% use implication to model compatibility
% but generate a large number of weak constraints
% if two workers are adjacent then they must be compatible
forall(w1, w2 in W)
(task[w2] = task[w1] + 1 /\ task[w1] != m -> compatible[w1, w2] )
% objective
maximize sum(w in W)(profit[w, task[w]]);A better idea is to use option types. We would like to invert the task, i.e. map each task to a worker (or to no worker at all, because it is not a bijection). Option types add an extra value <> to a type.
% use inverse function to model compatibility
% much more directly
array[T] of var opt W: worker; % worker assignment to a task
inverse(task, worker);
forall(t in 1..2*m-1 where t != m)
(compatible[worker[t], worker[t+1]])
% compatible[w1, w2] must hold if either w1 = <> or w2 = <>Optimization vs Satisfaction Problems
MiniZinc can solve both optimization problems (using solve maximize <expression>; or solve minimize <expression>;) and satisfaction problems (using solve satisfy;).
Solving an optimization problem is to find the best solution. Knapsack (a mixed integer program) is a well known example:
% parameters
par int: budget = 10000;
% decision variables
var 0..1000: F;
var 0..400: L;
var 0..500: Z;
var 0..150: J;
% constraints
constraint 13*F + 21*L + 17*Z + 100*J <= budget;
% objective
solve maximize 6*F + 10*L + 8*Z + 40*J;
% output
output ["F = \(F), L = \(L), Z = \(Z), J = \(J)"];Run the model, and the result is below. The objective value is 4752 and size is 496.
F = 0, L = 392, Z = 104, J = 0
---------- this line indicates a solution
========== this line indicates best solution (no better solution)
Finished in 794msec.Another kind of problem that MiniZinc can solve is satisfaction problems, the purpose is to find one solution which is not necessarily the best or optimal. In this case, the constraints do not need to be just linear equalities = and inequalities <, >, <=, >=; they can be modulo mod, multiplication *, division /, disequality !=, and much more. One of the powers of modern modeling language is being able to write down very complex, highly non-linear constraints, and have our solver solve them.
An example of satisfaction problem is here:
var 100..800: army;
constraint army mod 5 = 2;
constraint army mod 7 = 2;
constraint army mod 12 = 1;
solve satisfy;
Run the model, and the result is below:
army = 457;
----------
Finished in 658msec.Another classic satisfaction problem is coloring a map (graph). At least 4 kinds of colors are required the color countries such that adjacent countries do not share the same color:
enum COLOR = {GREEN, BLUE, PINK, YELLOW};
var COLOR: Yi;
var COLOR: Jing;
var COLOR: Yu;
var COLOR: Xu;
var COLOR: Yang;
var COLOR: Jiao;
constraint Yi != Jing;
constraint Yi != Jiao;
constraint Jing != Yu;
constraint Jing != Yang;
constraint Jing != Jiao;
constraint Jiao != Yang;
constraint Yu != Xu;
constraint Yu != Yang;
constraint Xu != Yang;
solve satisfy;Run the mode, the result is:
Yi = GREEN;
Jing = BLUE;
Yu = PINK;
Xu = BLUE;
Yang = GREEN;
Jiao = PINK;
----------
Finished in 96msec.Separation of Data from Model
A model is a formal description of a class of optimization problems. An instance of a model is one particular problem. To make a model into an instance is just to add data. The separation of data from model is very useful when you want to try difference scenarios. Usually data files *.dzn define values for parameters, but also possible for decision variables. Any parameters not assigned in the model *.mzn must be assigned in the data file *.dzn.
Suppose you want to borrow money from a bank. The bank will lend an amount, i.e. principle P, asking a regular payment R every quarter at the quarterly interest rate l. At the end of i-th quarter, the balance owing is given by the previous balance plus the interest on the previous balance minus the repayment. Suppose the loan is paid back over 4 installments in the following year. The mode (a *.mzn file without data) can be:
var float: P;
var float: R;
var 0.0 .. 4.0: l;
var float: B1;
var float: B2;
var float: B3;
var float: B4;
constraint B1 = P * (1.0 + l) - R;
constraint B2 = B1 * (1.0 + l) - R;
constraint B3 = B2 * (1.0 + l) - R;
constraint B4 = B3 * (1.0 + l) - R;
solve satisfy;For different situations / scenarios, we can create data files accordingly:
| Scenarios | Data file *.dzn | Result |
| Fixed principal, repayment, and interest rate. What is the remaining balance at the end of the year? Answer: 657.78 | P = 10000.0 | P = 10000.0; |
| Fixed principal, and repayment. We want to own nothing at the end. What is the interest rate? Answer: 0.077 | P = 10000.0 | P = 10000.0; |
Model: Production Planning
Production planning is a very generic form of problems. We have products, and each of them consumes some amount of resources. We have constraints (limits) on resources and our objective is to maximize profit.
%%% parameters
% products
enum PRODUCT;
% profit per unit for each product
array[PRODUCT] of float: profit;
% resources
enum RESOURCE;
% amount of each resource available;
array[RESOURCE] of float: capacity;
% unit of each resource required to produce 1 unit of product
array[PRODUCT, RESOURCE] of float: consumption;
%%% decision variables
% how much should we make of each product
array[PRODUCT] of var int: produce;
% must produce a non-negative amount
constraint forall(p in PRODUCT) (produce[p] >= 0);
% production can only use the available resources
constraint forall(r in RESOURCE) (
sum(p in PRODUCT) (consumption[p, r] * produce[p]) <= capacity[r]
);
%%% objective
% maximize profit
solve maximize sum(p in PRODUCT) (profit[p] * produce[p]);
% output
output ["\(p): \(produce[p])" | p in PRODUCT];For more on MiniZinc Introduction, please refer to the wonderful course here https://www.coursera.org/learn/basic-modeling
Related Quick Recap
I am Kesler Zhu, thank you for visiting my website. Check out more course reviews at https://KZHU.ai
