this repo has no description
dekker.one
1.. _sec-flattening:
2
3FlatZinc和展平
4=======================
5
6.. \pjs{Maybe show the toolset at this point?}
7
8约束求解器不会直接支持MiniZinc模型.为了运行一个MiniZinc模型,它被翻译成一个MiniZinc的简单子集叫FlatZinc.
9FlatZinc反映了大多数约束求解器只会求解具有 :math:`\bar{exists} c_1 \wedge \cdots \wedge c_m` 的满足问题
10或者有 :math:`\text{minimize } z \text{ subject to } c_1 \wedge \cdots \wedge c_m` 的优化问题, 其中
11:math:`c_i` 是基本的约束而 :math:`z` 是一个具有某些限定形式的整型或者浮点表达式.
12
13.. index::
14 single: minizinc -c
15
16``minizinc`` 工具包含了MiniZinc *编译器* ,它可以用一个MiniZinc模型和数据文件来创建
17一个展平后的FlatZinc模型,它等价于给定数据的MiniZinc模型表达为之前提到的受限制的形式.
18通常来说构建一个给求解器的FlatZinc模型是对用户隐藏的,不过你也可以通过以下命令查看结合
19数据 ``data.dzn`` 来展平一个模型 ``model.mzn`` 的结果:
20
21.. code-block:: bash
22
23 minizinc -c model.mzn data.dzn
24
25这会创建一个FlatZinc模型叫 ``model.fzn`` .
26
27在这一章中我们探索把MiniZinc翻译成FlatZinc的过程.
28
29展平表达式
30----------------------
31
32底层求解器的限制意味着复杂的MiniZinc表达式需要被 *展平* 为内部不具有更复杂结构项的基本约束的合取式.
33
34思考以下保证两个在长方形箱子的两个圆不会重叠的模型:
35
36.. literalinclude:: examples/cnonoverlap.mzn
37 :language: minizinc
38 :caption: 两个不会重叠的圆的模型 (:download:`cnonoverlap.mzn <examples/cnonoverlap.mzn>`).
39 :name: fig-nonoverlap
40
41简化和求值
42~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
43
44给定数据文件
45
46.. code-block:: minizinc
47
48 width = 10.0;
49 height = 8.0;
50 r1 = 2.0;
51 r2 = 3.0;
52
53转换到FlatZinc首先通过替换所有参数为它们的值来简化模型, 然后求出所有取值已经固定的表达式的值.
54在这步简化后参数的值将不再需要.
55一个例外是大型数组的参数值.如果它们被适用多于一次,那么为了避免重复大的表达式这个参数会被保留.
56
57在简化后, :numref:`fig-nonoverlap` 的模型的变量和参数声明部分变为
58
59.. literalinclude:: examples/cnonoverlap.fzn
60 :language: minizinc
61 :start-after: % 变量
62 :end-before: %
63
64.. _sec-flat-sub:
65
66定义子表达式
67~~~~~~~~~~~~~~~~~~~~~~~
68
69现在没有约束求解器可以直接处理像在 :numref:`fig-nonoverlap` 里复杂的约束表达式.
70作为替代,我们可以命名表达式中的每一个子表达式,我们创建约束来构建及代表子表达式的数值.
71让我们来看看约束表达式的子表达式. :mzn:`(x1 - x2)` 是一个子表达式, 如果我们将它命名为
72:mzn:`FLOAT01` 我们可以定义它为 :mzn:`constraint FLOAT01 = x1 - x2;` . 注意到这个表达式
73只在模型中出现两次. 我们只需要构建这个值一次,然后我们可以重复使用它. 这就是 *共同子表达式消除* .
74子表达式 :mzn:`(x1 - x2)*(x1 - x2)` 可以命名为 :mzn:`FLOAT02` , 而我们可以定义它为
75:mzn:`constraint FLOAT02 = FLOAT01 * FLOAT01;` . 我们可以命名 :mzn:`constraint FLOAT03 = y1 - y2;`
76和 :mzn:`constraint FLOAT04 = FLOAT03 * FLOAT03;` 最后 :mzn:`constraint FLOAT05 = FLOAT02 * FLOAT04;` .
77不等约束本身则变成 :mzn:`constraint FLOAT05 >= 25.0;` 因为 :mzn:`(r1+r2)*(r1 + r2)` 计算出结果为 :mzn:`25.0` .
78于是这个约束被展平为
79
80.. code-block:: minizinc
81
82 constraint FLOAT01 = x1 - x2;
83 constraint FLOAT02 = FLOAT01 * FLOAT01;
84 constraint FLOAT03 = y1 - y2;
85 constraint FLOAT04 = FLOAT03 * FLOAT03;
86 constraint FLOAT05 = FLOAT02 * FLOAT04;
87 constraint FLOAT05 >= 25.0
88
89.. _sec-flat-fzn:
90
91FlatZinc约束形式
92~~~~~~~~~~~~~~~~~~~~~~~~
93
94展平的最后步骤是把约束的形式转换成标准的FlatZinc形式,它总是以 :math:`p(a_1, \ldots, a_n)` 的形式出现.
95其中的 :mzn:`p` 是某个基础约束, :math:`a_1, \ldots, a_n` 是参数. FlatZinc尝试使用最少的
96不同约束形式. 所以 :mzn:`FLOAT01 = x1 - x2` 首先尝试重写为 :mzn:`FLOAT01 + x2 = x1`
97然后使用 :mzn:`float_plus` 输出基本的约束. 得出的约束形式如下:
98
99.. literalinclude:: examples/cnonoverlap.fzn
100 :language: minizinc
101 :start-after: % 约束
102 :end-before: %
103
104边界分析
105~~~~~~~~~~~~~~~
106
107我们仍然缺少一项,声明引入的变量 :mzn:`FLOAT01` , ...,
108:mzn:`FLOAT05` . 这些可以被声明为 :mzn:`var float` . 不过为了令求解器的任务更简单,
109MiniZinc尝试通过简单的分析确定新引入变量的上界和下界. 比如因为 :mzn:`FLOAT01 = x1 - x2`
110和 :math:`2.0 \leq` :mzn:`x1` :math:`\leq 8.0` 还有 :math:`3.0 \leq` :mzn:`x2` :math:`\leq 7.0`, 所以可以得出 :math:`- 5.0 \leq` :mzn:`FLOAT01` :math:`\leq 5.0`
111然后我们可以看到 :math:`-25.0 \leq` :mzn:`FLOAT02` :math:`\leq 25.0` (尽管注意到如果我们发现
112相乘实际上是平方,我们可以给出更精确的边界 :math:`0.0 \leq` :mzn:`FLOAT02` :math:`\leq 25.0` ).
113
114细心的读者会发现在 :ref:`sec-flat-sub` 和 :ref:`sec-flat-fzn` 里约束的展平形式的一点不同.
115在后面没有非等约束. 因为一元的不等式可以完全被一个变量的边界表示出来,不等关系可以令 :mzn:`FLOAT05`
116的下界变为 :mzn:`25.0` , 然后这会变得冗余. 最后 :numref:`fig-nonoverlap` 的展平后形式是:
117
118.. literalinclude:: examples/cnonoverlap.fzn
119 :language: minizinc
120
121目标函数
122~~~~~~~~~~
123
124MiniZinc 就像展平约束一样, 展平最小化和最大化目标函数. 跟其他表达式一样, 目标表达式
125被展平时创建一个变量. 在FlatZinc输出求解项永远是单一变量. 看一下例子 :ref:`sec-let` .
126
127.. \pjs{Do we need an example here?}
128
129线性表达式
130------------------
131
132约束的一个最重要的而广泛用于建模的形式是线性约束
133
134.. math:: a_1 x_1 + \cdots + a_n x_n \begin{array}[c]{c} = \\ \leq \\ < \end{array} a_0
135
136其中 :math:`a_i` 是整数或者浮点数约束, 而 :math:`x_i` 是整数或者浮点数变量.
137它们非常有表达能力,同时也是(整数)线性规划约束求解器唯一支持的形式.
138从MiniZinc到FlatZinc的翻译器尝试创建线性约束, 而不是把线性约束变成许多子表达式.
139
140.. \pjs{Maybe use the equation from SEND-MORE-MONEY instead?}
141
142.. literalinclude:: examples/linear.mzn
143 :language: minizinc
144 :caption: 说明线性约束展平的MiniZinc模型 (:download:`linear.mzn <examples/linear.mzn>`).
145 :name: fig-lflat
146
147考虑在 :numref:`fig-lflat` 中的模型. 这里并没有为所有子表达式 :math:`3*x`, :math:`3*x - y` , :math:`x * z` , :math:`3*x - y + x*z` ,
148:math:`x + y + z` , :math:`d * (x + y + z)` , :math:`19 + d * (x + y + z)` ,
149和 :math:`19 + d * (x + y + z) - 4*d` 创建一个变量. 这里的翻译在创建一个FlatZinc约束时, 会尝试创建一个尽可能记录大部分原约束内容的线性约束.
150
151展平会创建线性表达式并将其视为一个单位, 而不视为每个字表达是构建中间变量.这也使创建的表达式简单化.
152从约束中抽取出线性表达式为
153
154.. code-block:: minizinc
155
156 var 0..80: INT01;
157 constraint 4*x + z + INT01 <= 23;
158 constraint INT01 = x * z;
159
160注意到 *非线性表达式* :math:`x \times z` 是如何被抽取出来作为一个新的子表达式并赋予名字的,
161与此同时剩下的项会被收集起来从而使每个变量只出现一次 (的确变量 :math:`y` 的项被移除了)
162
163最后每个约束被写到FlatZinc形式, 从而得到:
164
165.. code-block:: minizinc
166
167 var 0..80: INT01;
168 constraint int_lin_le([1,4,1],[INT01,x,z],23);
169 constraint int_times(x,z,INT01);
170
171.. _sec-unroll:
172
173展开表达式
174---------------------
175
176大多数的模型需要创建一些基于输入数据的约束.
177MiniZinc通过数组类型,列表和列生成解析还有聚合函数来支持这些模型.
178
179考虑以下从生产调度例子 :numref:`ex-prod-planning` 中出现的聚合函数表达式
180
181.. code-block:: minizinc
182
183 int: mproducts = max (p in Products)
184 (min (r in Resources where consumption[p,r] > 0)
185 (capacity[r] div consumption[p,r]));
186
187由于这用到生成器语法,我们可以把它重写成可以被编译器处理的相等的形式:
188
189.. code-block:: minizinc
190
191 int: mproducts = max([ min [ capacity[r] div consumption[p,r]
192 | r in Resources where consumption[p,r] > 0])
193 | p in Products]);
194
195给定数据
196
197.. code-block:: minizinc
198
199 nproducts = 2;
200 nresources = 5;
201 capacity = [4000, 6, 2000, 500, 500];
202 consumption= [| 250, 2, 75, 100, 0,
203 | 200, 0, 150, 150, 75 |];
204
205这首先创建 :mzn:`p = 1` 的数组
206
207.. code-block:: minizinc
208
209 [ capacity[r] div consumption[p,r]
210 | r in 1..5 where consumption[p,r] > 0]
211
212也就是 :mzn:`[16, 3, 26, 5]` 然后计算最小值为3. 它之后为 :mzn:`p = 2` 建立相同的数组 :mzn:`[20, 13, 3, 6]` ,
213并计算最小的数值为3. 然后创建数组 :mzn:`[3, 3]` 并计算最大值为3. 在FlatZinc里面没有
214:mzn:`mproducts` 的表示, 这种通过计算数值3的方法会被用来代替 :mzn:`mproducts` .
215
216在约束模型中最常见的聚合表达式是 :mzn:`forall` . Forall表达式会被展开成为多个约束.
217
218考虑以下在SEND-MORE-MONEY例子 :numref:`ex-smm` 中使用预设的
219分解 :mzn:`alldifferent` 出现的MiniZinc片段.
220
221
222.. code-block:: minizinc
223
224 array[1..8] of var 0..9: v = [S,E,N,D,M,O,R,Y];
225 constraint forall(i,j in 1..8 where i < j)(v[i] != v[j])
226
227:mzn:`forall` 表达式为每一对需要满足 :math:`i < j` 的 :math:`i, j` 创建一个约束,
228所以创建
229
230.. code-block:: minizinc
231
232 constraint v[1] != v[2]; % S != E
233 constraint v[1] != v[3]; % S != N
234 ...
235 constraint v[1] != v[8]; % S != Y
236 constraint v[2] != v[3]; % E != N
237 ...
238 constraint v[7] != v[8]; % R != Y
239
240在FlatZinc中形成
241
242.. code-block:: minizinc
243
244 constraint int_neq(S,E);
245 constraint int_neq(S,N);
246 ...
247 constraint int_neq(S,Y);
248 constraint int_neq(E,N);
249 ...
250 constraint int_neq(R,Y);
251
252注意到临时的数组变量 :mzn:`v[i]` 是如何在FlatZinc的输出中被原来的变量替换的.
253
254数组
255------
256
257一维变量在MiniZinc中可以有任意的下标,只要它们是相邻的整数.
258在FlatZinc所有数组都被 :mzn:`1..l` 标注, 其中 :mzn:`l` 是数组的长度.
259这意味着数组查询时需要被转换成FlatZinc下标的形式.
260
261考虑以下MiniZinc模型来使用 :mzn:`m` 个1kg砝码来平衡一个长为 :mzn:`2 * l2` 的跷跷板, 其中上面有一个重为
262:mzn:`cw` kg小孩.
263
264.. code-block:: minizinc
265
266 int: cw; % 小孩重量
267 int: l2; % 一半跷跷板长度
268 int: m; % 1kg砝码的数量
269 array[-l2..l2] of var 0..max(m,cw): w; % 在每个点的重量
270 var -l2..l2: p; % 孩子的位置
271 constraint sum(i in -l2..l2)(i * w[i]) = 0; % 平衡
272 constraint sum(i in -l2..l2)(w[i]) = m + cw; % 所有使用的砝码
273 constraint w[p] = cw; % 孩子在位置p
274 solve satisfy;
275
276给定 :mzn:`cw = 2`, :mzn:`l2 = 2`, 和 :mzn:`m = 3` , 展开可以产生约束
277
278.. code-block:: minizinc
279
280 array[-2..2] of var 0..3: w;
281 var -2..2: p
282 constraint -2*w[-2] + -1*w[-1] + 0*w[0] + 1*w[1] + 2*w[2] = 0;
283 constraint w[-2] + w[-1] + w[0] + w[1] + w[2] = 5;
284 constraint w[p] = 2;
285
286不过FlatZinc坚持 :mzn:`w` 数组从下标1开始.
287这意味着我们需要重写所有数组获取来使用新的下标数值.
288对于固定值数组查找这很简单,对于变量值数组查找我们可能需要创建一个新的变量.
289以上公式的结果为
290
291.. code-block:: minizinc
292
293 array[1..5] of var 0..3: w;
294 var -2..2: p
295 var 1..5: INT01;
296 constraint -2*w[1] + -1*w[2] + 0*w[3] + 1*w[4] + 2*w[5] = 0;
297 constraint w[1] + w[2] + w[3] + w[4] + w[5] = 5;
298 constraint w[INT01] = 2;
299 constraint INT01 = p + 3;
300
301最后我们重写约束成FlatZinc的形式. 注意到变量数组下标查找的形式是如何映射到 :mzn:`array_var_int_element` 上的.
302
303.. code-block:: minizinc
304
305 array[1..5] of var 0..3: w;
306 var -2..2: p
307 var 1..5: INT01;
308 constraint int_lin_eq([2, 1, -1, -2], [w[1], w[2], w[4], w[5]], 0);
309 constraint int_lin_eq([1, 1, 1, 1, 1], [w[1],w[2],w[3],w[4],w[5]], 5);
310 constraint array_var_int_element(INT01, w, 2);
311 constraint int_lin_eq([-1, 1], [INT01, p], -3);
312
313MiniZinc支持多维数组,但是(目前来说)FlatZinc只支持单维度数组.
314这意味着多维度数组必须映射到单维度数组上,而且多维度数组访问必须映射到
315单维度数组访问.
316
317考虑在有限元平面模型 :numref:`ex-laplace`: 的Laplace等式约束:
318
319.. literalinclude:: examples/laplace.mzn
320 :language: minizinc
321 :start-after: % arraydec
322 :end-before: % sides
323
324假设 :mzn:`w = 4` 和 :mzn:`h = 4` ,这会创建约束
325
326.. code-block:: minizinc
327
328 array[0..4,0..4] of var float: t; % temperature at point (i,j)
329 constraint 4.0*t[1,1] = t[0,1] + t[1,0] + t[2,1] + t[1,2];
330 constraint 4.0*t[1,2] = t[0,2] + t[1,1] + t[2,2] + t[1,3];
331 constraint 4.0*t[1,3] = t[0,3] + t[1,2] + t[2,3] + t[1,4];
332 constraint 4.0*t[2,1] = t[1,1] + t[2,0] + t[3,1] + t[2,2];
333 constraint 4.0*t[2,2] = t[1,2] + t[2,1] + t[3,2] + t[2,3];
334 constraint 4.0*t[2,3] = t[1,3] + t[2,2] + t[3,3] + t[2,4];
335 constraint 4.0*t[3,1] = t[2,1] + t[3,0] + t[4,1] + t[3,2];
336 constraint 4.0*t[3,2] = t[2,2] + t[3,1] + t[4,2] + t[3,3];
337 constraint 4.0*t[3,3] = t[2,3] + t[3,2] + t[4,3] + t[3,4];
338
33925个元素的2维数组被转换成一维数组,而且下标也会相应改变: 所以 :mzn:`[i,j]` 下标会变成
340:mzn:`[i * 5 + j + 1]` .
341
342.. code-block:: minizinc
343
344 array [1..25] of var float: t;
345 constraint 4.0*t[7] = t[2] + t[6] + t[12] + t[8];
346 constraint 4.0*t[8] = t[3] + t[7] + t[13] + t[9];
347 constraint 4.0*t[9] = t[4] + t[8] + t[14] + t[10];
348 constraint 4.0*t[12] = t[7] + t[11] + t[17] + t[13];
349 constraint 4.0*t[13] = t[8] + t[12] + t[18] + t[14];
350 constraint 4.0*t[14] = t[9] + t[13] + t[19] + t[15];
351 constraint 4.0*t[17] = t[12] + t[16] + t[22] + t[18];
352 constraint 4.0*t[18] = t[13] + t[17] + t[23] + t[19];
353 constraint 4.0*t[19] = t[14] + t[18] + t[24] + t[20];
354
355
356具体化
357-----------
358
359.. index::
360 single: reification
361
362FlatZinc模型包含了只有变量和参数声明,和一系列原始的约束. 所以当我们在MiniZinc用
363布尔连接符而不是析取式来建模时,需要进行一些处理.
364处理使用连接符而不只是析取式来构建的复杂公式,其核心的方法是具体化.
365具体化一个约束 :math:`c` 创建新的约束等价于 :math:`b \leftrightarrow c` ,
366即如果约束满足则布尔变量 :math:`b` 的值是 :mzn:`true` , 否则为 :mzn:`false` .
367
368当我们有能力 *具体化* 约束,对待复杂公式的方式跟数学表达式并无不同. 我们为子表达式创建了一个名称和一个展平的约束来约束子表达式的数值.
369
370考虑以下任务调度例子 :numref:`ex-jobshop` 中出现在约束表达式:
371
372.. code-block:: minizinc
373
374 constraint %% 保证任务之间没有重叠
375 forall(j in 1..tasks) (
376 forall(i,k in 1..jobs where i < k) (
377 s[i,j] + d[i,j] <= s[k,j] \/
378 s[k,j] + d[k,j] <= s[i,j]
379 ) );
380
381对于数据文件
382
383.. code-block:: minizinc
384
385 jobs = 2;
386 tasks = 3;
387 d = [| 5, 3, 4 | 2, 6, 3 |]
388
389然后展开过程生成
390
391.. code-block:: minizinc
392
393 constraint s[1,1] + 5 <= s[2,1] \/ s[2,1] + 2 <= s[1,1];
394 constraint s[1,2] + 3 <= s[2,2] \/ s[2,2] + 6 <= s[1,2];
395 constraint s[1,3] + 4 <= s[2,3] \/ s[2,3] + 3 <= s[1,3];
396
397具体化在析取式中出现的约束创建新的布尔变量来定义每个表达式的数值.
398
399.. code-block:: minizinc
400
401 array[1..2,1..3] of var 0..23: s;
402 constraint BOOL01 <-> s[1,1] + 5 <= s[2,1];
403 constraint BOOL02 <-> s[2,1] + 2 <= s[1,1];
404 constraint BOOL03 <-> s[1,2] + 3 <= s[2,2];
405 constraint BOOL04 <-> s[2,2] + 6 <= s[1,2];
406 constraint BOOL05 <-> s[1,3] + 4 <= s[2,3];
407 constraint BOOL06 <-> s[2,3] + 3 <= s[1,3];
408 constraint BOOL01 \/ BOOL02;
409 constraint BOOL03 \/ BOOL04;
410 constraint BOOL05 \/ BOOL06;
411
412每个基础的约束现在会映射到FlatZinc形式下.
413注意到二维数组 :mzn:`s` 是如何映射到一维数组里面的.
414
415.. code-block:: minizinc
416
417 array[1..6] of var 0..23: s;
418 constraint int_lin_le_reif([1, -1], [s[1], s[4]], -5, BOOL01);
419 constraint int_lin_le_reif([-1, 1], [s[1], s[4]], -2, BOOL02);
420 constraint int_lin_le_reif([1, -1], [s[2], s[5]], -3, BOOL03);
421 constraint int_lin_le_reif([-1, 1], [s[2], s[5]], -6, BOOL04);
422 constraint int_lin_le_reif([1, -1], [s[3], s[6]], -4, BOOL05);
423 constraint int_lin_le_reif([-1, 1], [s[3], s[6]], -3, BOOL06);
424 constraint array_bool_or([BOOL01, BOOL02], true);
425 constraint array_bool_or([BOOL03, BOOL04], true);
426 constraint array_bool_or([BOOL05, BOOL06], true);
427
428:mzn:`int_lin_le_reif` 是线性约束 :mzn:`int_lin_le` 的具体化形式.
429
430大多数FlatZinc基本约束 :math:`p(\bar{x})` 有一个具体化形式 :math:`\mathit{p\_reif}(\bar{x},b)` ,
431它利用最后额外的参数 :math:`b` 来定义一个约束 :math:`b \leftrightarrow p(\bar{x})` .
432定义像 :mzn:`int_plus` 和 :mzn:`int_plus` 的函数式关系的FlatZinc基本约束
433不需要支持具体化. 反而,有结果的函数的等式被具体化了.
434
435具体化的另外一个重要作用出现在当我们使用强制转换函数 :mzn:`bool2int` (可能是显式地或者隐式地把布尔表达式使用成整数表达式使用). 平整过程将创建一个布尔变量来保存一个布尔表达式参数,
436以及一个整型变量 (限制到 :mzn:`0..1` )来保存这个数值.
437
438考虑 :numref:`ex-magic-series` 中的魔术序列问题.
439
440.. literalinclude:: examples/magic-series.mzn
441 :language: minizinc
442 :end-before: solve satisfy
443
444给定 :mzn:`n = 2` , 展开创造了
445
446.. code-block:: minizinc
447
448 constraint s[0] = bool2int(s[0] = 0) + bool2int(s[1] = 0);
449 constraint s[1] = bool2int(s[0] = 1) + bool2int(s[1] = 1);
450
451和展平创造了
452
453.. code-block:: minizinc
454
455 constraint BOOL01 <-> s[0] = 0;
456 constraint BOOL03 <-> s[1] = 0;
457 constraint BOOL05 <-> s[0] = 1;
458 constraint BOOL07 <-> s[1] = 1;
459 constraint INT02 = bool2int(BOOL01);
460 constraint INT04 = bool2int(BOOL03);
461 constraint INT06 = bool2int(BOOL05);
462 constraint INT08 = bool2int(BOOL07);
463 constraint s[0] = INT02 + INT04;
464 constraint s[1] = INT06 + INT08;
465
466最后的FlatZinc形式是
467
468.. code-block:: minizinc
469
470 var bool: BOOL01;
471 var bool: BOOL03;
472 var bool: BOOL05;
473 var bool: BOOL07;
474 var 0..1: INT02;
475 var 0..1: INT04;
476 var 0..1: INT06;
477 var 0..1: INT08;
478 array [1..2] of var 0..2: s;
479 constraint int_eq_reif(s[1], 0, BOOL01);
480 constraint int_eq_reif(s[2], 0, BOOL03);
481 constraint int_eq_reif(s[1], 1, BOOL05);
482 constraint int_eq_reif(s[2], 1, BOOL07);
483 constraint bool2int(BOOL01, INT02);
484 constraint bool2int(BOOL03, INT04);
485 constraint bool2int(BOOL05, INT06);
486 constraint bool2int(BOOL07, INT08);
487 constraint int_lin_eq([-1, -1, 1], [INT02, INT04, s[1]], 0);
488 constraint int_lin_eq([-1, -1, 1], [INT06, INT08, s[2]], 0);
489 solve satisfy;
490
491谓词
492----------
493
494MiniZinc支持许多不同求解器的的一个重要的因素是全局约束 (还有真正的FlatZinc约束)可以根据不同的
495求解器专业化.
496
497每一个求解器生命一个谓词有时会,但有时并不会提供具体的定义. 举个例子一个求解器有一个
498内建的全局 :mzn:`alldifferent` 谓词,会包含定义
499
500.. code-block:: minizinc
501
502 predicate alldifferent(array[int] of var int:x);
503
504在全局约束库中,同时一个求解器预设的分解会有定义
505
506.. code-block:: minizinc
507
508 predicate alldifferent(array[int] of var int:x) =
509 forall(i,j in index_set(x) where i < j)(x[i] != x[j]);
510
511谓词调用 :math:`p(\bar{t})` 在平整时, 首先为每个参数项 :math:`t_i` 创建对应变量 :math:`v_i` .
512如果谓词没有定义我们只需要使用创建的参数 :math:`p(\bar{v})` 来调用谓词. 如果一个谓词
513有一个定义 :math:`p(\bar{x}) = \phi(\bar{x})` 然后我们将用谓词的定义来替换这个谓词调用 :math:`p(\bar{t})` 当中形式参数被替换为对应的参数变量, 即 :math:`\phi(\bar{v})`.
514注意到如果一个谓词调用 :math:`p(\bar{t})` 出现在具体化位置而且它没有定义,我们则
515检查我们适用这个谓词的具体化版本 :math:`\mathit{p\_reif}(\bar{x},b)` .
516
517考虑在SEND-MORE-MONEY例子 :numref:`ex-smm` 中 :mzn:`alldifferent` 约束的:
518
519.. code-block:: minizinc
520
521 constraint alldifferent([S,E,N,D,M,O,R,Y]);
522
523如果这个求解器有一个内建的 :mzn:`alldifferent` 我们只需要为这个参数创建一个新的变量, 然后在调用时替换它.
524
525.. code-block:: minizinc
526
527 array[1..8] of var 0..9: v = [S,E,N,D,M,O,R,Y];
528 constraint alldifferent(v);
529
530注意到边界分析尝试在新的数组变量上找到一个紧的边界. 建造这个数组参数的理由就是,如果我们中使用
531相同的数组两次,FlatZinc求解器不会创建它两次. 在这种情况下因为它不是使用两次,后面的转换会把 :mzn:`v` 替换成它的定义.
532
533如果求解器使用预设的定义 :mzn:`alldifferent` 呢?
534然后变量 :mzn:`v` 会正常地定义,谓词调用会被替换为一个当中变量被重命名的版本, 其中 :mzn:`v` 替换了形式参数 :mzn:`x`.
535结果的程序是
536
537.. code-block:: minizinc
538
539 array[1..8] of var 0..9: v = [S,E,N,D,M,O,R,Y];
540 constraint forall(i,j in 1..8 where i < j)(v[i] != v[j])
541
542我们可以在 :ref:`sec-unroll` 中看到.
543
544考虑到以下约束, 其中 :mzn:`alldifferent` 在一个具体化位置出现.
545
546.. code-block:: minizinc
547
548 constraint alldifferent([A,B,C]) \/ alldifferent([B,C,D]);
549
550如果求解器有 :mzn:`alldifferent` 的具体化形式, 这将会被展平为
551
552.. code-block:: minizinc
553
554 constraint alldifferent_reif([A,B,C],BOOL01);
555 constraint alldifferent_reif([B,C,D],BOOL02);
556 constraint array_bool_or([BOOL01,BOOL02],true);
557
558适用这个预设的分解,谓词替换会首先创建
559
560.. code-block:: minizinc
561
562 array[1..3] of var int: v1 = [A,B,C];
563 array[1..3] of var int: v2 = [B,C,D];
564 constraint forall(i,j in 1..3 where i<j)(v1[i] != v1[j]) \/
565 forall(i,j in 1..3 where i<j)(v2[i] != v2[j]);
566
567它最终会展平成FlatZinc形式
568
569.. code-block:: minizinc
570
571 constraint int_neq_reif(A,B,BOOL01);
572 constraint int_neq_reif(A,C,BOOL02);
573 constraint int_neq_reif(B,C,BOOL03);
574 constraint array_bool_and([BOOL01,BOOL02,BOOL03],BOOL04);
575 constraint int_neq_reif(B,D,BOOL05);
576 constraint int_neq_reif(C,D,BOOL06);
577 constraint array_bool_and([BOOL03,BOOL05,BOOL06],BOOL07);
578 constraint array_bool_or([BOOL04,BOOL07],true);
579
580注意到共同子表达式消除是如何利用具体化不等式 :mzn:`B != C` 的.
581(虽然有一个更好的转换把共同约束提升到最顶层的合取式中)
582
583.. _sec-let:
584
585Let表达式
586---------------
587
588Let表达式是MiniZinc中可用于引入新的变量的非常强大的工具.
589在展平时,let表达式被转换成变量和约束声明. 这个MiniZinc的关系语义意味着这些约束必须像在第一个包含的布尔表达式中出现.
590
591let表达式的一个重要特征是每一次它们被使用时它们都创建新的变量.
592
593考虑一下展平的代码
594
595.. code-block:: minizinc
596
597 constraint even(u) \/ even(v);
598 predicate even(var int: x) =
599 let { var int: y } in x = 2 * y;
600
601首先谓词调用被他们的定义取代.
602
603.. code-block:: minizinc
604
605 constraint (let { var int: y} in u = 2 * y) \/
606 (let { var int: y} in v = 2 * y);
607
608然后let变量会另外被重命名
609
610.. code-block:: minizinc
611
612 constraint (let { var int: y1} in u = 2 * y1) \/
613 (let { var int: y2} in v = 2 * y2);
614
615最后变量声明会被抽取到第一层
616
617.. code-block:: minizinc
618
619 var int: y1;
620 var int: y2;
621 constraint u = 2 * y1 \/ v = 2 * y2;
622
623一旦let表达式被清除我们可以像之前那样展平.
624
625记住let表达式可以定义新引入的变量 (对某些参数的确需要这样做).
626这些隐式地定义了必须满足的约束.
627
628考虑婚礼座位问题 :numref:`ex-wedding2` 的复杂的目标函数.
629
630.. code-block:: minizinc
631
632 solve maximize sum(h in Hatreds)(
633 let { var Seats: p1 = pos[h1[h]],
634 var Seats: p2 = pos[h2[h]],
635 var 0..1: same = bool2int(p1 <= 6 <-> p2 <= 6) } in
636 same * abs(p1 - p2) + (1-same) * (abs(13 - p1 - p2) + 1));
637
638为了简介我们假设只使用前两个相互敌视的人,所以
639
640.. code-block:: minizinc
641
642 set of int: Hatreds = 1..2;
643 array[Hatreds] of Guests: h1 = [groom, carol];
644 array[Hatreds] of Guests: h2 = [clara, bestman];
645
646展平的第一步是展开 :mzn:`sum` 表达式,给定(为了简洁我们保留客人名字和参数 :mzn:`Seats` ,
647在实际中他们会被他们的定义取代):
648
649.. code-block:: minizinc
650
651 solve maximize
652 (let { var Seats: p1 = pos[groom],
653 var Seats: p2 = pos[clara],
654 var 0..1: same = bool2int(p1 <= 6 <-> p2 <= 6) } in
655 same * abs(p1 - p2) + (1-same) * (abs(13 - p1 - p2) + 1))
656 +
657 (let { var Seats: p1 = pos[carol],
658 var Seats: p2 = pos[bestman],
659 var 0..1: same = bool2int(p1 <= 6 <-> p2 <= 6) } in
660 same * abs(p1 - p2) + (1-same) * (abs(13 - p1 - p2) + 1));
661
662然后每一个在let表达式的新变量会被分别命名为
663
664.. code-block:: minizinc
665
666 solve maximize
667 (let { var Seats: p11 = pos[groom],
668 var Seats: p21 = pos[clara],
669 var 0..1: same1 = bool2int(p11 <= 6 <-> p21 <= 6) } in
670 same1 * abs(p11 - p21) + (1-same1) * (abs(13 - p11 - p21) + 1))
671 +
672 (let { var Seats: p12 = pos[carol],
673 var Seats: p22 = pos[bestman],
674 var 0..1: same2 = bool2int(p12 <= 6 <-> p22 <= 6) } in
675 same2 * abs(p12 - p22) + (1-same2) * (abs(13 - p12 - p22) + 1));
676
677在let表达式的变量会被抽取到第一层,并且定义约束会被抽取到正确的层(在这里是最顶层).
678
679.. code-block:: minizinc
680
681 var Seats: p11;
682 var Seats: p21;
683 var 0..1: same1;
684 constraint p12 = pos[clara];
685 constraint p11 = pos[groom];
686 constraint same1 = bool2int(p11 <= 6 <-> p21 <= 6);
687 var Seats p12;
688 var Seats p22;
689 var 0..1: same2;
690 constraint p12 = pos[carol];
691 constraint p22 = pos[bestman];
692 constraint same2 = bool2int(p12 <= 6 <-> p22 <= 6) } in
693 solve maximize
694 same1 * abs(p11 - p21) + (1-same1) * (abs(13 - p11 - p21) + 1))
695 +
696 same2 * abs(p12 - p22) + (1-same2) * (abs(13 - p12 - p22) + 1));
697
698现在我们已经构成不需要使用let表达式的等价的MiniZinc代码,和展平可以正常进行.
699
700为了说明没有出现在最顶层的let表达式的情况,看看以下模型
701
702.. code-block:: minizinc
703
704 var 0..9: x;
705 constraint x >= 1 -> let { var 2..9: y = x - 1 } in
706 y + (let { var int: z = x * y } in z * z) < 14;
707
708我们抽取变量定义到最顶层,约束到第一个围住的布尔语境,这里是蕴含的右手边.
709
710.. code-block:: minizinc
711
712 var 0..9: x;
713 var 2..9: y;
714 var int: z;
715 constraint x >= 1 -> (y = x - 1 /\ z = x * y /\ y + z * z < 14);
716
717注意到如果我们知道定义一个变量的等式的真值不会为假,我们可以抽取它到最顶层. 这通常可以是求解大幅加快.
718
719对于上面的例子,因为 :mzn:`y` 的值域对于 :mzn:`x - 1` 并不够大, 所以约束 :mzn:`y = x - 1` 可能失败.
720不过约束 :mzn:`z = x * y` 不可以(实际上边界分析会给予 :mzn:`z` 足够大的边界来包含 :mzn:`x * y` 所有的可能值).
721一个更好的展平可以给出
722
723.. code-block:: minizinc
724
725 var 0..9: x;
726 var 2..9: y;
727 var int: z;
728 constraint z = x * y;
729 constraint x >= 1 -> (y = x - 1 /\ y + z * z < 14);
730
731现在MiniZinc编译器通过总是使引入变量声明的边界足够大,它应该可以包含所有它定义的表达式的值.
732然后在正确的语境中为let表达式加入边界约束.在上面的例子中这个结果是
733
734.. code-block:: minizinc
735
736 var 0..9: x;
737 var -1..8: y;
738 var -9..72: z;
739 constraint y = x - 1;
740 constraint z = x * y;
741 constraint x >= 1 -> (y >= 2 /\ y + z * z < 14);
742
743这个转换可以使求解更加高效,因为let变量的所有可能的复杂计算并没有被具体化.
744
745这种方法的另外一个原因是在引入变量出现在取反语境的时候它也可以被使用(只要它们有一个定义). 考虑一下与之前相似的这个例子:
746
747.. code-block:: minizinc
748
749 var 0..9: x;
750 constraint (let { var 2..9: y = x - 1 } in
751 y + (let { var int: z = x * y } in z * z) > 14) -> x >= 5;
752
753这个let表达式出现在否定语境中,不过每个引入变量都被定义了.展平后的代码是
754
755.. code-block:: minizinc
756
757 var 0..9: x;
758 var -1..8: y;
759 var -9..72: z;
760 constraint y = x - 1;
761 constraint z = x * y;
762 constraint (y >= 2 /\ y + z * z > 14) -> x >= 5;
763
764注意到作为对比的let消除方法不能给出一个正确的转换:
765
766.. code-block:: minizinc
767
768 var 0..9: x;
769 var 2..9: y;
770 var int: z;
771 constraint (y = x - 1 /\ z = x * y /\ y + z * z > 14) -> x >= 5;
772
773以上转换对于所有 :mzn:`x` 的可能值给出结果,而原来的约束除掉了 :mzn:`x = 4` 的可能性.
774
775对于在let表达式中的处理跟对定义的变量的处理是相似的. 你可以认为一个约束等价于定义一个新的布尔变量.
776新的布尔变量定义可以从最顶层中抽取出来, 而布尔保存在正确的语境下.
777
778.. code-block:: minizinc
779
780 constraint z > 1 -> let { var int: y,
781 constraint (x >= 0) -> y = x,
782 constraint (x < 0) -> y = -x
783 } in y * (y - 2) >= z;
784
785可以处理成
786
787.. code-block:: minizinc
788
789 constraint z > 1 -> let { var int: y,
790 var bool: b1 = ((x >= 0) -> y = x),
791 var bool: b2 = ((x < 0) -> y = -x),
792 constraint b1 /\ b2
793 } in y * (y - 2) >= z;
794
795然后展平成
796
797.. code-block:: minizinc
798
799 constraint b1 = ((x >= 0) -> y = x);
800 constraint b2 = ((x < 0) -> y = -x);
801 constraint z > 1 -> (b1 /\ b2 /\ y * (y - 2) >= z);