數(shù)獨問題中約束的表達
數(shù)獨是一個經(jīng)典的問題，在計算機科學中，我們通常使用回溯法來進行求解，但是對于規(guī)模稍大的數(shù)獨問題，回溯法的設計是相當復雜的。這里我們也可以建立一個數(shù)學模型，讓求解器幫我們來得到答案。
我們從數(shù)獨網(wǎng)站上找一個困難級別的題目，如下圖所示：
根據(jù)數(shù)獨的要求，我們可以歸納出以下約束：
- 每行和每列中填入1-9的數(shù)字，并且保證每行每列中都不出現(xiàn)重復的數(shù)字；
- 每個3x3的小方格中也需要填入1-9的數(shù)字，并且填入的數(shù)字各不相同；
直接表達的約束
對于第一個約束，一種可行的表達方式是先定義一個輔助數(shù)組completed表示填充之后每個位置的數(shù)字
forall(i, j in COLS where i < j)(completed[1, i] != completed[1, j])，這樣就可以約束第1行中任意兩個元素不相等。
依次對第2，3，...，9行進行同樣的約束，我們就保證了每一行中不出現(xiàn)重復的數(shù)字。
按照同樣的思路對列進行約束，這樣的話一共我們需要寫18條約束語句，才能完成我們上面短短一句自然語言所表達的約束。
這個思路并不難，約束的表達也好理解，唯一的問題就是太過繁瑣。我們知道編程中有一個重要的原則叫做DRY，也就是Don't Repeat Yourself。在建模中也是同樣，我們是不是能夠找到更加簡潔的表達上面約束的方式呢？答案當然是可以的，就是利用MiniZinc中的全局約束。
forall(i in ROWS) alldifferent(completed[i, ..]); 就可以替代我們上面的9條語句，表達每行中所有元素不同的約束。這里的alldifferent是MiniZinc中定義的全局約束中的一個。
使用全局約束
模型文件3_1_Sudoku.mzn：
% 建模求解數(shù)獨問題
%--------------------------
% 數(shù)據(jù)
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表示當前棋盤上已經(jīng)填充的位置，其他數(shù)字表示應該填充的數(shù)字
array[rows, cols] of var 1..9: completed; % 建模輔助變量
%--------------------------
% 約束
% 0. 約束fill數(shù)組和completed數(shù)組的關(guān)系
constraint forall(i in rows, j in cols)(completed[i, j] = fill[i, j] + grid[i, j]);
% 1. 保證grid中已經(jīng)填好數(shù)字的位置在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的小塊中放入的都是不同的數(shù)字
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]));
%--------------------------
% 目標函數(shù)
solve satisfy;
%--------------------------
% 輸出
output ["\(completed[i, j])" ++ if ((j mod ncol) = 0) then "\n" else " " endif |i in rows, j in cols];
數(shù)據(jù)文件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|];
我們可以得到填好的數(shù)獨結(jié)果：
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個變量，都可以進行統(tǒng)一處理。
而從另外一個角度來說，”全局約束“也是在許多問題中會出現(xiàn)的共性的約束，這也是其全局性的一種體現(xiàn)。
”全局約束“其實是預先實現(xiàn)的一些謂詞(Predicate)，后面我們更加深入學習時會看到什么叫做謂詞以及如何使用謂詞。
全局約束的引入 -- include語句
利用語句include "alldifferent.mzn";，可以在模型中導入alldifferent全局約束；用include "globals.mzn"可以在模型中導入所有全局約束。
和C/C++中一樣include "<filename>"會在MiniZinc的環(huán)境變量中臨時添加一條路徑，使得程序編譯和鏈接模型時能夠在添加的路徑中查找相應的文件。
除了添加全局約束以外，我們還可以像C/C++中一樣，使用include來將較大的模型化整為零，分成功能單一便于理解和修改的部分。
為什么需要全局約束
為什么需要使用全局約束呢？
- 可以使得模型的表達更加簡潔，容易理解；就像我們上面展示的一樣，9條繁瑣重復語句可以用一條全局變量進行間接的表達，可讀性大大提升。
- 使用全局約束可能比我們自己表達約束高效得多(即使它們是基于分解來實現(xiàn)的)。這是因為對于全局約束，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中出現(xiàn)cover[i]的次數(shù)為counts[i]。例如global_cardinality([1, 2, 2, 3], [2, 3], [2, 2])就會返回False，因為要求元素3在x中出現(xiàn)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中出現(xiàn)的不同元素個數(shù)有n個，對于我們數(shù)獨這個案例來說，我們也可以用這條全局約束，要求每行每列都有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時肯定繞不開這個全局約束。
