2.1. MiniZinc基本模型

2.1.1. 第一个实例

作为我们的第一个例子，假设我们要去给 Fig. 2.1.1 中的澳大利亚地图涂色。 它包含了七个不同的州和地区，而每一块都要被涂一个颜色来保证相邻的区域有不同的颜色。

 1% 用nc个颜色来涂澳大利亚
 2int: nc = 3;
 3
 4var 1..nc: wa;   var 1..nc: nt;  var 1..nc: sa;   var 1..nc: q;
 5var 1..nc: nsw;  var 1..nc: v;   var 1..nc: t;
 6
 7constraint wa != nt;
 8constraint wa != sa;
 9constraint nt != sa;
10constraint nt != q;
11constraint sa != q;
12constraint sa != nsw;
13constraint sa != v;
14constraint q != nsw;
15constraint nsw != v;
16solve satisfy;
17
18output ["wa=\(wa)\t nt=\(nt)\t sa=\(sa)\n",
19        "q=\(q)\t nsw=\(nsw)\t v=\(v)\n",
20         "t=", show(t),  "\n"];

我们可以很容易的用MiniZinc给此问题建模。此模型在 Listing 2.1.1 中给出。

模型中的第一行是注释。注释开始于 % 来表明此行剩下的部分是注释。 MiniZinc同时也含有C语言风格的由 /* 开始和 */ 结束的块注释。

模型中的下一部分声明了模型中的变量。 此行

int: nc = 3;

定义了一个问题的 参数 来代表可用的颜色个数。 在很多编程语言中，参数和变量是类似的。它们必须被声明并且指定一个类型 type。 在此例中，类型是 int。 通过 赋值，它们被设了值。 MiniZinc允许变量声明时被赋值（就像上面那一行）或者单独给出一个赋值语句。 因此下面的表示跟上面的只一行表示是相等的

int: nc;
nc = 3;

和很多编程语言中的变量不一样的是，这里的参数只可以被赋 唯一 的值。 如果一个参数出现在了多于一个的赋值中，就会出现错误。

基本的 参数类型 包括 整型 (int)， 浮点型(float)， 布尔型 (bool) 以及 字符串型 (string)。 同时也支持数组和集合。

MiniZinc模型同时也可能包含另一种类型的变量 决策变量 。 决策变量 是数学的或者逻辑的变量。 和一般的编程语言中的参数和变量不同，建模者不需要给决策变量一个值。 而是在开始时，一个决策变量的值是不知道的。只有当MiniZinc模型被执行的时候， 求解系统才来决定决策变量是否可以被赋值从而满足模型中的约束。若满足，则被赋值。

在我们的模型例子中，我们给每一个区域一个 决策变量 wa, nt, sa, q, nsw, v 和 t。 它们代表了会被用来填充区域的（未知）颜色。

对于每一个决策变量，我们需要给出变量可能的取值集合。这个被称为变量的 定义域 。 定义域部分可以在 变量声明 的时候同时给出， 这时决策变量的 类型 就会从定义域中的数值的类型推断出。

MiniZinc中的决策变量的类型可以为布尔型，整型，浮点型或者集合。 同时也可以是元素为决策变量的数组。 在我们的MiniZinc模型例子中，我们使用整型去给不用的颜色建模。通过使用 var 声明， 我们的每一个决策变量 被声明为定义域为一个整数类型的范围表示 1..nc ， 来表明集合 \(\{ 1, 2, \dots, nc \}\) 。 所有数值的类型为整型，所以模型中的所有的变量是整型决策变量。

MiniZinc仔细地区别了以下两种模型变量：参数和决策变量。利用决策变量创建的表达式类型比利用参数可以创建的表达式类型更局限。 但是，在任何可以用决策变量的地方，同类型的参数变量也可以被应用。

int : <变量名>
<l> .. <u> : <变量名>

var int : <变量名>
var <l>..<u> : <变量名>

参数和决策变量形式上的区别在于对变量的 实例化。 变量的实例化和类型的结合被叫为 类型-实例化 。 既然你已经开始使用MiniZinc，毫无疑问的你会看到很多 类型-实例化 的错误例子。

模型的下一部分是 约束 。 它们详细说明了决策变量想要组成一个模型的有效解必须要满足的布尔型表达式。 在这个例子中我们有一些决策变量之间的不等式。它们规定如果两个区域是相邻的，则它们必须有不同的颜色。

模型中的下一行：

solve satisfy;

表明了它是什么类型的问题。 在这个例子中，它是一个 满足 问题： 我们希望给决策变量找到一个值使得约束被满足，但具体是哪一个值却没有所谓。

模型的最后一个部分是 输出 语句。它告诉MiniZinc当模型被运行并且找到一个解 解 的时候， 要输出什么。

"Invalid datafile: Amount of flour is non-negative"

