this repo has no description
dekker.one
1.. _sec-modelling:
2
3MiniZinc基本模型
4===========================
5
6.. highlight:: minizinc
7 :linenothreshold: 5
8
9在此节中，我们利用两个简单的例子来介绍一个MiniZinc模型的基本结构。
10
11第一个实例
12-----------------
13
14.. _fig-aust:
15
16.. figure:: figures/aust.*
17
18 澳大利亚各州
19
20作为我们的第一个例子，假设我们要去给 :numref:`fig-aust` 中的澳大利亚地图涂色。
21它包含了七个不同的州和地区，而每一块都要被涂一个颜色来保证相邻的区域有不同的颜色。
22
23
24.. literalinclude:: examples/aust.mzn
25 :language: minizinc
26 :caption: 一个用来给澳大利亚的州和地区涂色的MiniZinc模型 :download:`aust.mzn <examples/aust.mzn>`
27 :name: ex-aust
28
29我们可以很容易的用MiniZinc给此问题建模。此模型在 :numref:`ex-aust` 中给出。
30
31模型中的第一行是注释。注释开始于 ``%`` 来表明此行剩下的部分是注释。
32MiniZinc同时也含有C语言风格的由 ``/*`` 开始和 ``*/`` 结束的块注释。
33
34模型中的下一部分声明了模型中的变量。
35此行
36
37::
38
39 int: nc = 3;
40
41定义了一个问题的 :index:`参数` 来代表可用的颜色个数。
42在很多编程语言中，参数和变量是类似的。它们必须被声明并且指定一个类型 :index:`type`。
43在此例中，类型是 :mzn:`int`。
44通过 :index:`赋值`，它们被设了值。
45MiniZinc允许变量声明时被赋值（就像上面那一行）或者单独给出一个赋值语句。
46因此下面的表示跟上面的只一行表示是相等的
47
48::
49
50 int: nc;
51 nc = 3;
52
53和很多编程语言中的变量不一样的是，这里的参数只可以被赋 *唯一* 的值。
54如果一个参数出现在了多于一个的赋值中，就会出现错误。
55
56基本的 :index:`参数类型 <single: type; parameter>` 包括 :index:`整型 <integer>` (:mzn:`int`)，
57浮点型(:mzn:`float`)， :index:`布尔型 <Boolean>` (:mzn:`bool`) 以及 :index:`字符串型 <string>` (:mzn:`string`)。
58同时也支持数组和集合。
59
60.. index::
61 see: decision variable; variable
62
63MiniZinc模型同时也可能包含另一种类型的变量 *决策变量* 。 :index:`决策变量 <variable>` 是数学的或者逻辑的变量。
64和一般的编程语言中的参数和变量不同，建模者不需要给决策变量一个值。
65而是在开始时，一个决策变量的值是不知道的。只有当MiniZinc模型被执行的时候，
66求解系统才来决定决策变量是否可以被赋值从而满足模型中的约束。若满足，则被赋值。
67
68在我们的模型例子中，我们给每一个区域一个 *决策变量* ``wa``, ``nt``, ``sa``, ``q``, ``nsw``, ``v`` 和 ``t``。
69它们代表了会被用来填充区域的（未知）颜色。
70
71.. index::
72 single: domain
73
74对于每一个决策变量，我们需要给出变量可能的取值集合。这个被称为变量的 *定义域* 。
75定义域部分可以在 :index:`变量声明 <variable; declaration>` 的时候同时给出，
76这时决策变量的 :index:`类型` 就会从定义域中的数值的类型推断出。
77
78MiniZinc中的决策变量的类型可以为布尔型，整型，浮点型或者集合。
79同时也可以是元素为决策变量的数组。
80在我们的MiniZinc模型例子中，我们使用整型去给不用的颜色建模。通过使用 :mzn:`var` 声明，
81我们的每一个决策变量
82被声明为定义域为一个整数类型的范围表示 :mzn:`1..nc` ，
83来表明集合 :math:`\{ 1, 2, \dots, nc \}` 。
84所有数值的类型为整型，所以模型中的所有的变量是整型决策变量。
85
86.. defblock:: 标识符
87
88 用来命名参数和变量的标识符是一列由大小写字母，数字以及
89 下划线 ``_`` 字符组成的字符串。它们必须开始于一个字母字符。因此 ``myName_2`` 是一个有效的标识符。
90 MiniZinc（和Zinc）的 *关键字* 不允许被用为标识符名字。它们在 :ref:`spec-identifiers` 中被列出。
91 所有的MiniZinc *操作符* 都不能被用做标识符名字。它们在 :ref:`spec-Operators` 中被列出。
92
93MiniZinc仔细地区别了以下两种模型变量：参数和决策变量。利用决策变量创建的表达式类型比利用参数可以创建的表达式类型更局限。
94但是，在任何可以用决策变量的地方，同类型的参数变量也可以被应用。
95
96.. defblock:: 整型变量声明
97
98 一个 :index:`整型参数变量 <variable; declaration; integer>` 可以被声明为以下两种方式：
99
100 .. code-block:: minizincdef
101
102 int : <变量名>
103 <l> .. <u> : <变量名>
104
105 :mzndef:`<l>` 和 :mzndef:`<u>` 是固定的整型表达式。
106
107 一个整型决策变量被声明为以下两种方式：
108
109 .. code-block:: minizincdef
110
111 var int : <变量名>
112 var <l>..<u> : <变量名>
113
114 :mzndef:`<l>` 和 :mzndef:`<u>` 是固定的整型表达式。
115
116参数和决策变量形式上的区别在于对变量的 *实例化*。
117变量的实例化和类型的结合被叫为 :index:`类型-实例化` 。
118既然你已经开始使用MiniZinc，毫无疑问的你会看到很多 *类型-实例化* 的错误例子。
119
120.. index::
121 single: constraint
122
123模型的下一部分是 *约束* 。
124它们详细说明了决策变量想要组成一个模型的有效解必须要满足的布尔型表达式。
125在这个例子中我们有一些决策变量之间的不等式。它们规定如果两个区域是相邻的，则它们必须有不同的颜色。
126
127.. defblock:: 关系操作符
128
129 MiniZinc提供了以下关系操作符 :index:`关系操作符 <operator; relational>` ：
130
131 .. index::
132 single: =
133 single: ==
134 single: !=
135 single: <
136 single: <=
137 single: >
138 single: >=
139
140 相等 (``=`` or ``==``), 不等
141 (``!=``),
142 小于 (``<``),
143 大于 (``>``),
144 小于等于 (``<=``), and
145 和大于等于 (``>=``).
146
147模型中的下一行：
148
149::
150
151 solve satisfy;
152
153表明了它是什么类型的问题。
154在这个例子中，它是一个 :index:`满足` 问题：
155我们希望给决策变量找到一个值使得约束被满足，但具体是哪一个值却没有所谓。
156
157.. index::
158 single: output
159
160模型的最后一个部分是 *输出* 语句。它告诉MiniZinc当模型被运行并且找到一个解 :index:`解` 的时候，
161要输出什么。
162
163.. defblock:: 输出和字符串
164
165 .. index::
166 single: output
167 single: string
168 single: show
169
170 一个输出语句跟着一 *串* 字符。
171 它们通常或者是写在双引号之间的字符串常量 :index:`字符串常量 <string; literal>` 并且
172 对特殊字符用类似C语言的标记法，或者是 :mzn:`show(e)` 格式的表达式，
173 其中 :mzn:`e` 是MiniZinc表达式。例子中的 ``\n`` 代表换行符， ``\t`` 代表制表符。
174
175 数字的 :mzn:`show` 有各种不同方式的表示：
176 :mzn:`show_int(n,X)`
177 在至少$|n|$个字符里输出整型 ``X`` 的值，若 :math:`n > 0` 则右对齐，否则则左对齐；
178 :mzn:`show_float(n,d,X)` 在至少 :math:`|n|` 个字符里输出
179 浮点型 ``X`` 的值，若 :math:`n > 0` 则右对齐，否则则左对齐，并且小数点后有 :math:`d` 个字符。
180
181 :index:`字符串常量 <string; literal>` 必须在同一行中。长的字符串常量可以利用字符串连接符 ``++``
182 来分成几行。例如，字符串常量
183
184 ::
185
186 "Invalid datafile: Amount of flour is non-negative"
187
188 和字符串常量表达式
189
190 ::
191
192 "Invalid datafile: " ++
193 "Amount of flour is non-negative"
194
195 是相等的。
196
197 MiniZinc支持内插字符串 :index:`内插字符串 <string; literal; interpolated>` 。
198 表达式可以直接插入字符串常量中。 :mzn:`"\(e)"` 形式的子字符串
199 会被替代为 :mzn:`show(e)` 。例如，:mzn:`"t=\(t)\n"` 产生
200 和 :mzn:`"t=" ++ show(t) ++ "\n"` 一样的字符串。
201
202 一个模型可以包含多个输出语句。在这种情况下,所有输出会根据它们在模型中出现的顺序连接。
203
204我们可以通过点击MiniZinc IDE中的 *Run* 按钮,或者输入
205
206.. code-block:: bash
207
208 $ minizinc --solver Gecode aust.mzn
209
210来评估我们的模型。
211其中 :download:`aust.mzn <examples/aust.mzn>` 是包含我们的MiniZinc模型的文件名字。
212我们必须使用文件扩展名 ``.mzn`` 来表明一个MiniZinc模型。
213带有 ``--solver Gecode`` 选项的命令 ``minizinc`` 使用Gecode有限域求解器去评估我们的模型。如果你使用的是MiniZinc二进制发布,这个求解器实际上是预设的,所以你也可以运行 ``minizinc aust.mzn`` 。
214
215当我们运行上面的命令后，我们得到如下的结果：
216
217.. code-block:: none
218
219 wa=2 nt=3 sa=1
220 q=2 nsw=3 v=2
221 t=1
222 ----------
223
224
225.. index::
226 single: solution; separator ----------
227
22810个破折号 ``----------`` 这行是自动被MiniZinc输出的，用来表明一个解已经被找到。
229
230算术优化实例
231----------------------------------
232
233我们的第二个例子来自于要为了本地的校园游乐会烤一些蛋糕的需求。
234我们知道如何制作两种蛋糕。 \footnote{警告: 请不要在家里使用这些配方制作}
235一个香蕉蛋糕的制作需要250克自发酵的面粉，2个捣碎的香蕉，75克糖和100克黄油。
236一个巧克力蛋糕的制作需要200克自发酵的面粉，75克可可粉，150克糖和150克黄油。
237一个巧克力蛋糕可以卖\$4.50，一个香蕉蛋糕可以卖\$4.00。我们一共有4千克的自发酵面粉，
2386个香蕉，2千克的糖，500克的黄油和500克的可可粉。
239问题是对每一种类型的蛋糕，我们需要烤多少给游乐会来得到最大的利润。
240一个可能的MiniZinc模型在 :numref:`ex-cakes` 中给出。
241
242.. literalinclude:: examples/cakes.mzn
243 :language: minizinc
244 :caption: 决定为了校园游乐会要烤多少香蕉和巧克力蛋糕的模型。 (:download:`cakes.mzn <examples/cakes.mzn>`)
245 :name: ex-cakes
246
247.. index::
248 single: expression; arithmetic
249
250第一个新特征是 *arithmetic expressions* 的使用。
251
252.. defblock:: 整数算术操作符
253
254 .. index::
255 single: operator; integer
256 single: +
257 single: -
258 single: div
259 single: *
260 single: mod
261
262 MiniZinc提供了标准的整数算术操作符。
263 加 (``+``),
264 减 (``-``),
265 乘 (``*``),
266 整数除 (:mzn:`div`)
267 和
268 整数模 (:mzn:`mod`).
269 同时也提供了一元操作符 ``+`` 和 ``-`` 。
270
271 整数模被定义为输出和被除数 :math:`a` 一样正负的 :math:`a` :mzn:`mod` :math:`b` 值。整数除被定义为使得
272 :math:`a = b ` ``*`` :math:`(a` :mzn:`div` :math:`b) + (a` :mzn:`mod` :math:`b)` 值。
273
274 MiniZinc 提供了标准的整数函数用来取绝对值 (:mzn:`abs`) 和幂函数 (:mzn:`pow`).
275 例如 :mzn:`abs(-4)` 和 :mzn:`pow(2,5)` 分别求得数值
276 ``4`` 和 ``32`` 。
277
278 算术常量的语法是相当标准的。整数常量可以是十进制，十六进制或者八进制。例如 ``0``, ``5``,
279 ``123``, ``0x1b7``, ``0o777`` 。
280
281.. index::
282 single: optimization
283 single: objective
284 single: maximize
285 single: minimize
286
287例子中的第二个新特征是优化。这行
288
289::
290
291 solve maximize 400 * b + 450 * c;
292
293指出我们想找一个可以使solve语句中的表达式（我们叫做 *目标* ）最大化的解。
294这个目标可以为任何类型的算术表达式。我们可以把关键字 :mzn:`maximize`
295换为 :mzn:`minimize` 来表明一个最小化问题。
296
297当我们运行上面这个模型时，我们得到以下的结果：
298
299.. code-block:: none
300
301 no. of banana cakes = 2
302 no. of chocolate cakes = 2
303 ----------
304 ==========
305
306.. index::
307 single: solution; end `==========`
308
309一旦系统证明了一个解是最优解，这一行 ``==========`` 在最优化问题中会自动被输出。
310
311.. index::
312 single: data file
313
314数据文件和谓词
315------------------------
316
317此模型的一个缺点是如果下一次我们希望解决一个相似的问题，即我们需要为学校烤蛋糕（这是经常发生的），
318我们需要改变模型中的约束来表明食品间拥有的原料数量。如果我们想重新利用此模型，我们最好使得每个原料的数量作为
319模型的参数，然后在模型的最上层设置它们的值。
320
321更好的办法是在一个单独的 *数据文件* 中设置这些参数的值。
322MiniZinc（就像很多其他的建模语言一样）允许使用数据文件来设置在原始模型中声明的
323参数的值。
324通过运行不同的数据文件，使得同样的模型可以很容易地和不同的数据一起使用。
325
326数据文件的文件扩展名必须是 ``.dzn`` ，来表明它是一个MiniZinc数据文件。
327一个模型可以被任何多个数据文件运行（但是每个变量/参数在每个文件中只能被赋一个值）
328
329.. literalinclude:: examples/cakes2.mzn
330 :language: minizinc
331 :caption: 独立于数据的用来决定为了校园游乐会要烤多少香蕉和巧克力蛋糕的模型。(:download:`cakes2.mzn <examples/cakes2.mzn>`)
332 :name: ex-cakes2
333
334我们的新模型在 :numref:`ex-cakes2` 中给出。
335我们可以用下面的命令来运行
336
337.. code-block: bash
338
339 $ minizinc cakes2.mzn pantry.dzn
340
341数据文件 :download:`pantry.dzn <examples/pantry.dzn>` 在 :numref:`fig-pantry1` 中给出。我们得到和 :download:`cakes.mzn <examples/cakes.mzn>` 同样的结果。
342运行下面的命令
343
344.. code-block:: bash
345
346 $ minizinc cakes2.mzn pantry2.dzn
347
348利用另外一个 :numref:`fig-pantry2` 中定义的数据集，我们得到如下结果
349
350.. code-block:: none
351
352 no. of banana cakes = 3
353 no. of chocolate cakes = 8
354 ----------
355 ==========
356
357如果我们从 :download:`cakes.mzn <examples/cakes.mzn>` 中去掉输出语句，MiniZinc会使用默认的输出。
358这种情况下得到的输出是
359
360.. code-block:: none
361
362 b = 3;
363 c = 8;
364 ----------
365 ==========
366
367.. defblock:: 默认输出
368
369 一个没有输出语句的MiniZinc模型会给每一个决策变量以及它的值一个输出行，除非决策变量已经在声明的时候被赋了一个表达式。
370 注意观察此输出是如何呈现一个正确的数据文件格式的。
371
372.. literalinclude:: examples/pantry.dzn
373 :language: minizinc
374 :caption: :download:`cakes2.mzn <examples/cakes2.mzn>` 的数据文件例子 (:download:`pantry.dzn <examples/pantry.dzn>`)
375 :name: fig-pantry1
376
377.. literalinclude:: examples/pantry2.dzn
378 :language: minizinc
379 :caption: :download:`cakes2.mzn <examples/cakes2.mzn>` 的数据文件例子 (:download:`pantry2.dzn <examples/pantry2.dzn>`)
380 :name: fig-pantry2
381
382通过使用 :index:`命令行标示 <data file;command line>`
383``-D`` *string* ，
384小的数据文件可以被直接输入而不是必须要创建一个 ``.dzn`` 文件，
385其中 *string* 是数据文件里面的内容。
386
387.. code-block:: bash
388
389 $ minizinc cakes2.mzn -D \
390 "flour=4000;banana=6;sugar=2000;butter=500;cocoa=500;"
391
392会给出和
393
394.. code-block:: bash
395
396 $ minizinc cakes2.mzn pantry.dzn
397
398一模一样的结果。
399
400数据文件只能包含给模型中的决策变量和参数赋值的语句。
401
402.. index::
403 single: assert
404
405防御性编程建议我们应该检查数据文件中的数值是否合理。
406在我们的例子中，检查所有原料的份量是否是非负的并且若不正确则产生一个运行错误，这是明智的。
407MiniZinc提供了一个内置的布尔型操作符 *断言* 用来检查参数值。格式是 :mzn:`assert(B,S)` 。
408布尔型表达式 ``B`` 被检测。若它是假的，运行中断。此时字符串表达式 ``S`` 作为错误信息被输出。
409如果我们想当面粉的份量是负值的时候去检测出并且产生合适的错误信息，我们可以直接加入下面的一行
410
411::
412
413 constraint assert(flour >= 0,"Amount of flour is non-negative");
414
415到我们的模型中。注意 *断言* 表达式是一个布尔型表达式，所以它被看做是一种类型的约束。我们可以加入类似的行来检测其他原料的份量是否是非负值。
416
417实数求解
418-------------------
419
420MiniZinc also supports "real number" constraint solving using
421floating point variables and constraints. Consider a problem of taking out a short loan
422for one year to be repaid in 4 quarterly instalments.
423A model for this is shown in :numref:`ex-loan`. It uses a simple interest
424calculation to calculate the balance after each quarter.
425
426通过使用浮点数求解，MiniZinc也支持“实数”约束求解。考虑一个要在4季度分期偿还的一年短期贷款问题。
427此问题的一个模型在 :numref:`ex-loan` 中给出。它使用了一个简单的计算每季度结束后所欠款的利息计算方式。
428
429.. literalinclude:: examples/loan.mzn
430 :language: minizinc
431 :caption: 确定一年借款每季度还款关系的模型(:download:`loan.mzn <examples/loan.mzn>`)
432 :name: ex-loan
433
434注意我们声明了一个浮点型变量 ``f`` ，它和整型变量很类似。只是这里我们
435使用关键字 :mzn:`float` 而不是 :mzn:`int` 。
436
437我们可以用同样的模型来回答一系列不同的问题。第一个问题是：如果我以利息
4384\%借款\$1000并且每季度还款\$260，我最终还欠款多少？这个问题在数据文件 :download:`loan1.dzn <examples/loan1.dzn>` 中被编码。
439
440由于我们希望用实数求解，我们需要使用一个可以支持这种问题类型的求解器。Gecode(Minizinc捆绑二进制发布预设的求解器)支持浮点型变量,一个混合整数线性求解器可能更加适合这种类型的问题。
441MiniZinc发布包含了这样的一个求解器。我们可以通过从求解器IDE菜单( *Run* 按钮下面的三角形)选择 ``COIN-BC`` 来使用, 或者在命令行中运行命令 ``minizinc --solver cbc`` :
442
443.. code-block:: bash
444
445 $ minizinc --solver cbc loan.mzn loan1.dzn
446
447输出是
448
449.. code-block:: none
450
451 Borrowing 1000.00 at 4.0% interest, and repaying 260.00
452 per quarter for 1 year leaves 65.78 owing
453 ----------
454
455第二个问题是如果我希望用4\%的利息来借款\$1000并且在最后的时候一点都不欠款，我需要在每季度还款多少？
456这个问题在数据文件 :download:`loan2.dzn <examples/loan2.dzn>` 中被编码。
457运行命令
458
459.. code-block:: bash
460
461 $ minizinc --solver cbc loan.mzn loan2.dzn
462
463后的输出是
464
465.. code-block:: none
466
467 Borrowing 1000.00 at 4.0% interest, and repaying 275.49
468 per quarter for 1 year leaves 0.00 owing
469 ----------
470
471第三个问题是如果我可以每个季度返还\$250, 我可以用4\%的利息来借款多少并且在最后的时候一点都不欠款？
472这个问题在数据文件 :download:`loan3.dzn <examples/loan3.dzn>` 中被编码。
473运行命令
474
475.. code-block:: bash
476
477 $ minizinc --solver cbc loan.mzn loan3.dzn
478
479后的输出是
480
481.. code-block:: none
482
483 Borrowing 907.47 at 4.0% interest, and repaying 250.00
484 per quarter for 1 year leaves 0.00 owing
485 ----------
486
487.. literalinclude:: examples/loan1.dzn
488 :language: minizinc
489 :caption: :download:`loan.mzn <examples/loan.mzn>` 的数据文件例子(:download:`loan1.dzn <examples/loan1.dzn>`)
490
491.. literalinclude:: examples/loan2.dzn
492 :language: minizinc
493 :caption: :download:`loan.mzn <examples/loan.mzn>` 的数据文件例子(:download:`loan2.dzn <examples/loan2.dzn>`)
494
495.. literalinclude:: examples/loan3.dzn
496 :language: minizinc
497 :caption: :download:`loan.mzn <examples/loan.mzn>` 的数据文件例子(:download:`loan3.dzn <examples/loan3.dzn>`)
498
499
500.. defblock:: 浮点算术操作符
501
502 .. index:
503 single: operator; float
504 single: +
505 single: -
506 single: *
507 single: /
508 single: abs
509 single: sqrt
510 single: ln
511 single: log2
512 single: log10
513 single: exp
514 single: sin
515 single: cos
516 single: tan
517 single: asin
518 single: acos
519 single: atan
520 single: sinh
521 single: cosh
522 single: tanh
523 single: asinh
524 single: acosh
525 single: atanh
526 single: pow
527
528 MiniZinc提供了标准的浮点算术操作符:
529 加 (``+``),
530 减 (``-``),
531 乘 (``*``)
532 和浮点除 (``/``)。
533 同时也提供了一元操作符 ``+`` 和 ``-`` 。
534
535 MiniZinc不会自动地强制转换整数为浮点数。内建函数 :mzn:`int2float` 被用来达到此目的。注意强制转换的一个后果是表达式 :mzn:`a / b` 总是被认为是一个浮点除。 如果你需要一个整数除,请确定使用 :mzn:`div` 操作符。
536
537 MiniZinc同时也包含浮点型函数来计算:
538 绝对值 (``abs``),
539 平方根 (``sqrt``),
540 自然对数 (``ln``),
541 底数为2的对数 (``log2``),
542 底数为10的对数 (``log10``),
543 $e$的幂 (``exp``),
544 正弦 (``sin``),
545 余弦 (``cos``),
546 正切 (``tan``),
547 反正弦 (``asin``),
548 反余弦 (``acos``),
549 反正切 (``atan``),
550 双曲正弦 (``sinh``),
551 双曲余弦 (``cosh``),
552 双曲正切 (``tanh``),
553 双曲反正弦 (``asinh``),
554 双曲反余弦 (``acosh``),
555 双曲反正切 (``atanh``),
556 和唯一的二元函数次方 (``pow``)，其余的都是一元函数。
557
558 算术常量的语法是相当标准的。浮点数常量的例子有 ``1.05``， ``1.3e-5`` 和 ``1.3E+5`` 。
559
560.. \pjs{Should do multiple solutions????}
561
562模型的基本结构
563--------------------------
564
565我们现在可以去总结MiniZinc模型的基本结构了。
566它由多个项组成，每一个在其最后都有一个分号 ``;`` 。
567项可以按照任何顺序出现。例如，标识符在被使用之前不需要被声明。
568
569有八种类型的项 :index:`items <item>` 。
570
571- :index:`引用项 <item; include>` 允许另外一个文件的内容被插入模型中。
572 它们有以下形式：
573
574 .. code-block:: minizincdef
575
576 include <文件名>;
577
578 其中 :mzndef:`<文件名>` 是一个字符串常量。
579 它们使得大的模型可以被分为小的子模型以及包含库文件中定义的约束。
580 我们会在 :numref:`ex-smm` 中看到一个例子。
581
582- :index:`变量声明 <item; variable declaration>` 声明新的变量。
583 这种变量是全局变量，可以在模型中的任何地方被提到。
584 变量有两种。在模型中被赋一个固定值的参数变量以及只有在模型被求解的时候才会
585 被赋值的决策变量。
586 我们称参数是 :index:`固定的` ，决策变量是 :index:`不固定的` 。
587 变量可以选择性地被赋一个值来作为声明的一部分。形式是：
588
589 .. index:
590 single: expression; type-inst
591 single: par
592 single: var
593
594 .. code-block:: minizincdef
595
596 <类型-实例化 表达式>: <变量> [ = ] <表达式>;
597
598 :mzndef:`<类型-实例化 表达式>`
599 给了变量的类型和实例化。 这些是MiniZinc比较复杂的其中一面。
600 用 :mzn:`par` 来实例化声明
601 参数，用 :mzn:`var` 来实例化声明决策变量。
602 如果没有明确的实例化声明，则变量是一个参数。类型可以为基类型，一个 :index:`整数或者浮点数范围 <range>`，或者一个数组或集合。
603 基类型有
604 :mzn:`float`,
605 :mzn:`int`,
606 :mzn:`string`,
607 :mzn:`bool`,
608 :mzn:`ann`
609 。其中只有
610 :mzn:`float`, :mzn:`int` and :mzn:`bool` 可以被决策变量使用。
611 基类型 :mzn:`ann` 是一个 :index:`注解` --
612 我们会在 :ref:`sec-search` 中讨论注解。
613 :index:`整数范围表达式 <range; integer>` 可以被用来代替类型 :mzn:`int`.
614 类似的， :index:`浮点数范围表达式 <range; float>`
615 可以被用来代替类型 :mzn:`float` 。
616 这些通常被用来定义一个整型决策变量的定义域，但也可以被用来限制一个整型参数的范围。
617 变量声明的另外一个用处是定义 :index:`枚举类型`, ---我们会在 :ref:`sec-enum` 中讨论。
618
619- :index:`赋值项 <item; assignment>` 给一个变量赋一个值。它们有以下形式：
620
621 .. code-block:: minizincdef
622
623 <变量> = <表达式>;
624
625 数值可以被赋给决策变量。在这种情况下，赋值相当于加入 :mzndef:`constraint <变量> = <表达式>` ;
626
627- :index:`约束项 <item; constraint>` 是模型的核心。它们有以下形式：
628
629 .. code-block:: minizincdef
630
631 constraint <布尔型表达式>;
632
633 我们已经看到了使用算术比较的简单约束以及内建函数 :mzn:`assert` 操作符。 在下一节我们会看到更加复杂的约束例子。
634
635- :index:`求解项 <item; solve>` 详细说明了到底要找哪种类型的解。
636 正如我们看到的，它们有以下三种形式：
637
638 .. code-block:: minizincdef
639
640 solve satisfy;
641 solve maximize <算术表达式>;
642 solve minimize <算术表达式>;
643
644 一个模型必须有且只有一个求解项。
645
646- :index:`输出项 <item; output>` 用来恰当的呈现模型运行后的结果。
647 它们有下面的形式：
648
649 .. code-block:: minizincdef
650
651 output [ <字符串表达式>, ..., <字符串表达式> ];
652
653 如果没有输出项，MiniZinc会默认输出所有没有被以赋值项的形式赋值的决策变量值。
654
655- :index:`枚举类型声明 <item; enum>`.
656 我们会在 :ref:`sec-arrayset` 和 :ref:`sec-enum` 中讨论。
657
658- :index:`谓词函数和测试项 <item; predicate>` 被用来定义新的约束，函数和布尔测试。我们会在 :ref:`sec-predicates` 中讨论。
659
660
661- :index:`注解项 <item; annotation>` 用来定义一个新的注解。我们会在 :ref:`sec-search` 中讨论。