various problems getting a solution with minizinc

Question

I am trying to use minizinc to build me a matrix of true/false, where each column satisfies certain conditions (at least 3 true values, and there must be an odd number of true values). So far, so good - but when I add additional constraints to make it so that each column is different (from all other columns), I don't get consistent results:

With the commented out version below, with minizinc 2.1.7 on Ubuntu-on-WSL (Windows), it finds a solution pretty much immediately. However, any version of minizinc (2.1.7, 2.2.0, 2.3.1) on either a Mac, or on an ArchLinux install, can't satisfy the constraints (at least not within a few minutes). All of this is with Gecode.

Chuffed works fine to satisfy the constraints, again with the commented-out version of the code rather than the one below.

However, if I solve to minimize certain values (see second snippet), then Chuffed doesn't find any solution anymore (again, at least not within a few minutes). I would have expected it to at least find the same solution as it finds for "satisfy".

What am I doing wrong? Are there better ways of writing the constraint of "distinct columns" that works more consistently? I wouldn't think this is a particular hard problem for a constraint solver, so I suspect it's really an issue with how I've written the constraints.

I would like to keep the H matrix as a 2d matrix of true/false, as there's other constraints that benefit from having it in that shape.

int: k = 7;
int: n = 47;

array[1..k,1..n] of var bool: H;
array[1..k] of var bool : flip_bits;



predicate all_different_int(array[int] of var int: x) =
  forall(i,j in index_set(x) where i < j) ( x[i] != x[j] );


constraint forall(j in 1..n)(
  sum(i in 1..k)(
    if H[i,j] then 1 else 0 endif
  ) mod 2 > 0
);

constraint forall(j in 1..n)(
  sum(i in 1..k)(
    if H[i,j] then 1 else 0 endif
  ) >= 3
);

%array[1..n] of var int: H_t;
%constraint forall(j in 1..n)(
% H_t[j] = sum(i in 1..k)(
%   if H[i,j] then pow(2,i) else 0 endif
% )
%);
%constraint all_different_int(H_t);

constraint all_different_int(
  [sum(i in 1..k)(if H[i,j] then pow(2,i) else 0 endif) | j in 1..n]
);

solve satisfy;

var int: z2 = sum(i in 1..k, j in 1..n)(if H[i,j] then 1 else 0 endif);
var int: z1 = max(i in 1..k)(sum (j in 1..n)(if H[i,j] then 1 else 0 endif));

solve minimize z1*1000+z2;

To enforce an odd number of bool values, you might want to use xorall(). This should be much more efficient than mod 2. — Axel Kemper
@AxelKemper thanks - I had used xorall() in later constraints but didn't think of using it there. That indeed helped a lot in getting it to solve again with gecode. Still curious about other/better ways to write the column uniqueness, though. — Alex Hornung

hakank hakank · Accepted Answer · 2019-07-13T06:32:14

Here is a rewritten version of the model. It is solved by Chuffed in 43s, see below for an optimal solution.

The h_t is kept since it seems to "drive" the solution better using the all_different constraint. The lex2 constraint is a symmetry breaking constraint which ensure that the matrix H should be lexicographically ordered.

Also, some other constraints where rewritten as well, e.g. removed sum ... ( if H[i.j] then 1 else 0 endif) in some constraints when just sum .. (H[i,j]) was sufficient.

include "globals.mzn";

int: k = 7;
int: n = 47;

array[1..k,1..n] of var bool: H;
array[1..k] of var bool : flip_bits;

constraint forall(j in 1..n)(
    sum(i in 1..k)(H[i,j]) mod 2  = 1);

constraint forall(j in 1..n)(
     sum(i in 1..k)(H[i,j]) >= 3);

array[1..n] of var int: H_t;
constraint 
  forall(j in 1..n)(
    H_t[j] = sum(i in 1..k)(
      if H[i,j] then pow(2,i) else 0 endif
    )
  );
constraint all_different_int(H_t);

var int: z2 = sum(i in 1..k, j in 1..n)(H[i,j]);
var int: z1 = max(i in 1..k)(sum (j in 1..n)(H[i,j]));

constraint
  z1 > 0 /\ z2 > 0 /\  z > 0
;

% symmetry breaking
constraint lex2(H); 

var int: z = z1*1000+z2;

% solve :: int_search(H_t, first_fail, indomain_split, complete) minimize z;
% solve satisfy;
solve minimize z;

output [
  "z: \(z)\n",
  % "H: \(H)\n",
  "H_t: \(H_t)\n"
]
++
[
 if j = 1 then "\n" else "" endif++
   "\(H[i,j]*1)"

   | i in 1..k, j in 1..n
];

The optimal solution is found after 43s using the following command $ time minizinc test96.mzn -a -s --solver chuffed

 z: 24165
 H_t: [224, 208, 176, 112, 200, 168, 104, 152, 88, 56, 248, 196, 164, 100, 148, 84, 52, 140, 76, 44, 236, 28, 124, 194, 162, 98, 146, 82, 50, 242, 138, 74, 42, 234, 26, 218, 134, 70, 38, 230, 22, 182, 118, 14, 158, 94, 62]

 00000000000000000000000111111111111111111111111
 00000000000111111111111000000000000011111111111
 00001111111000000111111000000011111100000001111
 01110001111000111000011000111100001100001110111
 10110110011011001001101011001100110000110110001
 11011010101101010010101101010101010101010010010
 11101101001110100100100110100110010110010100100
 ----------
 ==========

Some other comments:

The constraint that all columns should be different can be stated by the following

constraint forall(j in 2..n) ( sum(i in 1..k) ( H[i,j] != H[i,j-1]) > 0 ) ;

but, it's not as efficient (in this model) as the all_different variant.
When a solver seems to be slow, a tip is to test different search strategies. Here's one that seems to be a bit faster when I started to play with the model:

solve :: int_search(H_t, first_fail, indomain_split, complete) minimize z;

But when adding the lex2 constraint it was slower than a plain solve minimize z. It is often a good thing to play with the search strategies...

various problems getting a solution with minizinc

1 Answers