"Invalid datafile: " ++
"Amount of flour is non-negative"

我们可以通过点击MiniZinc IDE中的 Run 按钮,或者输入

$ minizinc --solver Gecode aust.mzn

来评估我们的模型。 其中 aust.mzn 是包含我们的MiniZinc模型的文件名字。 我们必须使用文件扩展名 .mzn 来表明一个MiniZinc模型。 带有 --solver Gecode 选项的命令 minizinc 使用Gecode有限域求解器去评估我们的模型。如果你使用的是MiniZinc二进制发布,这个求解器实际上是预设的,所以你也可以运行 minizinc aust.mzn 。

当我们运行上面的命令后，我们得到如下的结果：

wa=2   nt=3  sa=1
q=2  nsw=3   v=2
t=1
----------

10个破折号 ---------- 这行是自动被MiniZinc输出的，用来表明一个解已经被找到。

2.1.2. 算术优化实例

我们的第二个例子来自于要为了本地的校园游乐会烤一些蛋糕的需求。 我们知道如何制作两种蛋糕。 footnote{警告: 请不要在家里使用这些配方制作} 一个香蕉蛋糕的制作需要250克自发酵的面粉，2个捣碎的香蕉，75克糖和100克黄油。 一个巧克力蛋糕的制作需要200克自发酵的面粉，75克可可粉，150克糖和150克黄油。 一个巧克力蛋糕可以卖$4.50，一个香蕉蛋糕可以卖$4.00。我们一共有4千克的自发酵面粉， 6个香蕉，2千克的糖，500克的黄油和500克的可可粉。 问题是对每一种类型的蛋糕，我们需要烤多少给游乐会来得到最大的利润。 一个可能的MiniZinc模型在 Listing 2.1.2 中给出。

 1% 为校园游乐会做蛋糕
 2
 3var 0..100: b; % 香蕉蛋糕的个数
 4var 0..100: c; % 巧克力蛋糕的个数
 5
 6% 面粉
 7constraint 250*b + 200*c <= 4000;
 8% 香蕉
 9constraint 2*b  <= 6;
10% 糖
11constraint 75*b + 150*c <= 2000;
12% 黄油
13constraint 100*b + 150*c <= 500;
14% 可可粉
15constraint 75*c <= 500;
16
17% 最大化我们的利润
18solve maximize 400*b + 450*c;
19
20output ["no. of banana cakes = \(b)\n",
21         "no. of chocolate cakes = \(c)\n"];

第一个新特征是 arithmetic expressions 的使用。

例子中的第二个新特征是优化。这行

solve maximize 400 * b + 450 * c;

指出我们想找一个可以使solve语句中的表达式（我们叫做 目标 ）最大化的解。 这个目标可以为任何类型的算术表达式。我们可以把关键字 maximize 换为 minimize 来表明一个最小化问题。

当我们运行上面这个模型时，我们得到以下的结果：

no. of banana cakes = 2
no. of chocolate cakes = 2
----------
==========

一旦系统证明了一个解是最优解，这一行 ========== 在最优化问题中会自动被输出。

2.1.3. 数据文件和谓词

此模型的一个缺点是如果下一次我们希望解决一个相似的问题，即我们需要为学校烤蛋糕（这是经常发生的）， 我们需要改变模型中的约束来表明食品间拥有的原料数量。如果我们想重新利用此模型，我们最好使得每个原料的数量作为 模型的参数，然后在模型的最上层设置它们的值。

更好的办法是在一个单独的 数据文件 中设置这些参数的值。 MiniZinc（就像很多其他的建模语言一样）允许使用数据文件来设置在原始模型中声明的 参数的值。 通过运行不同的数据文件，使得同样的模型可以很容易地和不同的数据一起使用。

数据文件的文件扩展名必须是 .dzn ，来表明它是一个MiniZinc数据文件。 一个模型可以被任何多个数据文件运行（但是每个变量/参数在每个文件中只能被赋一个值）

 1% 为校园游乐会做蛋糕（和数据文件一起）
 2
 3int: flour;  %拥有的面粉克数
 4int: banana; %拥有的香蕉个数
 5int: sugar;  %拥有的糖克数
 6int: butter; %拥有的黄油克数
 7int: cocoa;  %拥有的可可粉克数
 8
 9constraint assert(flour >= 0,"Invalid datafile: " ++
10                  "Amount of flour should be non-negative");
11constraint assert(banana >= 0,"Invalid datafile: " ++
12                  "Amount of banana should be non-negative");
13constraint assert(sugar >= 0,"Invalid datafile: " ++
14                  "Amount of sugar should be non-negative");
15constraint assert(butter >= 0,"Invalid datafile: " ++
16                  "Amount of butter should be non-negative");
17constraint assert(cocoa >= 0,"Invalid datafile: " ++
18                  "Amount of cocoa should be non-negative");
19
20var 0..100: b; % 香蕉蛋糕的个数
21var 0..100: c; % 巧克力蛋糕的个数
22
23% 面粉
24constraint 250*b + 200*c <= flour;
25% 香蕉
26constraint 2*b  <= banana;
27% 糖
28constraint 75*b + 150*c <= sugar;
29% 黄油
30constraint 100*b + 150*c <= butter;
31% 可可粉
32constraint 75*c <= cocoa;
33
34% 最大化我们的利润
35solve maximize 400*b + 450*c;
36
37output ["no. of banana cakes = \(b)\n",
38        "no. of chocolate cakes = \(c)\n"];

