2.8. Boolean Satisfiability Modelling in MiniZinc

MiniZinc can be used to model Boolean satisfiability problems where the variables are restricted to be Boolean (bool). MiniZinc can be used with efficient Boolean satisfiability solvers to solve the resulting models efficiently.

2.8.1. Modelling Integers

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.

2.8.2. Modelling Disequality

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

Listing 2.8.1 Integer model for Latin Squares (latin.mzn).
int: n; % size of latin square
array[1..n,1..n] of var 1..n: a;

include "alldifferent.mzn";
constraint forall(i in 1..n)(
             alldifferent(j in 1..n)(a[i,j]) /\
             alldifferent(j in 1..n)(a[j,i])
           );
solve satisfy;
output [ show(a[i,j]) ++ if j == n then "\n" else " " endif |
         i in 1..n, j in 1..n ];

The only constraint on the integers is in fact disequality, which is encoded in the alldifferent constraint. The value representation is the best way of representing disequality. A Boolean only model for latin squares is shown in Listing 2.8.2. Note each integer array element a[i,j] is replaced by an array of Booleans. We use the 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 a[i,j] is true.

Listing 2.8.2 Boolean model for Latin Squares (latinbool.mzn).
int: n; % size of latin square
array[1..n,1..n,1..n] of var bool: a;

predicate atmostone(array[int] of var bool:x) =
          forall(i,j in index_set(x) where i < j)(
            (not x[i] \/ not x[j]));
predicate exactlyone(array[int] of var bool:x) =
          atmostone(x) /\ exists(x);

constraint forall(i,j in 1..n)(
             exactlyone(k in 1..n)(a[i,j,k]) /\
             exactlyone(k in 1..n)(a[i,k,j]) /\
             exactlyone(k in 1..n)(a[k,i,j])
           );
solve satisfy;
output [ if fix(a[i,j,k]) then
            show(k) ++ if j == n then "\n" else " " endif 
         else "" endif | i,j,k in 1..n ];

2.8.3. Modelling Cardinality

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 Fig. 2.8.1 with its solution in Fig. 2.8.2.

images/lightup.svg

Fig. 2.8.1 An example of a Light Up puzzle

images/lightup2.svg

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

Listing 2.8.3 SAT Model for the Light Up puzzle (lightup.mzn).
int: h; set of int: H = 1..h; % board height
int: w; set of int: W = 1..w; % board width
array[H,W] of -1..5: b;       % board
int: E = -1;                  % empty square
set of int: N = 0..4;         % filled and numbered square
int: F =  5;                  % filled unnumbered square

% position (i1,j1) is visible to (i2,j2)
test visible(int: i1, int: j1, int: i2, int: j2) = 
    ((i1 == i2) /\ forall(j in min(j1,j2)..max(j1,j2))(b[i1,j] == E))
 \/ ((j1 == j2) /\ forall(i in min(i1,i2)..max(i1,i2))(b[i,j1] == E));

array[H,W] of var bool: l; % is there a light

% filled squares have no lights
constraint forall(i in H, j in W where b[i,j] != E)(l[i,j] == false);
% lights next to filled numbered square agree

constraint forall(i in H, j in W where b[i,j] in N)(
    bool_sum_eq([ l[i1,j1] | i1 in i-1..i+1, j1 in j-1..j+1 where
                             abs(i1 - i) + abs(j1 - j) == 1 /\
                             i1 in H /\ j1 in W ], b[i,j]));
% each blank square is illuminated
constraint forall(i in H, j in W where b[i,j] == E)(
             exists(j1 in W where visible(i,j,i,j1))(l[i,j1]) \/
             exists(i1 in H where visible(i,j,i1,j))(l[i1,j]) 
           );
% no two lights see each other
constraint forall(i1,i2 in H, j1,j2 in W where 
                  (i1 != i2 \/ j1 != j2) /\ b[i1,j1] == E 
                  /\ b[i2,j2] == E /\ visible(i1,j1,i2,j2))(
             not l[i1,j1] \/ not l[i2,j2]
           );

solve satisfy;
output [ if b[i,j] != E then show(b[i,j])
         else if fix(l[i,j]) then "L" else "." endif
         endif ++ if j == w then "\n" else " " endif |
         i in H, j in W];

