MiniZInc考前佛脚贴

MiniZInc考前佛脚贴

基本结构

它由多个项组成，每一个在其最后都有一个分号 ; 。 项可以按照任何顺序出现。例如，标识符在被使用之前不需要被声明。

有八种类型的项：

1. 引用项include <文件名>;。
2. 变量声明<类型-实例化 表达式>: <变量> [ = ] <表达式>; 。<类型-实例化 表达式> 给了变量的类型和实例化。用 par 来实例化声明参数，用 var 来实例化声明决策变量。 如果没有明确的实例化声明，则变量是一个参数。
3. 赋值项<变量> = <表达式>;。
4. 约束项constraint <布尔型表达式>;。
5. 求解项solve satisfy; solve maximize <算术表达式>; solve minimize <算术表达式>;。
6. 输出项output [ <字符串表达式>, ..., <字符串表达式> ];。如果没有输出项，默认输出所有没有被以赋值项的形式赋值的决策变量值。
7. 枚举类型声明。
8. 谓词函数和测试项。

复杂结构

数组和集合

集合变量用以下方式声明set of <类型-实例化> : <变量名> ;。
集合常量有以下形式{ <表达式-1>, ..., <表达式-n> }，或者是以下形式的整型，枚举型或浮点型范围表达式<表达式-1> .. <表达式-2>。

集合操作符：元素属于 (in), (非严格的) 集合包含 (subset), (非严格的) 超集关系 (superset), 并集 (union), 交集 (intersect), 集合差运算 (diff), 集合对称差 (symdiff) 和集合元素的个数 (card).

枚举类型，我们称为 enums , 用以下方式声明enum <变量名> ;，一个枚举类型用以下赋值的方式定义enum <变量名> = { <变量名-1>, ..., <变量名-n> } ;。
其中 <变量名-1>, …, <变量名-n> 是名为 <变量名> 的枚举类型中的元素。

一维和多维数组，它们用以下类型来声明：array [ <下标集合-1>, ..., <下标集合-n> ] of <类型-实例化>。

列表和集合推导式

列表推导式的一般格式是[ <表达式> | <生成元表达式> ]。<表达式> 指明了如何从 <生成元表达式>产生的元素输出列表中创建元素。生成元由逗号分开的一列生成元表达式组成，选择性地跟着一个布尔型表达式。

两种格式是<生成元>, ..., <生成元>、<生成元>, ..., <生成元> where <布尔表达式>。第二种格式中的可选择的 <布尔型表达式> 被用作生成元表达式的过滤器：只有满足布尔型表达式的输出列表中的元素才被用来构建元素。 生成元有以下格式<标识符>, ..., <标识符> in <数组表达式>。每一个标识符是一个迭代器，轮流从数值表达式中取值，最后一个标识符变化的最迅速。
例如，列表推导式 [i + j | i, j in 1..3 where j < i] 算得 [2 + 1, 3 + 1, 3 + 2] 等同于 [3, 4, 5] 。 [3, 4, 5] 只是一个下标集合为 1..3 的数组。

集合推导式几乎和列表推导式一样：唯一的不同是这里使用 { 和 } 括住表达式而不是 [ 和 ] 。集合推导式生成的元素必须是固定的，即不能是决策变量。类似的，集合推导式的生成元和可选择的<布尔型表达式>必须是固定的。
例如 {i + j | i, j in 1..3 where j < i} 计算得到集合 {3, 4, 5} 。

聚合函数

算术数组的聚合函数有：sum 把元素加起来， product 把元素乘起来，和 min 跟 max 各自返回数组中的最小和最大元素。 当作用于一个空的数组时， min 和 max 返回一个运行错误， sum 返回0， product 返回1。

包含有布尔型表达式的四个聚合函数有：

1. forall ，它返回一个等于多个约束的逻辑合取的单个约束。
2. exists ，返回多个约束的逻辑析取。因此 forall 强制数组中的所有约束都满足，而 exists 确保至少有一个约束满足。
3. xorall 确保奇数个约束满足。
4. 第四个函数， iffall 确保偶数个约束满足。

一个 生成表达式 有以下格式
<聚合函数> ( <生成元表达式> ) ( <表达式> )
圆括号内的 <生成元表达式> 以及构造表达式 <表达式> 是非选择性的：它们必须存在。它等同于
<聚合函数> ( [ <表达式> | <生成元表达式> ] )
<聚合函数> 可以是MiniZinc的任何由单个数组作为其参数的函数。

全局约束

条件表达式

条件表达式的格式是
if <布尔型表达式> then <表达式-1> else <表达式-2> endif
例如，若 y 不是零，则 r 设为 x 除以 y ，否则则设为零。
int: r = if y != 0 then x div y else 0 endif;

枚举类型

枚举类型操作符

1. enum_next(X,x): 返回枚举类型 X 中 x 后的下一个值。 这是一个部份函数, 如果 x 是枚举类型X 最后一个值, 则函数会返回$\perp$令包含这个表达式的布尔表达式返回 false 。
2. enum_prev(X,x) enum_prev(X,x): 返回枚举类型 X 中 x 的上一个值。 enum_prev同样是一个部份函数。
3. to_enum(X,i): 映射一个整型表达式i到一个在X的枚举类型值, 或者如果i是小于等于0或大于X中元素的个数, 则返回 :math:bot。

注意，一些标准函数也是可以应用于枚举类型上
4. card(X): 返回枚举类型 X 的势。
5. min(X): 返回枚举类型 X中最小的元素。
6. max(X): 返回枚举类型 X 中最大的元素。

复杂约束

布尔型布尔常量是真或假 ，布尔型操作符有合取，即，与 (/\) ，析取，即，或 (\/) ，必要条件蕴含 (<-) ，充分条件蕴含 (->) ，充分必要蕴含 (<->) 以及非 (not)。

集合约束

关键字 var 出现在 set 声明之前，表明这个集合本身是决策变量。

谓词和函数