優(yōu)化建模之MiniZinc(一) MiniZinc模型的基本組成

什么是MiniZinc？

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

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

當然喳张，除了MiniZinc续镇，我們也可以使用OPL、LINGO销部、AMPL等語言對模型進行表達摸航，可以根據(jù)個人需要進行選擇。對于我來說舅桩，MiniZinc對約束的表達非常貼近我們的邏輯酱虎，同時還有謂詞(predicate)、全局約束(Global Constraint)等強大的輔助功能擂涛，能幫助我們快速建立高效模型读串。

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

從一個簡單實例開始

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

如下圖所示的一個背包問題狰右，我們有一個最大負重為15kg的背包杰捂，以及5個重量與價值各不相同的物品，我們需要得到一個最優(yōu)的組合棋蚌，使得背包里裝的東西在不超重的同時嫁佳，有盡可能大的價值。

1_1 Knapsack.png

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

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

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

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

%--------------------------
% 目標函數(shù)：最大化背包內(nèi)物品的總價值
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來進行求解瓤漏。得到的結(jié)果如下：

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

也就是要我們選擇第2、3、4蔬充、5件物品俯在，總共的重量為8，總價值15娃惯。

模型的組成部分

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

注釋

在程序的第一行我們看到了%符號馒稍，它表示本行的后面部分都是注釋皿哨，在模型編譯求解時不作處理。

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

參數(shù)和變量

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

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

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

和C/C++中類似的崔步，MiniZinc中在命名一個變量時也需要給出變量的類型。

第3行的enum指定了一個枚舉類型缎谷，它給出了一個命名的取值空間井濒，也就是一個具有有限個對象的集合。

第4行的array[idx]給出了向量類型列林，[idx]給出了向量的下標瑞你，

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

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

在MiniZinc中舶赔，基本的數(shù)據(jù)類型有6種：整數(shù)(int)扫倡，浮點數(shù)(float)，布爾類型(bool)，字符串(string)撵溃，向量(array)和集合(set)疚鲤。

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

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

參數(shù)和變量的聲明和賦值可以放在一起姑蓝，也可以分開，例如var int: x = y + 10;和var int: x; x = y + 10;是等價的吕粗。注意在MiniZinc中纺荧，對每個參數(shù)/變量只能賦值一次，多次賦值會引起錯誤颅筋。

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

約束

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

約束用constraint關(guān)鍵詞標識。約束中給定的是一系列的布爾類型表達式(Boolean expression)肢簿，來對模型中變量的取值進行限制靶剑。

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

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

當然MiniZinc也支持一系列的邏輯關(guān)系，例如蘊含(->)池充、合取(/\)桩引、析取(\/)等，后面我們再進行詳細講解收夸。

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

目標函數(shù)

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

在目標函數(shù)的部分，我們需要給出一個求解的目標咽瓷。

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

最大化某個目標值：用語句solve maximize <obj_expr>來表示對表達式<obj_expr>求最大值设凹。
最小化某個目標值：用語句solve minimize <obj_expr>來表示對表達式<obj_expr>求最小值。
求解滿足約束的情況：用語句solve satisfy來表示求滿足約束的解茅姜，此時我們沒有目標函數(shù)闪朱。

結(jié)果輸出

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

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

此外我們還可以對輸出進行更精確的控制，show(<variable>)和\(<variable>)可以輸出變量的值称诗，而show_int(n, <varibale>)則表示用 $|n|$ 個字符輸出整數(shù)<variable>萍悴，如果 $n>0$ ，那么會向右對齊寓免，反之則向左對齊退腥。show_float(n, d, <variable>)表示用 $|n|$ 個字符輸出浮點數(shù)<variable>， $d$ 表示小數(shù)點之后保留的位數(shù)再榄。

對于長字符串，可以用++進行字符串拼接享潜，例如"This is a string"等同于"This is " ++ "a string"困鸥。

在一個模型中，最多只能有一個輸出語句剑按。

在不指定輸出語句的情況下疾就，MiniZinc會輸出所有有聲明，但是沒有被表達式賦值的變量艺蝴。因此有些情況下我們也可以利用這個特性猬腰，偷個懶不用明確給出輸出語句。

解的解讀

在我們得到的解中：

----------表示上面給出的解是問題的一個可行解猜敢。

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

默認情況下，minizinc在求解優(yōu)化問題時只會輸出最優(yōu)解缩擂。如果加上參數(shù)-a鼠冕，則表示輸出所有可行解。如果使用IDE胯盯，可以在configuration editor中進行設(shè)置懈费。

例如對于我們的例子：

minizinc 1_1_KnapsackProb.mzn

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

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

而

minizinc 1_1_KnapsackProb.mzn -a