我们的新模型在 Listing 2.1.3 中给出。 我们可以用下面的命令来运行

数据文件 pantry.dzn 在 Listing 2.1.4 中给出。我们得到和 cakes.mzn 同样的结果。 运行下面的命令

$ minizinc cakes2.mzn pantry2.dzn

利用另外一个 Listing 2.1.5 中定义的数据集，我们得到如下结果

no. of banana cakes = 3
no. of chocolate cakes = 8
----------
==========

如果我们从 cakes.mzn 中去掉输出语句，MiniZinc会使用默认的输出。 这种情况下得到的输出是

b = 3;
c = 8;
----------
==========

1flour = 4000; 
2banana = 6; 
3sugar = 2000; 
4butter = 500; 
5cocoa = 500;

1flour = 8000; 
2banana = 11; 
3sugar = 3000; 
4butter = 1500; 
5cocoa = 800; 

通过使用 命令行标示 -D string ， 小的数据文件可以被直接输入而不是必须要创建一个 .dzn 文件， 其中 string 是数据文件里面的内容。

$ minizinc cakes2.mzn -D \
     "flour=4000;banana=6;sugar=2000;butter=500;cocoa=500;"

会给出和

$ minizinc cakes2.mzn pantry.dzn

一模一样的结果。

数据文件只能包含给模型中的决策变量和参数赋值的语句。

防御性编程建议我们应该检查数据文件中的数值是否合理。 在我们的例子中，检查所有原料的份量是否是非负的并且若不正确则产生一个运行错误，这是明智的。 MiniZinc提供了一个内置的布尔型操作符 断言 用来检查参数值。格式是 assert(B,S) 。 布尔型表达式 B 被检测。若它是假的，运行中断。此时字符串表达式 S 作为错误信息被输出。 如果我们想当面粉的份量是负值的时候去检测出并且产生合适的错误信息，我们可以直接加入下面的一行

constraint assert(flour >= 0,"Amount of flour is non-negative");

到我们的模型中。注意 断言 表达式是一个布尔型表达式，所以它被看做是一种类型的约束。我们可以加入类似的行来检测其他原料的份量是否是非负值。

2.1.4. 实数求解

MiniZinc also supports “real number” constraint solving using floating point variables and constraints. Consider a problem of taking out a short loan for one year to be repaid in 4 quarterly instalments. A model for this is shown in Listing 2.1.6. It uses a simple interest calculation to calculate the balance after each quarter.

通过使用浮点数求解，MiniZinc也支持“实数”约束求解。考虑一个要在4季度分期偿还的一年短期贷款问题。 此问题的一个模型在 Listing 2.1.6 中给出。它使用了一个简单的计算每季度结束后所欠款的利息计算方式。

 1% 变量
 2var float: R;        % 季度还款
 3var float: P;        % 初始借贷本金
 4var 0.0 .. 10.0: I;  % 利率
 5
 6% 中间变量
 7var float: B1; % 一个季度后的欠款
 8var float: B2; % 两个季度后的欠款
 9var float: B3; % 三个季度后的欠款
10var float: B4; % 最后欠款
11
12constraint B1 = P * (1.0 + I) - R;
13constraint B2 = B1 * (1.0 + I) - R;
14constraint B3 = B2 * (1.0 + I) - R; 
15constraint B4 = B3 * (1.0 + I) - R;
16
17solve satisfy;
18
19output [
20 "Borrowing ", show_float(0, 2, P), " at ", show(I*100.0), 
21 "% interest, and repaying ", show_float(0, 2, R), 
22  "\nper quarter for 1 year leaves ", show_float(0, 2, B4), " owing\n"
23];

注意我们声明了一个浮点型变量 f ，它和整型变量很类似。只是这里我们 使用关键字 float 而不是 int 。

我们可以用同样的模型来回答一系列不同的问题。第一个问题是：如果我以利息 4%借款$1000并且每季度还款$260，我最终还欠款多少？这个问题在数据文件 loan1.dzn 中被编码。

