优化建模之MiniZinc(三) 全局约束 -- 以解数独为例

数独问题中约束的表达

数独是一个经典的问题，在计算机科学中，我们通常使用回溯法来进行求解，但是对于规模稍大的数独问题，回溯法的设计是相当复杂的。这里我们也可以建立一个数学模型，让求解器帮我们来得到答案。

我们从数独网站上找一个困难级别的题目，如下图所示：

3_1 Sudoku.jpg

根据数独的要求，我们可以归纳出以下约束：

每行和每列中填入1-9的数字，并且保证每行每列中都不出现重复的数字；
每个3x3的小方格中也需要填入1-9的数字，并且填入的数字各不相同；

直接表达的约束

对于第一个约束，一种可行的表达方式是先定义一个辅助数组completed表示填充之后每个位置的数字

forall(i, j in COLS where i < j)(completed[1, i] != completed[1, j])，这样就可以约束第1行中任意两个元素不相等。

依次对第2，3，...，9行进行同样的约束，我们就保证了每一行中不出现重复的数字。

按照同样的思路对列进行约束，这样的话一共我们需要写18条约束语句，才能完成我们上面短短一句自然语言所表达的约束。

这个思路并不难，约束的表达也好理解，唯一的问题就是太过繁琐。我们知道编程中有一个重要的原则叫做DRY，也就是Don't Repeat Yourself。在建模中也是同样，我们是不是能够找到更加简洁的表达上面约束的方式呢？答案当然是可以的，就是利用MiniZinc中的全局约束。

forall(i in ROWS) alldifferent(completed[i, ..]); 就可以替代我们上面的9条语句，表达每行中所有元素不同的约束。这里的alldifferent是MiniZinc中定义的全局约束中的一个。

使用全局约束

模型文件3_1_Sudoku.mzn：

% 建模求解数独问题

%--------------------------
% 数据
int: nrow;
int: ncol;
set of int: rows = 1..nrow;
set of int: cols = 1..ncol;
array[rows, cols] of int: grid; % 用0表示当前棋盘上空的位置

%--------------------------
% 决策变量
array[rows, cols] of var 0..9: fill; % 0表示当前棋盘上已经填充的位置，其他数字表示应该填充的数字
array[rows, cols] of var 1..9: completed; % 建模辅助变量

%--------------------------
% 约束
% 0. 约束fill数组和completed数组的关系
constraint forall(i in rows, j in cols)(completed[i, j] = fill[i, j] + grid[i, j]);
% 1. 保证grid中已经填好数字的位置在fill中为0
constraint forall(i in rows, j in cols)(grid[i, j] != 0 -> fill[i, j] = 0);
% 2. 保证每行都是1-9，每列都是1-9
include "alldifferent.mzn";
constraint forall(i in rows)(alldifferent(completed[i, ..]));
constraint forall(j in cols)(alldifferent(completed[.., j]));
% 3. 保证每个 3x3的小块中放入的都是不同的数字
constraint forall(i in 0..((nrow div 3) - 1), j in 0..((ncol div 3) - 1))
                (alldifferent([completed[3*i + u, 3*j + v] | u in 1..3, v in 1..3]));

%--------------------------
% 目标函数
solve satisfy;

%--------------------------
% 输出
output ["\(completed[i, j])" ++ if ((j mod ncol) = 0) then "\n" else " " endif  |i in rows, j in cols];

数据文件3_1_Sudoku.dzn

nrow = 9;
ncol = 9;
grid = [|0, 0, 3, 6, 0, 0, 0, 0, 7
        |0, 0, 0, 0, 0, 0, 0, 1, 5
        |0, 5, 0, 0, 7, 0, 6, 8, 0
        |0, 0, 9, 8, 0, 0, 0, 0, 0
        |1, 0, 2, 0, 0, 7, 0, 0, 8
        |0, 0, 0, 1, 0, 2, 0, 0, 0
        |0, 4, 0, 0, 0, 0, 0, 0, 0
        |7, 0, 0, 0, 0, 0, 3, 0, 9
        |8, 0, 1, 0, 0, 4, 2, 0, 0|];

我们可以得到填好的数独结果：

9 1 3 6 8 5 4 2 7
6 8 7 4 2 3 9 1 5
2 5 4 9 7 1 6 8 3
4 7 9 8 5 6 1 3 2
1 6 2 3 4 7 5 9 8
5 3 8 1 9 2 7 6 4
3 4 5 2 6 9 8 7 1
7 2 6 5 1 8 3 4 9
8 9 1 7 3 4 2 5 6
----------

全局约束

MiniZinc中的全局约束

MiniZinc中预置了一系列的约束供我们使用。

所谓的”全局约束“，指的是约束本身不限制变量的具体维度，也就是说对于任意大小的变量，只要其类型符合要求，就都可以套用，从这个角度来说，这种约束是”全局“的。例如alldifferent([<set>])，并不会在意传入的set到底维度如何，包含3个变量或者10个变量，都可以进行统一处理。

而从另外一个角度来说，”全局约束“也是在许多问题中会出现的共性的约束，这也是其全局性的一种体现。

”全局约束“其实是预先实现的一些谓词(Predicate)，后面我们更加深入学习时会看到什么叫做谓词以及如何使用谓词。

全局约束的引入 -- include语句

利用语句include "alldifferent.mzn";，可以在模型中导入alldifferent全局约束；用include "globals.mzn"可以在模型中导入所有全局约束。

和C/C++中一样include "<filename>"会在MiniZinc的环境变量中临时添加一条路径，使得程序编译和链接模型时能够在添加的路径中查找相应的文件。

除了添加全局约束以外，我们还可以像C/C++中一样，使用include来将较大的模型化整为零，分成功能单一便于理解和修改的部分。

为什么需要全局约束

为什么需要使用全局约束呢？

可以使得模型的表达更加简洁，容易理解；就像我们上面展示的一样，9条繁琐重复语句可以用一条全局变量进行间接的表达，可读性大大提升。
使用全局约束可能比我们自己表达约束高效得多(即使它们是基于分解来实现的)。这是因为对于全局约束，minizinc对每个求解器会有不同的，量身定做的分解方法。具体需要查看MiniZinc如何对约束进行分解，可以可以运行minizinc -k保留中间文件，来查看模型(FlatZinc文件格式，后缀名为.fzn)中具体的约束语句。

常用的全局约束

下面列出了一些建模中常用的全局约束，更多的全局约束可以参考MiniZinc的reference manual，当然在后面的系列文章里我们也会接触到更多的全局约束。

global_cardinality(array [$X] of var int: x, array [$Y] of int: cover, array [$Y] of var int: counts) -- 要求x中出现cover[i]的次数为counts[i]。例如global_cardinality([1, 2, 2, 3], [2, 3], [2, 2])就会返回False，因为要求元素3在x中出现2次，但是实际上x中只包含一个3。
all_disjoint(array [$X] of var set of int: S) -- 要求S中所有集合都不相交。
nvalue(var int: n, array [$X] of var int: x) -- 要求x中出现的不同元素个数有n个，对于我们数独这个案例来说，我们也可以用这条全局约束，要求每行每列都有9个不同的元素。
inverse(array [int] of var int: f, array [int] of var int: invf -- 要求f和invf是一对互逆的映射，也就是说f[i] = j <=> invf[j] = i，这在dual model combining 中非常有用，可以大幅提高模型的求解效率，后面在讲multi modelling时肯定绕不开这个全局约束。