this repo has no description
dekker.one
1.. _sec-flattening:
2
3FlatZinc y Flattening
4=======================
5
6.. \pjs{Maybe show the toolset at this point?}
7
8
9Los solucionadores de restricciones no son compatibles directamente con los modelos MiniZinc. Sino que para ejecutar un modelo MiniZinc se debe de traducir en un subconjunto simple de MiniZinc llamado FlatZinc. FlatZinc refleja el hecho de que la mayoría de los solucionadores de restricciones solo resuelven problemas de satisfacción de la forma :math:`\bar{exists } c_1 \wedge \cdots \wedge c_m` o problemas de optimización de la forma :math:`\text {minimize} z \text{ sujeto a } c_1 \wedge \cdots \wedge c_m`,
10donde :math:`c_i` son restricciones primitivas y :math:`z` es un entero o expresión flotante en una forma restringida.
11
12.. index::
13 single: mzn2fzn
14
15
16La herramienta ``mzn2fzn`` toma un modelo de MiniZinc y los archivos de datos, posteriormente crea un modelo FlatZinc aplanado que es equivalente al modelo MiniZinc con los datos dados, y que aparece en la forma restringida discutida anteriormente.
17Normalmente, la construcción de un modelo de FlatZinc que se envía a un solucionador está oculta para el usuario, pero puede ver el resultado de un modelo ``model.mzn`` con sus datos ``data.dzn`` de la siguiente manera:
18
19.. code-block:: bash
20
21 mzn2fzn model.mzn data.dzn
22
23El cual crea un modelo FlatZinc llamado ``model.fzn``.
24
25En este capítulo, exploramos el proceso de traducción de MiniZinc a FlatZinc.
26
27
28
29Flattening Expressiones
30-----------------------
31
32Las restricciones del solucionador subyacente significan que las expresiones complejas en MiniZinc deben *flattened* (aplanarse o aplanar) para usar solo conjunciones de restricciones primitivas que no contienen por sí mismas términos estructurados.
33
34Considere el siguiente modelo para asegurarse de que dos círculos en un recuadro rectangular no se superpongan:
35
36.. literalinclude:: examples/cnonoverlap_es.mzn
37 :language: minizinc
38 :caption: Modelado de no superposición de dos círculos (:download:`cnonoverlap_es.mzn <examples/cnonoverlap_es.mzn>`).
39 :name: fig-nonoverlap
40
41
42Simplificación y Evaluación
43~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
44
45Dado el siguiente archivo de datos:
46
47.. code-block:: minizinc
48
49 width = 10.0;
50 height = 8.0;
51 r1 = 2.0;
52 r2 = 3.0;
53
54La traducción a FlatZinc primero simplifica el modelo reemplazando todos los parámetros por sus valores y evaluando cualquier expresión fija.
55Después de esta simplificación, los valores de los parámetros ya no son necesarios.
56Una excepción a esto, son las grandes matrices de valores paramétricos. Si se usan más de una vez, el parámetro se conserva para evitar la duplicación expresiones grandes.
57
58
59Después de la simplificación, las partes de declaraciones de variables y parámetros del modelo de :numref:`fig-nonoverlap` se transforman en
60
61.. literalinclude:: examples/cnonoverlap_es.fzn
62 :language: minizinc
63 :start-after: % Variables
64 :end-before: %
65
66.. _sec-flat-sub:
67
68
69
70Definiendo Subexpresiones
71~~~~~~~~~~~~~~~~~~~~~~~~~
72
73Ahora, ningún solucionador de restricciones maneja directamente expresiones de restricciones complejas como la de :numref:`fig-nonoverlap`. En cambio, cada subexpresión en la expresión es nombrada, y posteriormente creamos una restricción para construir el valor de cada expresión. Examinemos las subexpresiones de la expresión de restricción.
74:mzn:`(x1 - x2)` es una subexpresión, si nombramos :mzn:`FLOAT01` podemos definirlo como :mzn:`constraint FLOAT01 = x1 - x2;`. Observe que esta expresión aparece dos veces en el modelo. Solo necesitamos calcular el valor una vez, luego podemos reutilizarlo. Esto se llama *eliminación de subexpresiones comunes*. La subexpresión :mzn:`(x1 - x2) * (x1 - x2)` se puede llamar :mzn:`FLOAT02` y podemos definirla como :mzn:`constraint FLOAT02 = FLOAT01 * FLOAT01;`. Podemos nombrar de forma similar :mzn:`restricción FLOAT03 = y1 - y2;` y :mzn:`restricción FLOAT04 = FLOAT03 * FLOAT03;` y finalmente :mzn:`restricción FLOAT05 = FLOAT02 * FLOAT04;`. La restricción de desigualdad se convierte en :mzn:`restricción FLOAT05> = 25.0;` desde :mzn:`(r1 + r2) * (r1 + r2)` se calcula como :mzn:`25.0`.
75
76La restricción aplanada es por lo tanto:
77
78.. code-block:: minizinc
79
80 constraint FLOAT01 = x1 - x2;
81 constraint FLOAT02 = FLOAT01 * FLOAT01;
82 constraint FLOAT03 = y1 - y2;
83 constraint FLOAT04 = FLOAT03 * FLOAT03;
84 constraint FLOAT05 = FLOAT02 * FLOAT04;
85 constraint FLOAT05 >= 25.0
86
87.. _sec-flat-fzn:
88
89
90Forma de restricciones FlatZinc
91~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
92
93El flatening como su paso final, convierte la forma de la restricción en una forma estándar de FlatZinc que siempre es :math:`p(a_1, \ldots, a_n)`, donde
94:mzn:`p` es el nombre de la restricción primitiva y :math:`a_1, \ldots, a_n` son los argumentos.
95FlatZinc intenta usar un mínimo de diferentes formas de restricción, por ejemplo, la restricción :mzn:`FLOAT01 = x1 - x2` se reescribe primero como :mzn:`FLOAT01 + x2 = x1` y luego se genera usando la restricción primitiva:mzn:`float_plus`.
96La forma de restricción resultante es la siguiente:
97
98.. literalinclude:: examples/cnonoverlap_es.fzn
99 :language: minizinc
100 :start-after: % Restricciones
101 :end-before: %
102
103Análisis de límites
104~~~~~~~~~~~~~~~~~~~
105
106Todavía nos falta una cosa, las declaraciones de las variables introducidas :mzn:`FLOAT01`, ..., :mzn:`FLOAT05`. Si bien estos podrían simplemente declararse como :mzn:`var float`, para facilitar la tarea del solucionador MiniZinc intenta determinar los límites superiores e inferiores de las variables recién introducidas, mediante un simple análisis de límites.
107Por ejemplo desde :mzn:`FLOAT01 = x1 - x2` y :math:`2.0 \leq` :mzn:`x1` :math:`\leq 8.0` y :math:`3.0 \leq` :mzn:`x2`
108:math:`\leq 7.0` luego podemos ver que
109:math:`-5.0 \leq` :mzn:`FLOAT0` :math:`\leq 5.0`. Dada esta información, podemos ver que
110:math:`-25.0 \leq` :mzn:`FLOAT02` :math:`\leq 25.0` (aunque tenga en cuenta que si reconociéramos que la multiplicación era en realidad una cuadratura podríamos dar mucho límites más precisos :math:`0.0 \leq` :mzn:`FLOAT02` :math:`\leq 25.0`).
111
112El lector alerta puede haber notado una discrepancia entre la forma aplanada de las restricciones en :ref:`sec-flat-sub` y :ref:`sec-flat-fzn`. En este último, no hay restricción de desigualdad. Como las desigualdades unarias pueden representarse completamente por los límites de una variable, la desigualdad fuerza al límite inferior de :mzn:`FLOAT05` a ser :mzn:`25.0` y luego es redundante. La forma aplanada final del modelo de :numref:`fig-nonoverlap` es:
113
114.. literalinclude:: examples/cnonoverlap_es.fzn
115 :language: minizinc
116
117Objetivos
118~~~~~~~~~~
119
120MiniZinc aplana los objetivos de minimización o maximización al igual que las restricciones. La expresión objetivo se aplana y se crea una variable para ella, al igual que para otras expresiones. En la salida de FlatZinc, el elemento de resolver siempre está en una sola variable. Ver :ref:`sec-let` para un ejemplo.
121
122.. \pjs{Do we need an example here?}
123
124Expresiones lineales
125--------------------
126
127Una de las restricciones más importantes, ampliamente utilizada para el modelado, son las restricciones lineales de la forma
128
129.. math:: a_1 x_1 + \cdots + a_n x_n \begin{array}[c]{c} = \\ \leq \\ < \end{array} a_0
130
131En donde :math:`a_i` son constantes de coma flotante o entero, y :math:`x_i` son variables enteras o de coma flotante. Son altamente expresivos, y son la única clase de restricción soportada por solucionadores de restricciones de programación lineal (entero). El traductor de MiniZinc a FlatZinc intenta crear restricciones lineales, en lugar de dividir las restricciones lineales en muchas subexpresiones.
132
133.. \pjs{Maybe use the equation from SEND-MORE-MONEY instead?}
134
135.. literalinclude:: examples/linear_es.mzn
136 :language: minizinc
137 :caption: Un modelo MiniZinc para ilustrar el aplanamiento de restricciones lineales (:download:`linear_es.mzn <examples/linear_es.mzn>`).
138 :name: fig-lflat
139
140Considere el modelo que se muestra en :numref:`fig-lflat`. En lugar de crear variables para todas las subexpresiones :math:`3 * x`, :math:`3 * x - y`, :math:`x * z`, :math:`3 * x - y + x * z `, :math:`x + y + z`, :math:`d * (x + y + z)`, :math:`19 + d * (x + y + z)`, y :math:`19 + d * (x + y + z) - 4 * d` la traducción intentará crear una restricción lineal grande que capture la mayor cantidad posible de la restricción en una única restricción FlatZinc.
141
142
143El flatening crea expresiones lineales como una sola unidad en lugar de generar variables intermedias para cada subexpresión. También simboliza la expresión lineal creada. La extracción de la expresión lineal de las restricciones conduce a:
144
145.. code-block:: minizinc
146
147 var 0..80: INT01;
148 constraint 4*x + z + INT01 <= 23;
149 constraint INT01 = x * z;
150
151Observe cómo la *expresión no lineal* :math:`x \times z` se extrae como una nueva subexpresión y se le da un nombre. Mientras que los términos restantes se recopilan juntos para que cada variable aparezca exactamente una vez (y de hecho variable :math:`y` cuyos términos cancelar se eliminan).
152
153Finalmente, cada restricción se escribe en la forma FlatZinc obteniendo:
154
155.. code-block:: minizinc
156
157 var 0..80: INT01;
158 constraint int_lin_le([1,4,1],[INT01,x,z],23);
159 constraint int_times(x,z,INT01);
160
161.. _sec-unroll:
162
163
164
165Desenrollar expresiones
166-----------------------
167
168La mayoría de los modelos requieren la creación de una serie de restricciones que dependen de los datos de entrada. MiniZinc admite estos modelos con tipos de matriz, listas y conjuntos de comprensiones y funciones de agregación.
169
170Considere la siguiente expresión desde el ejemplo de programación de planificación :numref:`ex-prod-planning`.
171
172.. code-block:: minizinc
173
174 int: mproducts = max (p in Products)
175 (min (r in Resources where consumption[p,r] > 0)
176 (capacity[r] div consumption[p,r]));
177
178Como esto utiliza la sintaxis de llamada del generador, podemos reescribirla en forma equivalente, que es procesada por ``mzn2fzn``:
179
180.. code-block:: minizinc
181
182 int: mproducts = max([ min [ capacity[r] div consumption[p,r]
183 | r in Resources where consumption[p,r] > 0])
184 | p in Products]);
185
186Teniendo en cuenta los datos
187
188.. code-block:: minizinc
189
190 nproducts = 2;
191 nresources = 5;
192 capacity = [4000, 6, 2000, 500, 500];
193 consumption= [| 250, 2, 75, 100, 0,
194 | 200, 0, 150, 150, 75 |];
195
196Esto primero construye la matriz de :mzn:`p = 1`
197
198.. code-block:: minizinc
199
200 [ capacity[r] div consumption[p,r]
201 | r in 1..5 where consumption[p,r] > 0]
202
203Que es :mzn:`[16, 3, 26, 5]` y luego calcula el mínimo como 3.
204Luego construye la misma matriz para :mzn:`p = 2` que es :mzn:`[20, 13, 3, 6]` y calcula el mínimo como 3. Luego construye la matriz :mzn:`[3, 3]` y calcula el máximo como 3. No hay representación de :mzn:`mproducts` en la salida FlatZinc, esta evaluación se usa simplemente para reemplazar :mzn:`mproducts` por el valor calculado 3.
205
206La forma más común de expresión agregada en un modelo de restricción es :mzn:`forall`. Todas las expresiones se desenrollan en múltiples restricciones.
207
208Considere el siguiente fragmento de MiniZinc
209
210.. code-block:: minizinc
211
212 array[1..8] of var 0..9: v = [S,E,N,D,M,O,R,Y];
213 constraint forall(i,j in 1..8 where i < j)(v[i] != v[j])
214
215Que surge del ejemplo SEND-MORE-MONEY de :numref:`ex-smm` utilizando una descomposición predeterminada para :mzn:`alldifferent`.
216La expresión :mzn:`forall` crea una restricción para cada par :math:`i, j` que cumple con el requisito :math:`i <j`, creando así:
217
218.. code-block:: minizinc
219
220 constraint v[1] != v[2]; % S != E
221 constraint v[1] != v[3]; % S != N
222 ...
223 constraint v[1] != v[8]; % S != Y
224 constraint v[2] != v[3]; % E != N
225 ...
226 constraint v[7] != v[8]; % R != Y
227
228En la forma de FlatZinc esto es:
229
230.. code-block:: minizinc
231
232 constraint int_neq(S,E);
233 constraint int_neq(S,N);
234 ...
235 constraint int_neq(S,Y);
236 constraint int_neq(E,N);
237 ...
238 constraint int_neq(R,Y);
239
240Observe cómo las variables temporales del arreglo :mzn:`v[i]` son reemplazadas por las variables originales en el resultado FlatZinc.
241
242
243Arreglos
244--------
245
246Los arrays unidimensionales en MiniZinc pueden tener índices arbitrarios siempre que sean enteros contiguos. En FlatZinc todas las matrices están indexadas desde :mzn:`1..l` donde :mzn:`l` es la longitud de la matriz. Esto significa que las búsquedas de matriz deben traducirse a la vista de índices de FlatZinc.
247
248Consider the following MiniZinc model for balancing a seesaw of length :mzn:`2 * l2`, with a child of weight :mzn:`cw` kg using exactly :mzn:`m` 1kg weights.
249
250Considere el siguiente modelo MiniZinc para equilibrar un balance de longitud :mzn:`2 * l2`, con un pequeño de peso :mzn:`cw` kg usando exactamente un peso :mzn:`m` de 1kg.
251
252.. code-block:: minizinc
253
254 int: cw; % Pequeño peso
255 int: l2; % La mitad de la longitud del balance
256 int: m; % Cantidad de 1 kg de peso
257 array[-l2..l2] of var 0..max(m,cw): w; % Peso en cada punto
258 var -l2..l2: p; % Posición del peso.
259 constraint sum(i in -l2..l2)(i * w[i]) = 0; % Balance
260 constraint sum(i in -l2..l2)(w[i]) = m + cw;% Todos los pesos usados.
261 constraint w[p] = cw; % El pequeño peso está en la posición p
262 solve satisfy;
263
264Dado :mzn:`cw = 2`, :mzn:`l2 = 2`, y :mzn:`m = 3` el desenrollado produce las restricciones
265
266.. code-block:: minizinc
267
268 array[-2..2] of var 0..3: w;
269 var -2..2: p
270 constraint -2*w[-2] + -1*w[-1] + 0*w[0] + 1*w[1] + 2*w[2] = 0;
271 constraint w[-2] + w[-1] + w[0] + w[1] + w[2] = 5;
272 constraint w[p] = 2;
273
274Pero FlatZinc insiste en que la matriz :mzn:`w` comienza en el índice 1.
275Esto significa que necesitamos reescribir todos los accesos a la matriz para usar el nuevo valor de índice. Para las búsquedas de arreglos fijos esto es fácil, para las búsquedas de arreglos variables, podemos necesitar crear una nueva variable. El resultado para las ecuaciones anteriores es
276
277.. code-block:: minizinc
278
279 array[1..5] of var 0..3: w;
280 var -2..2: p
281 var 1..5: INT01;
282 constraint -2*w[1] + -1*w[2] + 0*w[3] + 1*w[4] + 2*w[5] = 0;
283 constraint w[1] + w[2] + w[3] + w[4] + w[5] = 5;
284 constraint w[INT01] = 2;
285 constraint INT01 = p + 3;
286
287Finalmente reescribimos las restricciones en forma de FlatZinc. Observe cómo la búsqueda del índice de matriz variable está mapeada a :mzn:`array_var_int_element`.
288
289.. code-block:: minizinc
290
291 array[1..5] of var 0..3: w;
292 var -2..2: p
293 var 1..5: INT01;
294 constraint int_lin_eq([2, 1, -1, -2], [w[1], w[2], w[4], w[5]], 0);
295 constraint int_lin_eq([1, 1, 1, 1, 1], [w[1],w[2],w[3],w[4],w[5]], 5);
296 constraint array_var_int_element(INT01, w, 2);
297 constraint int_lin_eq([-1, 1], [INT01, p], -3);
298
299Las matrices multidimensionales son compatibles con MiniZinc, pero FlatZinc solo soporta las matrices de una sola dimensión (en este momento).
300Esto significa que las matrices multidimensionales se deben asignar a matrices de una dimensión, y el acceso de matriz multidimensional se debe asignar al acceso a una matriz de una dimensión.
301
302Considere las restricciones de ecuación de Laplace definidas para un modelo de placa de elementos finitos en :numref:`ex-laplace`:
303
304.. literalinclude:: examples/laplace_es.mzn
305 :language: minizinc
306 :start-after: % Array declaration.
307 :end-before: % Lados.
308
309Asumiendo :mzn:`w = 4` y :mzn:`h = 4` esto crea las restricciones:
310
311.. code-block:: minizinc
312
313 array[0..4,0..4] of var float: t; % temperatura en el punto (i,j)
314 constraint 4.0*t[1,1] = t[0,1] + t[1,0] + t[2,1] + t[1,2];
315 constraint 4.0*t[1,2] = t[0,2] + t[1,1] + t[2,2] + t[1,3];
316 constraint 4.0*t[1,3] = t[0,3] + t[1,2] + t[2,3] + t[1,4];
317 constraint 4.0*t[2,1] = t[1,1] + t[2,0] + t[3,1] + t[2,2];
318 constraint 4.0*t[2,2] = t[1,2] + t[2,1] + t[3,2] + t[2,3];
319 constraint 4.0*t[2,3] = t[1,3] + t[2,2] + t[3,3] + t[2,4];
320 constraint 4.0*t[3,1] = t[2,1] + t[3,0] + t[4,1] + t[3,2];
321 constraint 4.0*t[3,2] = t[2,2] + t[3,1] + t[4,2] + t[3,3];
322 constraint 4.0*t[3,3] = t[2,3] + t[3,2] + t[4,3] + t[3,4];
323
324La matriz bidimensional de 25 elementos se convierte en una matriz unidimensional y los índices :mzn:`[i, j]` se convierte en :mzn:`[i * 5 + j + 1]`.
325
326.. code-block:: minizinc
327
328 array [1..25] of var float: t;
329 constraint 4.0*t[7] = t[2] + t[6] + t[12] + t[8];
330 constraint 4.0*t[8] = t[3] + t[7] + t[13] + t[9];
331 constraint 4.0*t[9] = t[4] + t[8] + t[14] + t[10];
332 constraint 4.0*t[12] = t[7] + t[11] + t[17] + t[13];
333 constraint 4.0*t[13] = t[8] + t[12] + t[18] + t[14];
334 constraint 4.0*t[14] = t[9] + t[13] + t[19] + t[15];
335 constraint 4.0*t[17] = t[12] + t[16] + t[22] + t[18];
336 constraint 4.0*t[18] = t[13] + t[17] + t[23] + t[19];
337 constraint 4.0*t[19] = t[14] + t[18] + t[24] + t[20];
338
339
340Reificación
341-----------
342
343.. index::
344 single: reification
345
346Los modelos FlatZinc implican solo variables y declaraciones de parámetros y una serie de restricciones primitivas. Por lo tanto, cuando modelamos en MiniZinc con conectivas booleanas distintas a la conjunción, algo tiene que hacerse. El enfoque principal para manejar fórmulas complejas que usan conectivos que no sean la conjunción es por *reificación*. Reificar una restricción :math:`c` crea una nueva restricción equivalente a :math:`b \leftrightarrow c` donde la variable booleana :math:`b` es :mzn:`true` si la restricción se cumple y :mzn:`false` si no se sostiene.
347
348Una vez que tenemos la capacidad de *reificar* las restricciones, el tratamiento de fórmulas complejas no es diferente de las expresiones aritméticas. Creamos un nombre para cada subexpresión y una restricción plana para restringir el nombre y tomar el valor de su subexpresión.
349
350Considere la siguiente expresión de restricción que ocurre en el ejemplo de programación de jobshop de :numref:`ex-jobshop`.
351
352
353
354
355.. code-block:: minizinc
356
357 constraint %% Asegurar que no haya superposición de tareas
358 forall(j in 1..tasks) (
359 forall(i,k in 1..jobs where i < k) (
360 s[i,j] + d[i,j] <= s[k,j] \/
361 s[k,j] + d[k,j] <= s[i,j]
362 ) );
363
364Dado el archivo de datos:
365
366.. code-block:: minizinc
367
368 jobs = 2;
369 tasks = 3;
370 d = [| 5, 3, 4 | 2, 6, 3 |]
371
372Entonces el desenrollar crea:
373
374.. code-block:: minizinc
375
376 constraint s[1,1] + 5 <= s[2,1] \/ s[2,1] + 2 <= s[1,1];
377 constraint s[1,2] + 3 <= s[2,2] \/ s[2,2] + 6 <= s[1,2];
378 constraint s[1,3] + 4 <= s[2,3] \/ s[2,3] + 3 <= s[1,3];
379
380La reificación de las restricciones que aparecen en la disyunción crea nuevas variables booleanas para definir los valores de cada expresión.
381
382.. code-block:: minizinc
383
384 array[1..2,1..3] of var 0..23: s;
385 constraint BOOL01 <-> s[1,1] + 5 <= s[2,1];
386 constraint BOOL02 <-> s[2,1] + 2 <= s[1,1];
387 constraint BOOL03 <-> s[1,2] + 3 <= s[2,2];
388 constraint BOOL04 <-> s[2,2] + 6 <= s[1,2];
389 constraint BOOL05 <-> s[1,3] + 4 <= s[2,3];
390 constraint BOOL06 <-> s[2,3] + 3 <= s[1,3];
391 constraint BOOL01 \/ BOOL02;
392 constraint BOOL03 \/ BOOL04;
393 constraint BOOL05 \/ BOOL06;
394
395Cada restricción primitiva ahora se puede asignar a la forma FlatZinc.
396Observe cómo la matriz de dos dimensiones :mzn:`s` está mapeada a una forma unidimensional.
397Cada restricción se puede asignar a la forma FlatZinc.
398Observe cómo la matriz de dos dimensiones :mzn:`s` está mapeada a una forma unidimensional.
399
400.. code-block:: minizinc
401
402 array[1..6] of var 0..23: s;
403 constraint int_lin_le_reif([1, -1], [s[1], s[4]], -5, BOOL01);
404 constraint int_lin_le_reif([-1, 1], [s[1], s[4]], -2, BOOL02);
405 constraint int_lin_le_reif([1, -1], [s[2], s[5]], -3, BOOL03);
406 constraint int_lin_le_reif([-1, 1], [s[2], s[5]], -6, BOOL04);
407 constraint int_lin_le_reif([1, -1], [s[3], s[6]], -4, BOOL05);
408 constraint int_lin_le_reif([-1, 1], [s[3], s[6]], -3, BOOL06);
409 constraint array_bool_or([BOOL01, BOOL02], true);
410 constraint array_bool_or([BOOL03, BOOL04], true);
411 constraint array_bool_or([BOOL05, BOOL06], true);
412
413El :mzn:`int_lin_le_reif` es la forma reificada de la restricción lineal :mzn:` int_lin_le`.
414
415
416La mayoría de las restricciones primitivas de FlatZinc :math:`p(\bar{x})` tiene una forma reificada :math:`\mathit{p\_reif}(\bar{x},b)` que toma un argumento final adicional :math:`b` y define la restricción :math:`b \leftrightarrow p(\bar{x})`. Las restricciones primitivas de FlatZinc que definen relaciones funcionales, como :mzn:`int_plus` y :mzn:`int_plus`, no necesitan admitir la reificación. En cambio, la igualdad con el resultado de la función se reifica.
417
418Otro uso importante de la reificación surge cuando usamos la función de coerción :mzn:`bool2int` (explícita o implícitamente usando una expresión booleana como una expresión entera). El aplanamiento crea una variable booleana para contener el valor del argumento de expresión booleana, así como una variable entera (restringida a :mzn:`0..1`) para mantener este valor.
419
420
421Considere el problema de la serie mágica de :numref:`ex-magic-series`.
422
423.. literalinclude:: examples/magic-series_es.mzn
424 :language: minizinc
425 :end-before: solve satisfy
426
427Dado :mzn:`n = 2` el desenrollado crea
428
429.. code-block:: minizinc
430
431 constraint s[0] = bool2int(s[0] = 0) + bool2int(s[1] = 0);
432 constraint s[1] = bool2int(s[0] = 1) + bool2int(s[1] = 1);
433
434y el aplanamiento crea:
435
436.. code-block:: minizinc
437
438 constraint BOOL01 <-> s[0] = 0;
439 constraint BOOL03 <-> s[1] = 0;
440 constraint BOOL05 <-> s[0] = 1;
441 constraint BOOL07 <-> s[1] = 1;
442 constraint INT02 = bool2int(BOOL01);
443 constraint INT04 = bool2int(BOOL03);
444 constraint INT06 = bool2int(BOOL05);
445 constraint INT08 = bool2int(BOOL07);
446 constraint s[0] = INT02 + INT04;
447 constraint s[1] = INT06 + INT08;
448
449El formulario final de FlatZinc es:
450
451.. code-block:: minizinc
452
453 var bool: BOOL01;
454 var bool: BOOL03;
455 var bool: BOOL05;
456 var bool: BOOL07;
457 var 0..1: INT02;
458 var 0..1: INT04;
459 var 0..1: INT06;
460 var 0..1: INT08;
461 array [1..2] of var 0..2: s;
462 constraint int_eq_reif(s[1], 0, BOOL01);
463 constraint int_eq_reif(s[2], 0, BOOL03);
464 constraint int_eq_reif(s[1], 1, BOOL05);
465 constraint int_eq_reif(s[2], 1, BOOL07);
466 constraint bool2int(BOOL01, INT02);
467 constraint bool2int(BOOL03, INT04);
468 constraint bool2int(BOOL05, INT06);
469 constraint bool2int(BOOL07, INT08);
470 constraint int_lin_eq([-1, -1, 1], [INT02, INT04, s[1]], 0);
471 constraint int_lin_eq([-1, -1, 1], [INT06, INT08, s[2]], 0);
472 solve satisfy;
473
474Predicados
475----------
476
477Un factor importante en el soporte para MiniZinc por muchos solucionadores diferentes es que las restricciones globales (y de hecho las restricciones de FlatZinc) pueden ser especializadas para el solucionador particular.
478
479Cada solucionador especificará un predicado sin una definición, o con una definición. Por ejemplo, un solucionador que tiene un predicado global integrado :mzn:`alldifferent`, incluirá la definición
480
481.. code-block:: minizinc
482
483 predicate alldifferent(array[int] of var int:x);
484
485en su biblioteca global, mientras que un solucionador que usa la descomposición por defecto tendrá la definición
486
487.. code-block:: minizinc
488
489 predicate alldifferent(array[int] of var int:x) =
490 forall(i,j in index_set(x) where i < j)(x[i] != x[j]);
491
492Las llamadas a predicados :math:`p(\bar{t})` se aplanan construyendo primero las variables :math:`v_i` para cada argumento :math:`t_i`. Si el predicado no tiene definición, simplemente usamos una llamada al predicado con los argumentos construidos: :math:`p(\bar{v})`.
493
494Si el predicado tiene una definición :math:`p(\bar{x}) = \phi(\bar{x})` luego reemplazamos la llamada del predicado :math:`p(\bar{t})` con el cuerpo del predicado con los argumentos formales reemplazados por las variables del argumento, es decir :math:`\phi(\bar{v})`.
495
496Tenga en cuenta que si una llamada de predicado :math:`p(\bar{t})` aparece en una posición reificada y no tiene definición, verificamos la existencia de una versión reificada del predicado :math:`\mathit{p\_reif}(\bar{x},b)` en cuyo caso usamos eso.
497
498Consideremos la restricción :mzn:`alldifferent` en el ejemplo de SEND-MORE-MONEY de :numref:`ex-smm`
499
500.. code-block:: minizinc
501
502 constraint alldifferent([S,E,N,D,M,O,R,Y]);
503
504Si el solucionador tiene una función incorporada :mzn:`alldifferent` simplemente construimos una nueva variable para el argumento y la reemplazamos en la llamada.
505
506.. code-block:: minizinc
507
508 array[1..8] of var 0..9: v = [S,E,N,D,M,O,R,Y];
509 constraint alldifferent(v);
510
511Observe que el análisis de límites intenta encontrar límites estrechos en la nueva variable de matriz. La razón para construir el argumento de la matriz es si usamos la misma matriz dos veces, el solucionador FlatZinc no tiene que construirla dos veces.
512En este caso, dado que no se usa dos veces, una etapa posterior de la traducción reemplazará :mzn:`v` por su definición.
513
514¿Qué ocurre si el solucionador usa la definición predeterminada de :mzn:`alldifferent`?.
515
516Entonces la variable :mzn:`v` se define como de costumbre, y la llamada del predicado se reemplaza por una copia renombrada donde :mzn:`v` reemplaza el argumento formal :mzn:`x`.
517
518El código resultante es:
519
520.. code-block:: minizinc
521
522 array[1..8] of var 0..9: v = [S,E,N,D,M,O,R,Y];
523 constraint forall(i,j in 1..8 where i < j)(v[i] != v[j])
524
525Que examinamos en :ref:`sec-unroll`.
526
527Considere la siguiente restricción, donde :mzn:`alldifferent` aparece en una posición reificada.
528
529.. code-block:: minizinc
530
531 constraint alldifferent([A,B,C]) \/ alldifferent([B,C,D]);
532
533Si el solucionador tiene una forma reificada de :mzn:`alldifferent` esto será flattend a:
534
535.. code-block:: minizinc
536
537 constraint alldifferent_reif([A,B,C],BOOL01);
538 constraint alldifferent_reif([B,C,D],BOOL02);
539 constraint array_bool_or([BOOL01,BOOL02],true);
540
541Usando la descomposición por defecto, el reemplazo del predicado creará primero:
542
543.. code-block:: minizinc
544
545 array[1..3] of var int: v1 = [A,B,C];
546 array[1..3] of var int: v2 = [B,C,D];
547 constraint forall(i,j in 1..3 where i<j)(v1[i] != v1[j]) \/
548 forall(i,j in 1..3 where i<j)(v2[i] != v2[j]);
549
550que eventualmente será aplanado a la forma FlatZinc:
551
552.. code-block:: minizinc
553
554 constraint int_neq_reif(A,B,BOOL01);
555 constraint int_neq_reif(A,C,BOOL02);
556 constraint int_neq_reif(B,C,BOOL03);
557 constraint array_bool_and([BOOL01,BOOL02,BOOL03],BOOL04);
558 constraint int_neq_reif(B,D,BOOL05);
559 constraint int_neq_reif(C,D,BOOL06);
560 constraint array_bool_and([BOOL03,BOOL05,BOOL06],BOOL07);
561 constraint array_bool_or([BOOL04,BOOL07],true);
562
563
564Observe cómo la eliminación de subexpresiones común reutiliza la desigualdad reificada :mzn:`B! = C` (aunque hay una traducción mejor que eleva la restricción común a la conjunción de nivel superior).
565
566.. _sec-let:
567
568
569
570Expresiones Let
571---------------
572
573Las expresiones ``let`` son una poderosa herramienta de MiniZinc para introducir nuevas variables. Esto es útil para crear sub expresiones comunes y para definir variables locales para predicados.
574
575Durante el aplanamiento, las expresiones de ``let`` se traducen a declaraciones de variables y restricciones. La semántica relacional de MiniZinc significa que estas restricciones deben aparecer como si estuvieran conjuntas en la primera expresión booleana adjunta.
576
577Una característica clave de las expresiones ``let`` es que cada vez que se utilizan crean nuevas variables.
578
579Considere el aplanamiento del código:
580
581.. code-block:: minizinc
582
583 constraint even(u) \/ even(v);
584 predicate even(var int: x) =
585 let { var int: y } in x = 2 * y;
586
587Primero, las llamadas de predicados se reemplazan por su definición.
588
589.. code-block:: minizinc
590
591 constraint (let { var int: y} in u = 2 * y) \/
592 (let { var int: y} in v = 2 * y);
593
594A continuación, las variables ``let`` se renombran aparte como:
595
596.. code-block:: minizinc
597
598 constraint (let { var int: y1} in u = 2 * y1) \/
599 (let { var int: y2} in v = 2 * y2);
600
601Finalmente, las declaraciones variables se extraen al nivel superior
602
603.. code-block:: minizinc
604
605 var int: y1;
606 var int: y2;
607 constraint u = 2 * y1 \/ v = 2 * y2;
608
609Una vez que se elimina la expresión ``let`` podemos aplanar como de costumbre.
610
611Recuerde que las expresiones ``let`` pueden definir valores para las variables recién introducidas (y de hecho deben hacerlo para los parámetros).
612Estos definen implícitamente restricciones que también deben aplastarse.
613
614Considere la compleja función objetivo para el problema de asignación de asientos en una bodas :numref:`ex-wedding2`.
615
616.. code-block:: minizinc
617
618 solve maximize sum(h in Hatreds)(
619 let { var Seats: p1 = pos[h1[h]],
620 var Seats: p2 = pos[h2[h]],
621 var 0..1: same = bool2int(p1 <= 6 <-> p2 <= 6) } in
622 same * abs(p1 - p2) + (1-same) * (abs(13 - p1 - p2) + 1));
623
624Por concisión asumimos solo los dos primeros Hatreds (odios), entonces:
625
626.. code-block:: minizinc
627
628 set of int: Hatreds = 1..2;
629 array[Hatreds] of Guests: h1 = [groom, carol];
630 array[Hatreds] of Guests: h2 = [clara, bestman];
631
632
633El primer paso de flattening es desenrollar la expresión :mzn:`sum`, mantenemos los nombres y parámetros de los invitados :mzn:`Seats` solo para mayor claridad, en realidad serían reemplazados por su definición:
634
635.. code-block:: minizinc
636
637 solve maximize
638 (let { var Seats: p1 = pos[groom],
639 var Seats: p2 = pos[clara],
640 var 0..1: same = bool2int(p1 <= 6 <-> p2 <= 6) } in
641 same * abs(p1 - p2) + (1-same) * (abs(13 - p1 - p2) + 1))
642 +
643 (let { var Seats: p1 = pos[carol],
644 var Seats: p2 = pos[bestman],
645 var 0..1: same = bool2int(p1 <= 6 <-> p2 <= 6) } in
646 same * abs(p1 - p2) + (1-same) * (abs(13 - p1 - p2) + 1));
647
648A continuación, cada nueva variable en una expresión ``let`` se renombra para ser distinta
649
650.. code-block:: minizinc
651
652 solve maximize
653 (let { var Seats: p11 = pos[groom],
654 var Seats: p21 = pos[clara],
655 var 0..1: same1 = bool2int(p11 <= 6 <-> p21 <= 6) } in
656 same1 * abs(p11 - p21) + (1-same1) * (abs(13 - p11 - p21) + 1))
657 +
658 (let { var Seats: p12 = pos[carol],
659 var Seats: p22 = pos[bestman],
660 var 0..1: same2 = bool2int(p12 <= 6 <-> p22 <= 6) } in
661 same2 * abs(p12 - p22) + (1-same2) * (abs(13 - p12 - p22) + 1));
662
663Las variables en la expresión ``let`` se extraen al nivel superior y las restricciones de definición se extraen al nivel correcto (que en este caso también es el nivel superior).
664
665.. code-block:: minizinc
666
667 var Seats: p11;
668 var Seats: p21;
669 var 0..1: same1;
670 constraint p12 = pos[clara];
671 constraint p11 = pos[groom];
672 constraint same1 = bool2int(p11 <= 6 <-> p21 <= 6);
673 var Seats p12;
674 var Seats p22;
675 var 0..1: same2;
676 constraint p12 = pos[carol];
677 constraint p22 = pos[bestman];
678 constraint same2 = bool2int(p12 <= 6 <-> p22 <= 6) } in
679 solve maximize
680 same1 * abs(p11 - p21) + (1-same1) * (abs(13 - p11 - p21) + 1))
681 +
682 same2 * abs(p12 - p22) + (1-same2) * (abs(13 - p12 - p22) + 1));
683
684Ahora hemos construido un código en MiniZinc equivalente sin el uso de expresiones ``let`` y el aplanamiento puede continuar como de costumbre.
685
686Como una ilustración de las expresiones ``let`` que no aparecen en el nivel superior, considere el siguiente modelo:
687
688.. code-block:: minizinc
689
690 var 0..9: x;
691 constraint x >= 1 -> let { var 2..9: y = x - 1 } in
692 y + (let { var int: z = x * y } in z * z) < 14;
693
694Extraemos las definiciones de las variables al nivel superior y las restricciones al primer contexto booleano que lo incluye, que aquí está en el lado derecho de la implicación.
695
696.. code-block:: minizinc
697
698 var 0..9: x;
699 var 2..9: y;
700 var int: z;
701 constraint x >= 1 -> (y = x - 1 /\ z = x * y /\ y + z * z < 14);
702
703Tenga en cuenta que si sabemos que la ecuación que define una definición de variable no puede fallar, podemos extraerla al nivel superior. Esto generalmente hará que la resolución sea mucho más rápida.
704
705Para el ejemplo anterior, la restricción :mzn:`y = x - 1` puede fallar ya que el dominio de :mzn:`y` no es lo suficientemente grande para todos los valores posibles de :mzn:`x - 1`. Pero la restricción :mzn:`z = x * y` no puede (de hecho el análisis de límites dará :mzn:`z` límites lo suficientemente grandes como para contener todos los valores posibles de :mzn:`x * y`).
706
707Un mejor aplanamiento dará:
708
709.. code-block:: minizinc
710
711 var 0..9: x;
712 var 2..9: y;
713 var int: z;
714 constraint z = x * y;
715 constraint x >= 1 -> (y = x - 1 /\ y + z * z < 14);
716
717Actualmente ``mzn2fzn`` hace esto definiendo siempre los límites declarados de una variable introducida para que sea lo suficientemente grande como para que su ecuación de definición mantenga siempre y luego agregue restricciones de límites en el contexto correcto para la expresión ``let``. En el ejemplo anterior, esto da como resultado
718
719
720.. code-block:: minizinc
721
722 var 0..9: x;
723 var -1..8: y;
724 var -9..72: z;
725 constraint y = x - 1;
726 constraint z = x * y;
727 constraint x >= 1 -> (y >= 2 /\ y + z * z < 14);
728
729Esta traducción conduce a una solución más eficiente ya que el cálculo posiblemente complejo de la variable ``let`` no se reifica.
730
731Otra razón para este enfoque es que también funciona cuando las variables introducidas aparecen en contextos negativos (siempre que tengan una definición).
732
733Considere el siguiente ejemplo similar al anterior:
734
735.. code-block:: minizinc
736
737 var 0..9: x;
738 constraint (let { var 2..9: y = x - 1 } in
739 y + (let { var int: z = x * y } in z * z) > 14) -> x >= 5;
740
741Las expresiones ``let`` aparecen en un contexto negado, pero se define cada variable introducida.
742
743El código aplanado es:
744
745.. code-block:: minizinc
746
747 var 0..9: x;
748 var -1..8: y;
749 var -9..72: z;
750 constraint y = x - 1;
751 constraint z = x * y;
752 constraint (y >= 2 /\ y + z * z > 14) -> x >= 5;
753
754Tenga en cuenta que el método simple para la eliminación de ``let`` no proporciona una traducción correcta:
755
756.. code-block:: minizinc
757
758 var 0..9: x;
759 var 2..9: y;
760 var int: z;
761 constraint (y = x - 1 /\ z = x * y /\ y + z * z > 14) -> x >= 5;
762
763Da respuestas para todos los valores posibles de :mzn:`x`, mientras que la restricción original elimina la posibilidad de que :mzn:`x = 4`.
764
765El tratamiento de *elementos de restricción* en ``let`` expresiones es análogo a variables definidas. Uno puede pensar en una restricción como equivalente a la definición de una nueva variable booleana. Las definiciones de las nuevas variables booleanas se extraen al nivel superior y las Boolean permanece en el contexto correcto.
766
767.. code-block:: minizinc
768
769 constraint z > 1 -> let { var int: y,
770 constraint (x >= 0) -> y = x,
771 constraint (x < 0) -> y = -x
772 } in y * (y - 2) >= z;
773
774Es tratado como:
775
776.. code-block:: minizinc
777
778 constraint z > 1 -> let { var int: y,
779 var bool: b1 = ((x >= 0) -> y = x),
780 var bool: b2 = ((x < 0) -> y = -x),
781 constraint b1 /\ b2
782 } in y * (y - 2) >= z;
783
784Y se aplana a:
785
786.. code-block:: minizinc
787
788 constraint b1 = ((x >= 0) -> y = x);
789 constraint b2 = ((x < 0) -> y = -x);
790 constraint z > 1 -> (b1 /\ b2 /\ y * (y - 2) >= z);