使用 minizinc 解决的各种问题

Question

我正在尝试使用 minizinc 为我构建一个真/假矩阵，其中每一列都满足某些条件（至少 3 个真值，并且必须有奇数个真值）。到目前为止，一切都很好 - 但是当我添加额外的约束以使每一列都不同（与所有其他列）时，我没有得到一致的结果：

使用下面注释掉的版本，在 Ubuntu-on-WSL (Windows) 上使用 minizinc 2.1.7，它几乎可以立即找到解决方案。但是，Mac 或 ArchLinux 安装上的任何版本的 minizinc（2.1.7、2.2.0、2.3.1）都不能满足这些限制（至少在几分钟内）。这一切都与 Gecode 相关。

Chuffed 可以很好地满足约束条件，同样是注释掉的代码版本，而不是下面的代码。

但是，如果我解决以最小化某些值（参见第二个 sn-p），那么 Chuffed 将不再找到任何解决方案（同样，至少在几分钟内不会）。我原以为它至少会找到与“满足”相同的解决方案。

我做错了什么？是否有更好的方法来编写更一致的“不同列”约束？我不认为这对于约束求解器来说是一个特别困难的问题，所以我怀疑这确实是我如何编写约束的问题。

我想将 H 矩阵保留为真/假的 2d 矩阵，因为具有该形状还有其他约束。

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;

Answer 1

这是模型的重写版本。由Chuffed在43s内解决，最佳解决方案见下文。

h_t 被保留，因为它似乎使用all_different 约束更好地“驱动”解决方案。 lex2 约束是一个对称破坏约束，它确保矩阵 H 应按字典顺序排列。

此外，还重写了一些其他约束，例如当 sum .. (H[i,j]) 足够时，在某些约束中删除了 sum ... ( if H[i.j] then 1 else 0 endif)。

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
];

使用以下命令在43s后找到最优解 $ 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
 ----------
 ==========

其他一些cmets：

• 所有列都应该不同的约束可以通过以下方式说明

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

  但是，它不如all_different 变体高效（在此模型中）。

• 当求解器看起来很慢时，一个提示是测试不同的搜索策略。当我开始使用模型时，这里似乎有点快：

  solve :: int_search(H_t, first_fail, indomain_split, complete) 最小化z；

  但是当添加lex2 约束时，它比普通的solve minimize z 慢。 使用搜索策略通常是一件好事......