MiniZinc can be used to model Boolean satisfiability problems where the variables are restricted to be Boolean (:mzn:`bool`). MiniZinc can be used with efficient Boolean satisfiability solvers to solve the resulting models efficiently.
Many times although we wish to use a Boolean satisfiability solver we may need to model some integer parts of our problem.
There are three common ways of modelling an integer variables I in the range 0 \dots m where m = 2^{k}-1 using Boolean variables.
Binary: I is represented by k binary variables i_0, \ldots, i_{k-1} where I = 2^{k-1} i_{k-1} + 2^{k-2} i_{k-2} + \cdots + 2 i_1 + i_0. This can be represented in MiniZinc as
array[0..k-1] of var bool: i; var 0..pow(2,k)-1: I = sum(j in 0..k-1)(bool2int(i[j])*pow(2,j));
Unary: where I is represented by m binary variables i_1, \ldots, i_m and i = \sum_{j=1}^m \mathtt{bool2int}(i_j). Since there is massive redundancy in the unary representation we usually require that i_j \rightarrow i_{j-1}, 1 < j \leq m. This can be represented in MiniZinc as
array[1..m] of var bool: i; constraint forall(j in 2..m)(i[j] -> i[j-1]); var 0..m: I = sum(j in 1..m)(bool2int(i[j]);
Value: where I is represented by m+1 binary variables i_0, \ldots, i_m where I = k \Leftrightarrow i_k, and at most one of i_0, \ldots, i_m is true. This can be represented in MiniZinc as
array[0..m] of var bool: i; constraint sum(j in 0..m)(bool2int(i[j]) == 1; var 0..m: I; constraint forall(j in 0..m)(I == j <-> i[j]);
There are advantages and disadvantages to each representation. It depends on what operations on integers are to required in the model as to which is preferable.
Let us consider modelling a latin squares problem. A latin square is an n \times n grid of numbers from 1..n such that each number appears exactly once in every row and column. An integer model for latin squares is shown in :numref:`ex-latin`.
.. literalinclude:: examples/latin/latin.mzn :language: minizinc :name: ex-latin :caption: Integer model for Latin Squares (:download:`latin.mzn <examples/latin/latin.mzn>`). :playground:`latin`
The only constraint on the integers is in fact disequality, which is encoded in the :mzn:`alldifferent` constraint. The value representation is the best way of representing disequality. A Boolean only model for latin squares is shown in :numref:`ex-latinbool`. Note each integer array element :mzn:`a[i,j]` is replaced by an array of Booleans. We use the :mzn:`exactlyone` predicate to encode that each value is used exactly once in every row and every column, as well as to encode that exactly one of the Booleans corresponding to integer array element :mzn:`a[i,j]` is true.
.. literalinclude:: examples/latinbool/latinbool.mzn :language: minizinc :name: ex-latinbool :caption: Boolean model for Latin Squares (:download:`latinbool.mzn <examples/latinbool/latinbool.mzn>`). :playground:`latinbool`
Let us consider modelling the Light Up puzzle. The puzzle consists of a rectangular grid of squares which are blank, or filled. Every filled square may contain a number from 1 to 4, or may have no number. The aim is to place lights in the blank squares so that
- Each blank square is "illuminated", that is can see a light through an uninterrupted line of blank squares
- No two lights can see each other
- The number of lights adjacent to a numbered filled square is exactly the number in the filled square.
An example of a Light Up puzzle is shown in :numref:`fig-lightup` with its solution in :numref:`fig-lightup-sol`.
An example of a Light Up puzzle
The completed solution of the Light Up puzzle
It is natural to model this problem using Boolean variables to determine which squares contain a light and which do not, but there is some integer arithmetic to consider for the filled squares.
.. literalinclude:: examples/lightup/lightup.mzn :language: minizinc :name: ex-lightup :caption: SAT Model for the Light Up puzzle (:download:`lightup.mzn <examples/lightup/lightup.mzn>`). :playground:`lightup`
A model for the problem is given in :numref:`ex-lightup`. A data file for the problem shown in :numref:`fig-lightup` is shown in :numref:`fig-lightupdzn`.
.. literalinclude:: examples/lightup/lightup.dzn :language: minizinc :name: fig-lightupdzn :caption: Datafile for the Light Up puzzle instance shown in :numref:`fig-lightup` (:download:`lightup.dzn <examples/lightup/lightup.dzn>`). :playground:`lightup`
The model makes use of a Boolean sum predicate
predicate bool_sum_eq(array[int] of var bool:x, int:s);
which requires that the sum of an array of Boolean equals some fixed integer. There are a number of ways of modelling such cardinality constraints using Booleans.
- Adder networks: we can use a network of adders to build a binary Boolean representation of the sum of the Booleans
- Sorting networks: we can use a sorting network to sort the array of Booleans to create a unary representation of the sum of the Booleans
- Binary decision diagrams: we can create a binary decision diagram (BDD) that encodes the cardinality constraint.
.. literalinclude:: examples/bboolsum/bboolsum.mzn :language: minizinc :name: ex-bboolsum :caption: Cardinality constraints by binary adder networks (:download:`bboolsum.mzn <examples/bboolsum/bboolsum.mzn>`). :playground:`bboolsum`
.. literalinclude:: examples/binarysum/binarysum.mzn :language: minizinc :name: ex-binarysum :caption: Code for building binary addition networks (:download:`binarysum.mzn <examples/binarysum/binarysum.mzn>`). :playground:`binarysum`
We can implement :mzn:`bool_sum_eq` using binary adder networks using the code shown in :numref:`ex-bboolsum`. The predicate :mzn:`binary_sum` defined in :numref:`ex-binarysum` creates a binary representation of the sum of :mzn:`x` by splitting the list into two, summing up each half to create a binary representation and then summing these two binary numbers using :mzn:`binary_add`. If the list :mzn:`x` is odd the last bit is saved to use as a carry in to the binary addition.
.. literalinclude:: examples/uboolsum/uboolsum.mzn :language: minizinc :name: ex-uboolsum :caption: Cardinality constraints by sorting networks (:download:`uboolsum.mzn <examples/uboolsum/uboolsum.mzn>`). :playground:`uboolsum`
.. literalinclude:: examples/oesort/oesort.mzn :language: minizinc :name: ex-oesort :caption: Odd-even merge sorting networks (:download:`oesort.mzn <examples/oesort/oesort.mzn>`). :playground:`oesort`
We can implement :mzn:`bool_sum_eq` using unary sorting networks using the code shown in :numref:`ex-uboolsum`. The cardinality constraint is defined by expanding the input :mzn:`x` to have length a power of 2, and sorting the resulting bits using an odd-even merge sorting network. The odd-even merge sorter shown in :mzn:`ex-oesort` works recursively by splitting the input list in 2, sorting each list and merging the two sorted lists.
.. literalinclude:: examples/bddsum/bddsum.mzn :language: minizinc :name: ex-bddsum :caption: Cardinality constraints by binary decision diagrams (:download:`bddsum.mzn <examples/bddsum/bddsum.mzn>`). :playground:`bddsum`
We can implement :mzn:`bool_sum_eq` using binary decision diagrams using the code shown in :mzn:`ex:bddsum`. The cardinality constraint is broken into two cases: either the first element :mzn:`x[1]` is :mzn:`true`, and the sum of the remaining bits is :mzn:`s-1`, or :mzn:`x[1]` is :mzn:`false` and the sum of the remaining bits is :mzn:`s`. For efficiency this relies on common subexpression elimination to avoid creating many equivalent constraints.