Foreword
The purpose of this article is to prepare for the discrete modeling exam no. 23. Although the questions are objective questions, but time interval is too long, before learning also forgot almost. So I decided to organize the original study notes and upload them here. Hopefully it will wake up the memories of months of sleep. I am about to take an examination of the principles of chemical engineering. There is not much time for me, so I will update it at 2:00 every day. I will update the four chapters before the exam. My editor may make mistakes, so we are welcome to exchange ideas and learn from each other.
第一章 MiniZinc介绍
MiniZinc的求解程序分为5部分,参数定义、决策变量声明、约束、目标、输出。
参数分为两种:决策变量和参数变量。
变量类型:int,float,或者bool(或者是一个范围/集合);l..u 表示一个从l 到u 的连续整数序列(若l,u为小数则表示该精确度下从l到u虽有的数)。
决策变量定义:var 变量类型: 变量名称
int: i=3;
var 0..4: i;
约束表达:
constraint <约束表达式>;
求解:solve satisfy 或 solve maximize(minimize)约束式;
输出:output <字符串列表>;show(v) 以字符串形式输出v的值;"house" ++ "boat" 用于连接字符串;\(v) 在字符串常量中显示v。
枚举类型:
enum:枚举类型名;
枚举类型名= { id1, …, idn } ;
可以使用枚举类型名来声明变量: var 枚举类型名: 变量名 %变量的取值范围是枚举类型。(数组下标可以是枚举类型)
数据文件后缀名: .dzn
数组声明:
array[DISH] of int: satisf; %satis是一数组,其下标用枚举类型[DISH]表示。int前加var定义决策变量。
数组查找:数组名[下标表达式]如satisf[i]。
生成器表达式:
forall(i in DISH)(amt[i] >= 0);sum(i in DISH)(satisf[i] * amt[i]);
两维数组声明:
array[PRODUCT,RESOURCE] of float: consumption; consumption是一个二维数组,确定了PRODUCT和RESOURCE后consumption有唯一确定值。
二维数组查找: consumption[p, r];同时前面要说明“p in PRODUCT”"r in RESOURCE"。
数组的元素可以是任何类型,但不可以是另外一个数组。
内建函数length返回一维数组的长度。
数组的表达:一维数组:
profit = [400, 500];
二维数组:起始于[| | 用来分隔行(第一维) 结束于|] 如:
consumption = [| 1.5, 1.0, 1.0, 1.0
| 2.0, 0.0, 2.0, 0.0
| 1.5, 0.5, 1.0, 1.0
| 0.5, 1.0, 0.9, 1.5
| 0.1, 2.5, 0.1, 2.5 |];
对任何维度的数组(≤ 6)都可以使用arraynd族的函数进行初始化。它们把一个一维数组转换为一个n 维数组。
也可以使用推导式来把一个n 维数组展平为一个列表(一维数组)。
array[1..20] of int: list =[consumption[i,j] | i in 1..5, j in 1..4]; %(这我也不是很懂)
数组推导式:[ 表达式| 生成器1, 生成器2, … where 测试]
例如[i + j | i, j in 1..4 where i < j]
= [1+2, 1+3, 1+4, 2+3, 2+4, 3+4]
= [3, 4, 5, 5, 6, 7]
MiniZinc提供了各种对列表或者集合进行操
作的内建函数
数字列表:sum, product, min, max
约束列表:forall, exists
语法:
%下面两个式子等价
forall(i,j in 1..10 where i < j)(a[i] != a[j]);
forall([a[i] != a[j]| i,j in 1..10 where i < j]);
枚举类型为对象命名
数组来捕捉(存放)对象的信息
推导式用来创建适用于不同规模的数据的
• 约束,以及
• 表达式
全局约束:
原则上,任何可以取无限个变量为参数的约束(就是全局约束),所以线性约束是“全局的”。
全局约束是在很多问题都会出现的约束。
全局约束可以使模型更简短求解变得更容易(因为求解器可以利用全局约束
的结构信息)
Include 语句:
include "文件名";
会在MiniZinc模型中包含该文件
会在当前文件夹和MiniZinc库路径中寻找
include "alldifferent.mzn";
constraint alldifferent([M1,M2,M3,M4,M5]);
集合参数可如下定义
set of 类型: 变量名= 固定值集合;
它们可以作为固定值集合使用
变量对应表 下标表达式可以包括决策变量
例子:
set of int: DIGIT = 1..9;%DIGIT集合{1,2,...,9}
array[DIGIT] of int: rods = [1,2,3,4,5,2,3,4,5];%吧roads这一个一维数组的下角标设置为DIGIPT
MiniZinc中将变量分为两类:参数变量和决策变量。其中参数变量一般是固定或者已知的值,其中决策变量简单的理解就是我们优化模型中要求解的那个自变量x。决策变量在定义时只需在前面加上var即可。
变量可以有多种类型如int(整数),float(浮点数),bool(只有0,1两种状态的布尔数)还有集合(第二章会提到)。学习中主要用的都是整数。建模优化过程中经常用到一个变量的范围,程序中用l .. u : b来表示b<=u,b>=l间所有的整数。
int : a=4 %引入一个参数a=4
var int : a %引入一个整数决策变量a
var l .. u : b %决策变量b为[l,u]之间的整数
第二章 集合建模
0-1布尔数组定义:array[MOVES] of var bool: occur; occur是以MOVES为下表的数组,且只能为0或1。
bool2int(false) = 0
bool2int(true) = 1
如果在MiniZinc期望为整型数据的地方使用布尔型数据,bool2int可以神略,MiniZinc会自动”使用"bool2int函数。
集合变量:与集合参数(见第一章)类似,var set of {1,2,3}: x; 表示为x为集合{1,2,3}的一个子集。
emun MOVES;var set of MOVES: occur; 集合不一定是数,枚举类型也可以作为一个集合。
其他可对集合变量的可选值建模的集合表示方式,例如:array[1..3] of var 0..1: y;这里的y是一个一维数组,下标是1到3,取值范围是0到1。大家注意它和var set of {1,2,3}: x;的区别和联系,他们可以用来表达相同的意思。若x为{3}那么y的[0,0,1]与它是一个意思,同理x为{1,3}那么y的[1,0,1]与它是一个意思。
集合操作符(作业中用到的比较少)
MiniZinc提供了(中缀)集合操作符
in(集合中的元素例如: x in s)
subset, superset(子集,超集)
intersect(交集)
union(并集)
card(集合势)
diff(差运算,例如:x diff y = x \ y)
symdiff(对称差)
• 例如:
- {1, 2, 5, 6} symdiff {2, 3, 4, 5} = {1, 3, 4, 6}
贪心算法:用每一小步的最优解一步步算下来最后得到整体的最优解,贪心算法得到的不一定是最佳答案(数学建模常用算法,做过校内赛的同学应该都知道,这里也不是这个课的重点就不多说了)
set of int: SPOT = 1..nSpots;%定义一个集合SPOT
enum SYMB;%一个枚举类型SYMB
array[SYMB] of set of SPOT: group;%一个一维数组group,以SYMB为下角标,取值范围在SPOT这个集合里
语句可以多层嵌套,主要理解最后一句的意思。
确定一个固定势集合(势可以理解为元素的个数)
array[1..3] of var 1..10: x;%定义一个元素个数为3的数组,取值范围shi是1到10
var set of 1..10: x;%x为{1..10}的所有子集
card(x) = 3;%限定x元素个数(势)为3
第一个用数组表达代表了1000中可能,第二种用集合表达代表了120种可能。为了让第一个表达和第二个表达集合等价,于是需要添加约束。
forall(i,j in 1..u where i < j)(x[i] != x[j]);%确保它们全部都不相同
forall(i in 1..u-1)(x[i] < x[i+1]);%确保按顺序排列
有多种方式去表示固定势集合
var set of OBJ + 势约束
• 适用情况:求解器本身支持集合
• 适用情况:OBJ不是太大
array[1..u] of var OBJ
• 适用情况:当u比较小
两个对决策变量建模时的关键问题:确保模型的每个解是问题的一个解
确定一个有界势集合(比如确定一个元素个数小于3的集合)
array[1..size] of var SPOTx: attacks;%SPOTx里面要有一个元素表示“无”或“空”元素,这个元素的其他值都为0
forall(i in 1..size-1)(attacks[i] >=(attacks[i]!=0)+attacks[i+1]);%0这个元素可以重复,使势减小就可以用0来替代元素,多一个0原来的势就少1.
多种方式去表示集合
var set of OBJ
• 适用情况:求解器本身支持集合
• 适用情况:OBJ不是太大
array[OBJ] of var bool / 0..1
• 适用情况:OBJ不是太大
array[1..u] of var OBJ
• 只用于固定势u
• 适用情况:当u比较小
array[1..u] of var OBJx
• 需要表示“无”这个元素
第三章 函数建模
函数可以分为
单射:分配问题
双射(|DOM|=|COD|):匹配问题
全局约束alldifferent
强制使一个数组内元素各不相同
array[HERO] of var SPOT: pos;%pos是一个以HERO为下标的一维数组,pos的值从SPOT里面选。用函数的角度来说HERO就是x的定义域,SPOT是取值范围。
include “alldifferent.mzn”;
alldifferent(pos); %每一个x都有不同的y值与他对应
分配子问题在很多应用中都很常见,可以通过添加其它约束来完善模型。
逻辑联结词
布尔表达式
true
false
/\ 合取
\/ 析取
-> 蕴含
<-> 双蕴含或者等价
not 非
forall(s in SOLDIER, d in 1..nDays-2)
(roster[s,d] = NIGHT /\ roster[s,d+1] = NIGHT
-> roster[s,d+2] != NIGHT);
模型代码中有共同的子表达式会导致求解时间变长
forall(d in DAY)
(sum(s in SOLDIER)
(roster[s,d] = EVE) >= l);
forall(d in DAY)
(sum(s in SOLDIER)
(roster[s,d] = EVE) <= u);
于是就需要合并表达式,这里有两种方法:
- 中间变量
存储会再次用到的表达式的值
依赖于决策变量
(注意: 中间参数也是!)给中间变量选择一个好的界限
array[DAY] of var 0..card(SOLDIER): onEve;
onEve = [sum(s in SOLDIER)(roster[s,d] = EVE)
| d in DAY];
forall(d in DAY)
(onEve[d] >= l /\ onEve[d] <= u);
- 直接定义时给出范围
array[DAY] of var l..u: onEve;
onEve = [sum(s in SOLDIER)(roster[s,d] = EVE)
| d in DAY];
划分问题
很多时候当我们划分一个集合时,我们必须要限定每个划分类的大小。我们有特殊的约束来限定划分类的大小。
global_cardinality(x, v, c)
v和c的大小一样
约束ci = Σj in 1..n(xj = vi)
收集出现次数,限定vi出现的次数
例如,
global_cardinality(x,[1,2],[4,3]);%x中1必须出现4次,2必须出现3次
x = [1,1,1,1,2,2,2,3] √ x = [1,1,1,1,1,2,2,2,3] ×
其它全局势约束(global_cardinality 族函数)
收集出现次数,要求每个值都出现
global_cardinality_closed(x, v, c)
xi 的值都要从v 来: 就是∀i.∃j. xi = vj
限定出现次数的上限和下限
global_cardinality_low_up(x, v, lo, hi)
约束loi ≤ (Σj in 1..n (xj = vi)) ≤ hii
限定出现次数的上限和下限,要求每个值都出现
global_cardinality_low_up_closed(x,v,l,u)
纯划分
把DOM划分为最多k部分
对DOM的每一个元素, 用一个变量来指明被
分配到了哪个划分类
简单的数组表示
array[DOM] of var 1..k: x
注意会出现多重表示,因为用哪个数字表示类别是无关紧要的(只做分类不做排序)
例如,DOM = 1..4, k = 3
x = [1,2,1,3] ➔ {1,3} {2} {4}
x = [3,1,3,2] ➔ {2} {4} {1,3}
x = [3,2,3,1] ➔ {4} {2} {1,3}
为了消除多重表示就需要去除值对称
MiniZinc包含了一个用于去值对称的全局约束
value_precede_chain(array[int] of int: c,array[int] of var int: x)
强制c[i]在x中的第一次出现先于c[i+1]在x中的第一次出现
例如,
value_precede_chain([1,2,3], x);
x = [1,1,2,3] √, [1,3,1,2] ×,[1,2,1,2] √(这个模型并不要求正好而只是最多k个类)
可以很容易地添加一条约束来强制每个类都有成员
下界= 1
上界= nSpot - k + 1
global_cardinality_low_up_closed(shot,
[i | i in CLUSTER], [1 | i in CLUSTER],
[nSpot-k+1 | i in CLUSTER]);
半监督聚类法会向问题添加约束,例如:
某些点必须在相同或不同的类中
用相等(=)约束或者非等(≠) 约束表达
类大小的界限
用全局势约束表达
其他种类的约束
实际上就是个添加约束的过程,这一章提出了全局约束(程序的内置函数)这一概念来优化模型,减少求解时间。这一章了解什么是分配、匹配、分类问题如何求解,几个全局约束名称和含义,以及它知道可以用来减少计算时间就可以了。
第四章 多重建模
可能更新不完了。。
inverse函数的使用
include "globals.mzn";
enum FOOD;
enum WINE;
array[FOOD, WINE] of int: joy;
array[FOOD] of var WINE: drink; %一个函数
array[WINE] of var FOOD: eat; %它的逆函数
constraint inverse(eat, drink); %类似于alldifferent,使两个函数一一对应
solve maximize sum(f in FOOD)(joy[f, drink[f]]);
% solve maximize sum(w in WINE)(joy[eat[w], w]);
当且仅当的表达式:<->
使用inverse函数后可以完成一些原来难以表达的映射。
当且仅当蛇羹和花雕配对时,麻婆豆腐才会
跟米酒配对
eat[RICE] = MAPOTOFU <->eat[HUADIAO] = SNAKESOUP;
或
drink[MAPOTOFU] = RICE <->drink[SNAKESOUP] = HUADIAO;
或
eat[RICE] = MAPOTOFU <->drink[SNAKESOUP] = HUADIAO;
或
drink[MAPOTOFU] = RICE <->eat[HUADIAO] = SNAKESOUP;
附录
本页面固定链接 http://liuxuan.xyz/minizinc/
原课程链接 http://www.cnmooc.org/portal/course/3783/7604.mooc;
https://www.coursera.org/learn/basic-modeling
MiniZinc官网 http://www.minizinc.org/
官方指南(中文版) http://www.minizinc.org/tutorial/minizinc-tute-cn.pdf
GitHub仓库 https://github.com/liuxuan99/MyMiniZinc