什么是MiniZinc？

MiniZinc是對(duì)約束優(yōu)化模型進(jìn)行建模的一種語言。

它本身只是一種對(duì)模型的描述，而后續(xù)的求解則依賴于求解器來進(jìn)行。根據(jù)要求解問題的類型不同，它可以調(diào)用不同種類的求解器，例如Constraint Programming (CP) / Mixed Integer Programming / Satisfiability(SAT) Solver，來對(duì)問題進(jìn)行求解。更具體的，MiniZinc兼容的求解器有：Chuffed，CBC，findMUS，Gecode，CPLEX等。

當(dāng)然，除了MiniZinc，我們也可以使用OPL、LINGO、AMPL等語言對(duì)模型進(jìn)行表達(dá)，可以根據(jù)個(gè)人需要進(jìn)行選擇。對(duì)于我來說，MiniZinc對(duì)約束的表達(dá)非常貼近我們的邏輯，同時(shí)還有謂詞(predicate)、全局約束(Global Constraint)等強(qiáng)大的輔助功能，能幫助我們快速建立高效模型。

MiniZinc在Linux，Macos和Windows下都可以使用，在不同系統(tǒng)下的安裝方式可以參考這里。

從一個(gè)簡(jiǎn)單實(shí)例開始

下面我們可以從一個(gè)簡(jiǎn)單的背包問題(Knapsack Problem)看一下MiniZinc模型最基本的組成。

如下圖所示的一個(gè)背包問題，我們有一個(gè)最大負(fù)重為15kg的背包，以及5個(gè)重量與價(jià)值各不相同的物品，我們需要得到一個(gè)最優(yōu)的組合，使得背包里裝的東西在不超重的同時(shí)，有盡可能大的價(jià)值。

1_1 Knapsack.png

對(duì)應(yīng)這個(gè)問題的MiniZinc程序如下：

% 背包問題的模型
%--------------------------
% 數(shù)據(jù)部分
enum ITEMS = {Item1, Item2, Item3, Item4, Item5}; % 枚舉類型，標(biāo)記物品ID
array[ITEMS] of int: weight = [12, 2, 1, 4, 1]; % 數(shù)組，每個(gè)物品的重量
array[ITEMS] of int: value = [4, 2, 1, 10, 2]; % 數(shù)組，每個(gè)物品的價(jià)值
int: MAX_WT = 15; % 背包能容納的最大重量

%--------------------------
% 決策變量
var set of ITEMS: knapsack;

%--------------------------
% 約束: 物品總重量不能超過背包最大重量限制
var int: total_wt = sum(it in knapsack)(weight[it]);
constraint total_wt <= MAX_WT;

%--------------------------
% 目標(biāo)函數(shù)：最大化背包內(nèi)物品的總價(jià)值
var int: total_val = sum(it in knapsack)(value[it]);
solve maximize total_val;

%--------------------------
% 結(jié)果輸出
output ["Picked Items: \(knapsack)\nTotal weight: \(total_wt)\nTotal value: \(total_val)\n"];

可以用MiniZinc IDE求解，也可以在command line中調(diào)用minizinc來進(jìn)行求解。得到的結(jié)果如下：

Picked Items: {Item2, Item3, Item4, Item5}
Total weight: 8
Total value: 15
----------
==========

也就是要我們選擇第2、3、4、5件物品，總共的重量為8，總價(jià)值15。

模型的組成部分

下面我們來逐行進(jìn)行解釋，看一下MiniZinc中模型的組成。MiniZinc的語言組成和C/C++有些相似，在每條語句的最后需要以;標(biāo)示語句的結(jié)束。

注釋

在程序的第一行我們看到了%符號(hào)，它表示本行的后面部分都是注釋，在模型編譯求解時(shí)不作處理。

需要注意的是，MiniZinc中沒有多行注釋，并不能像C/C++中一樣，用/* */來注釋多行。

參數(shù)和變量

我們繼續(xù)看下面一部分的程序：

%--------------------------
% 數(shù)據(jù)部分
enum ITEMS = {Item1, Item2, Item3, Item4, Item5}; % 枚舉類型，標(biāo)記物品ID
array[ITEMS] of int: weight = [12, 2, 1, 4, 1]; % 數(shù)組，每個(gè)物品的重量
array[ITEMS] of int: value = [4, 2, 1, 10, 2]; % 數(shù)組，每個(gè)物品的價(jià)值
int: MAX_WT = 15; % 背包能容納的最大重量

%--------------------------
% 決策變量
var set of ITEMS: knapsack;

和C/C++中類似的，MiniZinc中在命名一個(gè)變量時(shí)也需要給出變量的類型。

第3行的enum指定了一個(gè)枚舉類型，它給出了一個(gè)命名的取值空間，也就是一個(gè)具有有限個(gè)對(duì)象的集合。

第4行的array[idx]給出了向量類型，[idx]給出了向量的下標(biāo)，

第6行的int表示為參數(shù)MAX_WT指定整數(shù)類型，并且為它賦值為15。

第10行給出了當(dāng)前模型的決策變量，不同于一邊變量，對(duì)于決策變量我們無法預(yù)先為它賦值，只有等到求解之后我們才能知道它可以取什么值。但是通常對(duì)于決策變量，我們需要給定其值域(domain)來幫助求解器進(jìn)行搜索，在這個(gè)問題里，我們給出的domain是set of ITEMS也就是ITEMS中任意選取的一個(gè)集合。

