Tutorial

In this tutorial we will cover the basics of how to use PyMzn to solve MiniZinc problems inside Python scripts. Bare in mind that this tutorial is not meant to be an introduction to MiniZinc, so if you are new to MiniZinc go check out the official MiniZinc tutorial and then come back here to learn about how to use MiniZinc in Python.

Let’s start with a simple coloring problem of Australia (which happens to be the same of the MiniZinc tutorial):

aust.mzn
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
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=\(wa)\t nt=\(nt)\t sa=\(sa)\n",
    "q=\(q)\t nsw=\(nsw)\t v=\(v)\n",
    "t=", show(t), "\n"
];

Using PyMzn we can call MiniZinc to solve the above problem from a Python script and get the result as a Python object. Calling PyMzn is just as easy as:

import pymzn
solns = pymzn.minizinc('aust.mzn')
print(solns)

which will return a solution like:

[{'wa': 3, 'nt': 2, 'sa': 1, 'q': 3, 'nsw': 2, 'v': 3, 't': 1}]

The pymzn.minizinc function takes as input the path to the MiniZinc file, takes care of launching MiniZinc for you and parses the solution stream to get back solutions as Python dictionaries. Internally, PyMzn takes care of how solutions should be returned by MiniZinc in order to be able to parse them. By default it will ignore the output statement on your MiniZinc model, so you can leave it there, just in case. If instead you want to get solutions as strings formatted according to the output statement present in your MiniZinc model, you can use the option output_mode='item' with the pymzn.minizinc function:

solns = pymzn.minizinc('aust.mzn', output_mode='item')
print(solns[0])

which will print:

wa=3     nt=2    sa=1
q=3      nsw=2   v=3
t=1

There are other options for the output_mode flag, namely dzn, json and raw. The former two return strings formatted as dzn and json respectively, while the latter does not return a list of solutions but rather the entire solution stream as a single string.

As you may have noticed, the pymzn.minizinc function returns an object of type Solutions which in most cases may be addressed and iterated as a list:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
solns = pymzn.minizinc('aust.mzn')

print(type(solns).__name__)
# Solutions

print(len(solns))
# 1

print(type(iter(solns)))
# list_iterator

The Solutions object returned by the pymzn.minizinc function has also few other useful attributes, such as the status attribute:

solns = pymzn.minizinc('aust.mzn')

print(solns.status)
# Status.INCOMPLETE

The status attribute is an instance of a pymzn.Status enum, which represents the status of the solution stream, i.e. wheter it is complete or not, whether the problem is unsatisfiable or there has been an error with the solver. In this case the status is incomplete because it is a satisfiability problem and the solver returned only one of the feasible solution.

To get all the solutions of the problem, we can use the all_solutions flag:

1
2
3
4
5
6
7
solns = pymzn.minizinc('aust.mzn', all_solutions=True)

print(len(solns))
# 18

print(solns.status)
# Status.COMPLETE

To be able to get all the solutions for a satisfiability problem, this feature needs to be supported by the solver. The default solver used by PyMzn is Gecode, which does support this feature.

Data

Let us now move on to another problem, a simple 0-1 knapsack encoded with MiniZinc:

knapsack01.mzn
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
int: n;                     % number of objects
set of int: OBJ = 1..n;
array[OBJ] of int: profit;  % the profit of each object
array[OBJ] of int: size;    % the size of each object
int: capacity;              % the capacity of the knapsack

var set of OBJ: x;
constraint sum(i in x)(size[i]) <= capacity;

var int: obj = sum(i in x)(profit[i]);
solve maximize obj;

output [
    "knapsack = ", show(x), "\n",
    "objective = ", show(obj)
];

As you can see, in the above problem some data is missing, so we need to specify it via a data file or via inline data. Here is a data file for the above problem:

knapsack01.dzn
1
2
3
n = 5;
profit = [10, 3, 9, 4, 8];
size = [14, 4, 10, 6, 9];

In the above file we are still missing the capacity parameter, which we can specify as inline data. To solve the above problem with the provided data we use:

import pymzn
solns = pymzn.minizinc('knapsack01.mzn', 'knapsack01.dzn', data={'capacity': 20})
print(solns)
# [{'x': {3, 5}}]

The second argument we passed to the pymzn.minizinc function is the data file specified above. We also passed the keyword argument data as a dictionary assigning the value 20 to the variable capacity. PyMzn will automatically convert the dictionary into an appropriate dzn representation and pass it to MiniZinc as inline data. PyMzn does so by using the function pymzn.dict2dzn which you can use yourself:

dzn = pymzn.dict2dzn({'capacity': 20})
print(dzn)

which will return a list of dzn assignments, one for each variable, in this case:

['capacity = 20;']

Conveniently, you can also save the dzn assignments directly on a file:

pymzn.dict2dzn({'capacity': 20}, fout='capacity.dzn')

This file can then be used in subsequent calls to the pymzn.minizinc function. We can actually specify as many data files we need as additional positional argument to the pymzn.minizinc function, so the above problem can now be solved with:

solns = pymzn.minizinc('knapsack01.mzn', 'knapsack01.dzn', 'capacity.dzn')
print(solns)
# [{'x': {3, 5}}]

If you want to get back the content of a data file into a Python dictionary, PyMzn also offers the inverse function pymzn.dzn2dict, which accepts the path to a .dzn file as input and returns the content of the file converted to Python objects:

data = pymzn.dzn2dict('capacity.dzn')
print(data)
# {'capacity': 20}

The pymzn.dzn2dict function also accept dzn content directly:

data = pymzn.dzn2dict('capacity = 20;')
print(data)
# {'capacity': 20}

You can read more about converting data to and from dzn format in the Dzn files section.

Solver arguments

Usually, solvers provide arguments that can be used to modify their behavior. You can specify arguments to pass to the solver as additional keyword arguments in the minizinc function. When using Gecode, for example, the fzn_flags option is available, which can take any flag described when executing fzn-gecode --help. The pymzn.minizinc can take fzn_flags as a keyword argument, which will then be passed to the solver, e.g.:

pymzn.minizinc('test.mzn', fzn_flags=['-restart linear', '-restart-base 1.5'])

More details can be found in the Solvers section.