由于我们希望用实数求解，我们需要使用一个可以支持这种问题类型的求解器。Gecode(Minizinc捆绑二进制发布预设的求解器)支持浮点型变量,一个混合整数线性求解器可能更加适合这种类型的问题。 MiniZinc发布包含了这样的一个求解器。我们可以通过从求解器IDE菜单( Run 按钮下面的三角形)选择 COIN-BC 来使用, 或者在命令行中运行命令 minizinc --solver cbc :

$ minizinc --solver cbc loan.mzn loan1.dzn

输出是

Borrowing 1000.00 at 4.0% interest, and repaying 260.00
per quarter for 1 year leaves 65.78 owing
----------

第二个问题是如果我希望用4%的利息来借款$1000并且在最后的时候一点都不欠款，我需要在每季度还款多少？ 这个问题在数据文件 loan2.dzn 中被编码。 运行命令

$ minizinc --solver cbc loan.mzn loan2.dzn

后的输出是

Borrowing 1000.00 at 4.0% interest, and repaying 275.49
per quarter for 1 year leaves 0.00 owing
----------

第三个问题是如果我可以每个季度返还$250, 我可以用4%的利息来借款多少并且在最后的时候一点都不欠款？ 这个问题在数据文件 loan3.dzn 中被编码。 运行命令

$ minizinc --solver cbc loan.mzn loan3.dzn

后的输出是

Borrowing 907.47 at 4.0% interest, and repaying 250.00
per quarter for 1 year leaves 0.00 owing
----------

I = 0.04;
P = 1000.0;
R = 260.0;

I = 0.04;
P = 1000.0;
B4 = 0.0;

I = 0.04;
R = 250.0;
B4 = 0.0;

2.1.5. 模型的基本结构

我们现在可以去总结MiniZinc模型的基本结构了。 它由多个项组成，每一个在其最后都有一个分号 ; 。 项可以按照任何顺序出现。例如，标识符在被使用之前不需要被声明。

有八种类型的项 items 。

• 引用项 允许另外一个文件的内容被插入模型中。 它们有以下形式：

  include <文件名>;
  

  其中 <文件名> 是一个字符串常量。 它们使得大的模型可以被分为小的子模型以及包含库文件中定义的约束。 我们会在 Listing 2.2.4 中看到一个例子。

• 变量声明 声明新的变量。 这种变量是全局变量，可以在模型中的任何地方被提到。 变量有两种。在模型中被赋一个固定值的参数变量以及只有在模型被求解的时候才会 被赋值的决策变量。 我们称参数是 固定的 ，决策变量是 不固定的 。 变量可以选择性地被赋一个值来作为声明的一部分。形式是：

  <类型-实例化 表达式>: <变量> [ = ] <表达式>;
  

  <类型-实例化 表达式> 给了变量的类型和实例化。 这些是MiniZinc比较复杂的其中一面。 用 par 来实例化声明 参数，用 var 来实例化声明决策变量。 如果没有明确的实例化声明，则变量是一个参数。类型可以为基类型，一个 整数或者浮点数范围，或者一个数组或集合。 基类型有 float, int, string, bool, ann 。其中只有 float, int and bool 可以被决策变量使用。 基类型 ann 是一个 注解 – 我们会在 搜索 中讨论注解。 整数范围表达式 可以被用来代替类型 int. 类似的， 浮点数范围表达式 可以被用来代替类型 float 。 这些通常被用来定义一个整型决策变量的定义域，但也可以被用来限制一个整型参数的范围。 变量声明的另外一个用处是定义 枚举类型, —我们会在 枚举类型 中讨论。

• 赋值项 给一个变量赋一个值。它们有以下形式：

  <变量> = <表达式>;
  

  数值可以被赋给决策变量。在这种情况下，赋值相当于加入 constraint <变量> = <表达式> ;

• 约束项 是模型的核心。它们有以下形式：

  constraint <布尔型表达式>;
  

  我们已经看到了使用算术比较的简单约束以及内建函数 assert 操作符。 在下一节我们会看到更加复杂的约束例子。

• 求解项 详细说明了到底要找哪种类型的解。 正如我们看到的，它们有以下三种形式：

  solve satisfy;
  solve maximize <算术表达式>;
  solve minimize <算术表达式>;
  

  一个模型必须有且只有一个求解项。

• 输出项 用来恰当的呈现模型运行后的结果。 它们有下面的形式：

  output [ <字符串表达式>, ..., <字符串表达式> ];
  

  如果没有输出项，MiniZinc会默认输出所有没有被以赋值项的形式赋值的决策变量值。

• 枚举类型声明. 我们会在 数组和集合 和 枚举类型 中讨论。

• 谓词函数和测试项 被用来定义新的约束，函数和布尔测试。我们会在 谓词和函数 中讨论。

• 注解项 用来定义一个新的注解。我们会在 搜索 中讨论。