在MiniZinc中，基本的數(shù)據(jù)類型有6種：整數(shù)(int)，浮點(diǎn)數(shù)(float)，布爾類型(bool)，字符串(string)，向量(array)和集合(set)。

參數(shù)用關(guān)鍵詞par標(biāo)識(shí)，但是如果給出了數(shù)據(jù)類型，那么par可以省略，也就是說par int: k和int: k是等價(jià)的。

變量用關(guān)鍵詞var標(biāo)識(shí)，我們上面第10行的語句var set of ITEMS: knapsack;生成了一個(gè)名字為knapsack的變量，其類型為set of ITEMS，也就是ITEMS的一個(gè)集合。

參數(shù)和變量的聲明和賦值可以放在一起，也可以分開，例如var int: x = y + 10;和var int: x; x = y + 10;是等價(jià)的。注意在MiniZinc中，對(duì)每個(gè)參數(shù)/變量只能賦值一次，多次賦值會(huì)引起錯(cuò)誤。

此外在MiniZinc中，變量名稱可以由大小寫字母和下劃線組合而成，其他字符和miniZinc的保留關(guān)鍵字、操作符不能作為變量名。

約束

%--------------------------
% 約束: 物品總重量不能超過背包最大重量限制
var int: total_wt = sum(it in knapsack)(weight[it]);
constraint total_wt <= MAX_WT;

約束用constraint關(guān)鍵詞標(biāo)識(shí)。約束中給定的是一系列的布爾類型表達(dá)式(Boolean expression)，來對(duì)模型中變量的取值進(jìn)行限制。

MiniZinc支持的關(guān)系操作符有：

• 等于：=或者==
• 不等：!=
• 小于和小于等于：<和<=
• 大于和大于等于：>和>=

當(dāng)然MiniZinc也支持一系列的邏輯關(guān)系，例如蘊(yùn)含(->)、合取(/\)、析取(\/)等，后面我們?cè)龠M(jìn)行詳細(xì)講解。

另外需要注意的是，MiniZinc中并不支持連續(xù)不等式，所以0<=a<=2是不合法的，而應(yīng)該寫成0<=a /\ a<=2。

目標(biāo)函數(shù)

%--------------------------
% 目標(biāo)函數(shù)：最大化背包內(nèi)物品的總價(jià)值
var int: total_val = sum(it in knapsack)(value[it]);
solve maximize total_val;

在目標(biāo)函數(shù)的部分，我們需要給出一個(gè)求解的目標(biāo)。

通常需要求解的有三種情況：

• 最大化某個(gè)目標(biāo)值：用語句solve maximize <obj_expr>來表示對(duì)表達(dá)式<obj_expr>求最大值。
• 最小化某個(gè)目標(biāo)值：用語句solve minimize <obj_expr>來表示對(duì)表達(dá)式<obj_expr>求最小值。
• 求解滿足約束的情況：用語句solve satisfy來表示求滿足約束的解，此時(shí)我們沒有目標(biāo)函數(shù)。

結(jié)果輸出

%--------------------------
% 結(jié)果輸出
output ["Picked Items: \(knapsack)\nTotal weight: \(total_wt)\nTotal value: \(total_val)\n"];

output [<string_expr>] 可以用來輸出一個(gè)字符串。\和C/C++中一樣是轉(zhuǎn)義符，用\(<variable>)可以輸出變量，\n和\t分別代表換行符和制表符。

此外我們還可以對(duì)輸出進(jìn)行更精確的控制，show(<variable>)和\(<variable>)可以輸出變量的值，而show_int(n, <varibale>)則表示用個(gè)字符輸出整數(shù)<variable>，如果，那么會(huì)向右對(duì)齊，反之則向左對(duì)齊。show_float(n, d, <variable>)表示用個(gè)字符輸出浮點(diǎn)數(shù)<variable>，表示小數(shù)點(diǎn)之后保留的位數(shù)。

對(duì)于長(zhǎng)字符串，可以用++進(jìn)行字符串拼接，例如"This is a string"等同于"This is " ++ "a string"。

在一個(gè)模型中，最多只能有一個(gè)輸出語句。

在不指定輸出語句的情況下，MiniZinc會(huì)輸出所有有聲明，但是沒有被表達(dá)式賦值的變量。因此有些情況下我們也可以利用這個(gè)特性，偷個(gè)懶不用明確給出輸出語句。

解的解讀

在我們得到的解中：

----------表示上面給出的解是問題的一個(gè)可行解。

==========表示上面的解是最優(yōu)解。

默認(rèn)情況下，minizinc在求解優(yōu)化問題時(shí)只會(huì)輸出最優(yōu)解。如果加上參數(shù)-a，則表示輸出所有可行解。如果使用IDE，可以在configuration editor中進(jìn)行設(shè)置。

例如對(duì)于我們的例子：

minizinc 1_1_KnapsackProb.mzn

對(duì)應(yīng)的結(jié)果為：

Picked Items: {Item2, Item3, Item4, Item5}
Total weight: 8
Total value: 15
----------
==========

而

minizinc 1_1_KnapsackProb.mzn -a

對(duì)應(yīng)的結(jié)果為：

Picked Items: {Item1, Item2, Item3}
Total weight: 15
Total value: 7
----------
Picked Items: {Item1, Item2, Item5}
Total weight: 15
Total value: 8
----------
Picked Items: {Item2, Item3, Item4, Item5}
Total weight: 8
Total value: 15
----------
==========

可以看到上面兩個(gè)解是可行解，但并非最優(yōu)解。