关于添加哪些约束来优化 Minizinc 模型的建议

Question

我最近开始使用 Minizinc 来解决这个简单的问题：

问题定义：

我有布尔变量维度 H 和 W 的网格。唯一的限制是，如果一个变量为假，则至少有一个相邻变量（上、右、左、下、对角线不算）必须为真。目标是最小化网格中真实值的数量。

我的代码：

include "globals.mzn";

int: H = 20;
int: W = 20;
array[1..H, 1..W] of var bool: grid;

% Objective
var int: totsum = sum(i in 1..H, j in 1..W)(grid[i, j]);

% If a variable is false then at least one of the adjacent ones must be true
constraint forall(i in 1..H, j in 1..W)(not(grid[i, j]) -> grid[max(1, i-1), j] \/ grid[min(i+1, H), j] \/ grid[i, max(1, j-1)] \/ grid[i, min(W, j+1)]);

% If a variable is true then there must be at least 1 false variable
constraint forall(i in 1..H, j in 1..W)(grid[i, j] -> not(grid[max(1, i-1), j] /\ grid[min(i+1, H), j] /\ grid[i, max(1, j-1)] /\ grid[i, min(W, j+1)]));

% Implied constraint: the sum of trues along the rows must be less than the length of the row since no optimal solution should display this behavior
constraint forall(i in 1..H)(sum(row(grid, i)) < H);

% Same for columns
constraint forall(j in 1..W)(sum(col(grid, j)) < W);

% It is not possible to have 3x3 patches of equal values
constraint forall(i in 1..H-2, j in 1..W-2)(not(all_equal(a in i..i+2, b in j..j+2)(grid[a, b])));

% Symmetric rows (1 and H, 2 and H-1 etc...) ordering to break symmetry
constraint symmetry_breaking_constraint(forall(i in 1..(H div 2))(lex_lesseq(row(grid, i), row(grid, H+1-i))));

% Same for columns
constraint symmetry_breaking_constraint(forall(j in 1..(W div 2))(lex_lesseq(col(grid, j), col(grid, W+1-j))));

% Trivial upper bound: This is the case where the grid has alternating columns of true and false
constraint totsum < H*(W div 2 + 1);

solve :: bool_search(grid, input_order, indomain_min, complete) minimize totsum;

我的代码可以工作，但是当 H 和 W 都大于 20 时，它会变得非常慢。因为我想解决 H=32 和 W=32 的问题，所以这是不可行的。我尝试运行 1 小时，但 Minizinc 无法找到最佳解决方案。我正在使用 OR-TOOLS 解算器。

我想过要在模型中添加什么来提高速度，我唯一能想到的就是添加对角对称破缺；在正方形上找到对角线是微不足道的，但我真的不知道如何在一般情况下计算它。

有什么改进我的模型的建议吗？非常感谢你

Answer 1

通过以下精简代码，我得到了

totsum 232

的中间结果

H = W = 32

。
求解器是OR Tools或CPLEX，两者都有8个线程。运行时间是几分钟。

include "globals.mzn";

int: H = 32;
int: W = 32;
set of int: OuterRows = 0..H+1;
set of int: Rows = 1..H;
set of int: OuterCols = 0..W+1;
set of int: Cols = 1..W;

array[OuterRows, OuterCols] of var bool: grid;

% Objective
var 1 .. ((H*W) div 4): totsum = sum(i in Rows, j in Cols)(grid[i, j]);

% outer grid frame is false
% it helps to avoid case distinctions
constraint forall(i in OuterRows, j in {0, W+1})
  (not grid[i, j]);
constraint forall(i in {0, H+1}, j in OuterCols)
  (not grid[i, j]);

% If a variable is false then at least one of the adjacent ones must be true
constraint forall(i in Rows, j in Cols)
  (not(grid[i, j]) -> grid[i-1, j] \/ grid[i+1, j] \/ grid[i, j-1] \/ grid[i, j+1]);

solve minimize totsum;

function string: g(Rows: i, Cols: j) =
  if fix(grid[i, j]) then " T " else " - " endif;
  
output ["\n\ntotsum \(totsum)\n\n"] 
++ ["    "] ++ [ format(2, j) ++ " " | j in Cols ]
++ [ if j == 1 then "\n" ++ format(2, i) ++ ": " else "" endif ++ g(i, j) | i in Rows, j in Cols ];