A model for the problem is given in Listing 2.8.3. A data file for the problem shown in Fig. 2.8.1 is shown in Listing 2.8.4.

Listing 2.8.4 Datafile for the Light Up puzzle instance shown in Fig. 2.8.1 (lightup.dzn).
h = 7;
w = 7;
b = [| -1,-1,-1,-1, 0,-1,-1 
     | -1,-1,-1,-1,-1,-1,-1
     |  0,-1,-1, 3,-1,-1,-1
     | -1,-1, 2,-1, 4,-1,-1
     | -1,-1,-1, 5,-1,-1, 1
     | -1,-1,-1,-1,-1,-1,-1
     |  1,-1, 2,-1,-1,-1,-1 |];

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.

Listing 2.8.5 Cardinality constraints by binary adder networks (bboolsum.mzn).
% the sum of booleans x = s
predicate bool_sum_eq(array[int] of var bool:x, int:s) =
     let { int: c = length(x) } in
     if s < 0 then false 
     elseif s == 0 then
          forall(i in 1..c)(x[i] == false)
     elseif s < c then
          let { % cp = number of bits required for representing 0..c
                int: cp = floor(log2(int2float(c))),
                % z is sum of x in binary 
                array[0..cp] of var bool:z  } in
          binary_sum(x, z) /\ 
          % z == s
          forall(i in 0..cp)(z[i] == ((s div pow(2,i)) mod 2 == 1)) 
     elseif s == c then
          forall(i in 1..c)(x[i] == true)
     else false endif;

include "binarysum.mzn";
Listing 2.8.6 Code for building binary addition networks (binarysum.mzn).
% the sum of bits x = s in binary. 
%            s[0], s[1], ..., s[k] where 2^k >= length(x) > 2^(k-1)
predicate binary_sum(array[int] of var bool:x, 
                     array[int] of var bool:s)=
     let { int: l = length(x) } in 
     if l == 1 then s[0] = x[1]
     elseif l == 2 then 
             s[0] = (x[1] xor x[2]) /\ s[1] = (x[1] /\ x[2])
     else let { int: ll = (l div 2),
                array[1..ll] of var bool: f = [ x[i] | i in 1..ll ], 
                array[1..ll] of var bool: t = [x[i]| i in ll+1..2*ll],
                var bool: b = if ll*2 == l then false else x[l] endif,
                int: cp = floor(log2(int2float(ll))),
                array[0..cp] of var bool: fs,
                array[0..cp] of var bool: ts } in
                binary_sum(f, fs) /\ binary_sum(t, ts) /\
                binary_add(fs, ts, b, s)
     endif;

% add two binary numbers x, and y and carry in bit ci to get binary s
predicate binary_add(array[int] of var bool: x,
                     array[int] of var bool: y,
                     var bool: ci,
                     array[int] of var bool: s) =
    let { int:l = length(x), 
          int:n = length(s), } in  
    assert(l == length(y),
          "length of binary_add input args must be same",
    assert(n == l \/ n == l+1, "length of binary_add output " ++
                         "must be equal or one more than inputs",
    let { array[0..l] of var bool: c } in
    full_adder(x[0], y[0], ci, s[0], c[0]) /\
    forall(i in 1..l)(full_adder(x[i], y[i], c[i-1], s[i], c[i])) /\
    if n > l then s[n] = c[l] else c[l] == false endif ));
    
predicate full_adder(var bool: x, var bool: y, var bool: ci,
                     var bool: s, var bool: co) =
          let { var bool: xy = x xor y } in 
          s = (xy xor ci) /\ co = ((x /\ y) \/ (ci /\ xy));

We can implement bool_sum_eq using binary adder networks using the code shown in Listing 2.8.5. The predicate binary_sum defined in Listing 2.8.6 creates a binary representation of the sum of x by splitting the list into two, summing up each half to create a binary representation and then summing these two binary numbers using binary_add. If the list x is odd the last bit is saved to use as a carry in to the binary addition.

