什么是MiniZinc？
MiniZinc是对约束优化模型进行建模的一种语言。
它本身只是一种对模型的描述，而后续的求解则依赖于求解器来进行。根据要求解问题的类型不同，它可以调用不同种类的求解器，例如Constraint Programming (CP) / Mixed Integer Programming / Satisfiability(SAT) Solver，来对问题进行求解。更具体的，MiniZinc兼容的求解器有：Chuffed，CBC，findMUS，Gecode，CPLEX等。
当然，除了MiniZinc，我们也可以使用OPL、LINGO、AMPL等语言对模型进行表达，可以根据个人需要进行选择。对于我来说，MiniZinc对约束的表达非常贴近我们的逻辑，同时还有谓词(predicate)、全局约束(Global Constraint)等强大的辅助功能，能帮助我们快速建立高效模型。
MiniZinc在Linux，Macos和Windows下都可以使用，在不同系统下的安装方式可以参考这里。
从一个简单实例开始
下面我们可以从一个简单的背包问题(Knapsack Problem)看一下MiniZinc模型最基本的组成。
如下图所示的一个背包问题，我们有一个最大负重为15kg的背包，以及5个重量与价值各不相同的物品，我们需要得到一个最优的组合，使得背包里装的东西在不超重的同时，有尽可能大的价值。
1_1 Knapsack.png
对应这个问题的MiniZinc程序如下：
% 背包问题的模型
%--------------------------
% 数据部分
enum ITEMS = {Item1, Item2, Item3, Item4, Item5}; % 枚举类型，标记物品ID
array[ITEMS] of int: weight = [12, 2, 1, 4, 1]; % 数组，每个物品的重量
array[ITEMS] of int: value = [4, 2, 1, 10, 2]; % 数组，每个物品的价值
int: MAX_WT = 15; % 背包能容纳的最大重量
%--------------------------
% 决策变量
var set of ITEMS: knapsack;
%--------------------------
% 约束: 物品总重量不能超过背包最大重量限制
var int: total_wt = sum(it in knapsack)(weight[it]);
constraint total_wt <= MAX_WT;
%--------------------------
% 目标函数：最大化背包内物品的总价值
var int: total_val = sum(it in knapsack)(value[it]);
solve maximize total_val;
%--------------------------
% 结果输出
output ["Picked Items: \(knapsack)\nTotal weight: \(total_wt)\nTotal value: \(total_val)\n"];
可以用MiniZinc IDE求解，也可以在command line中调用minizinc来进行求解。得到的结果如下：
Picked Items: {Item2, Item3, Item4, Item5}
Total weight: 8
Total value: 15
----------
==========
也就是要我们选择第2、3、4、5件物品，总共的重量为8，总价值15。
模型的组成部分
下面我们来逐行进行解释，看一下MiniZinc中模型的组成。MiniZinc的语言组成和C/C++有些相似，在每条语句的最后需要以;标示语句的结束。
注释
在程序的第一行我们看到了%符号，它表示本行的后面部分都是注释，在模型编译求解时不作处理。
需要注意的是，MiniZinc中没有多行注释，并不能像C/C++中一样，用/* */来注释多行。
参数和变量
我们继续看下面一部分的程序：
%--------------------------
% 数据部分
enum ITEMS = {Item1, Item2, Item3, Item4, Item5}; % 枚举类型，标记物品ID
array[ITEMS] of int: weight = [12, 2, 1, 4, 1]; % 数组，每个物品的重量
array[ITEMS] of int: value = [4, 2, 1, 10, 2]; % 数组，每个物品的价值
int: MAX_WT = 15; % 背包能容纳的最大重量
%--------------------------
% 决策变量
var set of ITEMS: knapsack;
和C/C++中类似的，MiniZinc中在命名一个变量时也需要给出变量的类型。
第3行的enum指定了一个枚举类型，它给出了一个命名的取值空间，也就是一个具有有限个对象的集合。
第4行的array[idx]给出了向量类型，[idx]给出了向量的下标，
第6行的int表示为参数MAX_WT指定整数类型，并且为它赋值为15。
第10行给出了当前模型的决策变量，不同于一边变量，对于决策变量我们无法预先为它赋值，只有等到求解之后我们才能知道它可以取什么值。但是通常对于决策变量，我们需要给定其值域(domain)来帮助求解器进行搜索，在这个问题里，我们给出的domain是set of ITEMS也就是ITEMS中任意选取的一个集合。
在MiniZinc中，基本的数据类型有6种：整数(int)，浮点数(float)，布尔类型(bool)，字符串(string)，向量(array)和集合(set)。
参数用关键词par标识，但是如果给出了数据类型，那么par可以省略，也就是说par int: k和int: k是等价的。
变量用关键词var标识，我们上面第10行的语句var set of ITEMS: knapsack;生成了一个名字为knapsack的变量，其类型为set of ITEMS，也就是ITEMS的一个集合。
参数和变量的声明和赋值可以放在一起，也可以分开，例如var int: x = y + 10;和var int: x; x = y + 10;是等价的。注意在MiniZinc中，对每个参数/变量只能赋值一次，多次赋值会引起错误。
此外在MiniZinc中，变量名称可以由大小写字母和下划线组合而成，其他字符和miniZinc的保留关键字、操作符不能作为变量名。
约束
%--------------------------
% 约束: 物品总重量不能超过背包最大重量限制
var int: total_wt = sum(it in knapsack)(weight[it]);
constraint total_wt <= MAX_WT;
约束用constraint关键词标识。约束中给定的是一系列的布尔类型表达式(Boolean expression)，来对模型中变量的取值进行限制。
MiniZinc支持的关系操作符有：
- 等于：
=或者== - 不等：
!= - 小于和小于等于：
<和<= - 大于和大于等于：
>和>=
当然MiniZinc也支持一系列的逻辑关系，例如蕴含(->)、合取(/\)、析取(\/)等，后面我们再进行详细讲解。
另外需要注意的是，MiniZinc中并不支持连续不等式，所以0<=a<=2是不合法的，而应该写成0<=a /\ a<=2。
目标函数
%--------------------------
% 目标函数：最大化背包内物品的总价值
var int: total_val = sum(it in knapsack)(value[it]);
solve maximize total_val;
在目标函数的部分，我们需要给出一个求解的目标。
通常需要求解的有三种情况：
- 最大化某个目标值：用语句
solve maximize <obj_expr>来表示对表达式<obj_expr>求最大值。 - 最小化某个目标值：用语句
solve minimize <obj_expr>来表示对表达式<obj_expr>求最小值。 - 求解满足约束的情况：用语句
solve satisfy来表示求满足约束的解，此时我们没有目标函数。
结果输出
%--------------------------
% 结果输出
output ["Picked Items: \(knapsack)\nTotal weight: \(total_wt)\nTotal value: \(total_val)\n"];
output [<string_expr>] 可以用来输出一个字符串。\和C/C++中一样是转义符，用\(<variable>)可以输出变量，\n和\t分别代表换行符和制表符。
此外我们还可以对输出进行更精确的控制，show(<variable>)和\(<variable>)可以输出变量的值，而show_int(n, <varibale>)则表示用个字符输出整数
<variable>，如果，那么会向右对齐，反之则向左对齐。
show_float(n, d, <variable>)表示用个字符输出浮点数
<variable>，表示小数点之后保留的位数。
对于长字符串，可以用++进行字符串拼接，例如"This is a string"等同于"This is " ++ "a string"。
在一个模型中，最多只能有一个输出语句。
在不指定输出语句的情况下，MiniZinc会输出所有有声明，但是没有被表达式赋值的变量。因此有些情况下我们也可以利用这个特性，偷个懒不用明确给出输出语句。
解的解读
在我们得到的解中：
----------表示上面给出的解是问题的一个可行解。
==========表示上面的解是最优解。
默认情况下，minizinc在求解优化问题时只会输出最优解。如果加上参数-a，则表示输出所有可行解。如果使用IDE，可以在configuration editor中进行设置。
例如对于我们的例子：
minizinc 1_1_KnapsackProb.mzn
对应的结果为：
Picked Items: {Item2, Item3, Item4, Item5}
Total weight: 8
Total value: 15
----------
==========
而
minizinc 1_1_KnapsackProb.mzn -a
对应的结果为：
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
----------
==========
可以看到上面两个解是可行解，但并非最优解。
网友评论