Listing 2.8.7 Cardinality constraints by sorting networks (uboolsum.mzn).
% the sum of booleans x = s
predicate bool_sum_eq(array[int] of var bool:x, int:s) =
     let { int: c = length(x) } in
     if s < 0 then false 
     elseif s == 0 then forall(i in 1..c)(x[i] == false)
     elseif s < c then
          let { % cp = nearest power of 2 >= c
                int: cp = pow(2,ceil(log2(int2float(c)))),
                array[1..cp] of var bool:y, % y is padded version of x
                array[1..cp] of var bool:z  } in
          forall(i in 1..c)(y[i] == x[i]) /\
          forall(i in c+1..cp)(y[i] == false) /\
          oesort(y, z) /\ z[s] == true /\ z[s+1] == false
     elseif s == c then forall(i in 1..c)(x[i] == true)
     else false endif;

include "oesort.mzn";
Listing 2.8.8 Odd-even merge sorting networks (oesort.mzn).
%% odd-even sort
%% y is the sorted version of x, all trues before falses
predicate oesort(array[int] of var bool:x, array[int] of var bool:y)=
  let { int: c = card(index_set(x)) } in
  if c == 1 then x[1] == y[1] 
  elseif c == 2 then comparator(x[1],x[2],y[1],y[2])
  else
    let { 
      array[1..c div 2] of var bool:xf = [x[i] | i in 1..c div 2],
      array[1..c div 2] of var bool:xl = [x[i] | i in c div 2 +1..c],
      array[1..c div 2] of var bool:tf,
      array[1..c div 2] of var bool:tl } in
    oesort(xf,tf) /\ oesort(xl,tl) /\ oemerge(tf ++ tl, y)
  endif;

%% odd-even merge
%% y is the sorted version of x, all trues before falses
%% assumes first half of x is sorted, and second half of x
predicate oemerge(array[int] of var bool:x, array[int] of var bool:y)=
  let { int: c = card(index_set(x)) } in
  if c == 1 then x[1] == y[1] 
  elseif c == 2 then comparator(x[1],x[2],y[1],y[2])
  else
    let { array[1..c div 2] of var bool:xo = 
            [ x[i] | i in 1..c where i mod 2 == 1],
          array[1..c div 2] of var bool:xe = 
            [ x[i] | i in 1..c where i mod 2 == 0],
          array[1..c div 2] of var bool:to,
          array[1..c div 2] of var bool:te } in
      oemerge(xo,to) /\ oemerge(xe,te) /\
      y[1] = to[1] /\
      forall(i in 1..c div 2 -1)(
        comparator(te[i],to[i+1],y[2*i],y[2*i+1])) /\ 
      y[c] = te[c div 2]
  endif;
 
% comparator o1 = max(i1,i2), o2 = min(i1,i2)
predicate comparator(var bool:i1,var bool:i2,var bool:o1,var bool:o2)=
          (o1 = (i1 \/ i2)) /\ (o2 = (i1 /\ i2));

We can implement bool_sum_eq using unary sorting networks using the code shown in Listing 2.8.7. The cardinality constraint is defined by expanding the input 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 ex-oesort works recursively by splitting the input list in 2, sorting each list and merging the two sorted lists.

Listing 2.8.9 Cardinality constraints by binary decision diagrams (bddsum.mzn).
% the sum of booleans x = s
predicate bool_sum_eq(array[int] of var bool:x, int:s) =
     let { int: c = length(x),
           array[1..c] of var bool: y = [x[i] | i in index_set(x)] 
     } in
     rec_bool_sum_eq(y, 1, s);

predicate rec_bool_sum_eq(array[int] of var bool:x, int: f, int:s) =
     let { int: c = length(x) } in
     if s < 0 then false 
     elseif s == 0 then
          forall(i in f..c)(x[i] == false)
     elseif s < c - f + 1 then
          (x[f] == true /\ rec_bool_sum_eq(x,f+1,s-1)) \/
          (x[f] == false /\ rec_bool_sum_eq(x,f+1,s))
     elseif s == c - f + 1 then
          forall(i in f..c)(x[i] == true)
     else false endif;

We can implement bool_sum_eq using binary decision diagrams using the code shown in ex:bddsum. The cardinality constraint is broken into two cases: either the first element x[1] is true, and the sum of the remaining bits is s-1, or x[1] is false and the sum of the remaining bits is s. For efficiency this relies on common subexpression elimination to avoid creating many equivalent constraints.