this repo has no description
dekker.one
1.. _sec-sat:
2
3Modelado de la satisfacción Booleana en MiniZinc
4================================================
5
6MiniZinc puede usarse para modelar problemas de satisfaccion booleanos, donde las variables estan restringidas a ser booleano (:mzn:`bool`).
7MiniZinc se puede utilizar con solucionadores de satisfacción booleanos eficientes para resolver los modelos resultantes de manera eficiente.
8
9Modelando Enteros
10-----------------
11
12Muchas veces, aunque deseamos utilizar un solucionador de satisfaccion booleano, podriamos necesitar modelar algunas partes enteras de nuestro problema.
13
14Hay tres formas comunes de modelar variables enteras: :math:`I` en el rango de :math:`0 \dots m`, donde :math:`m = 2^{k}-1` utiliza variables booleanas.
15
16- Binary: :math:`I` es representado por :math:`k` variables binarias :math:`i_0, \ldots, i_{k-1}`, donde :math:`I = 2^{k-1} i_{k-1} + 2^{k-2} i_{k-2} + \cdots + 2 i_1 + i_0`.
17
18 Esto puede ser representado en MiniZinc como
19
20 .. code-block:: minizinc
21
22 array[0..k-1] of var bool: i;
23 var 0..pow(2,k)-1: I = sum(j in 0..k-1)(bool2int(i[j])*pow(2,j));
24
25- Unary: donde :math:`I` es representado por :math:`m` variables binarias :math:`i_1, \ldots, i_m` y :math:`i = \sum_{j=1}^m \mathtt{bool2int}(i_j)`. Como hay redundancia masiva en la representacion unaria, usualmente requerimos que :math:`i_j \rightarrow i_{j-1}, 1 < j \leq m`.
26
27 Esto puede ser representado en MiniZinc como
28
29 .. code-block:: minizinc
30
31 array[1..m] of var bool: i;
32 constraint forall(j in 2..m)(i[j] -> i[j-1]);
33 var 0..m: I = sum(j in 1..m)(bool2int(i[j]);
34
35- Value: donde :math:`I` es representado por :math:`m+1` variables binarias :math:`i_0, \ldots, i_m` donde :math:`i = k \Leftrightarrow i_k`, y como máximo uno de :math:`i_0, \ldots, i_m` es verdadero.
36
37 Esto puede ser representado en MiniZinc como
38
39 .. code-block:: minizinc
40
41 array[0..m] of var bool: i;
42 constraint sum(j in 0..m)(bool2int(i[j]) == 1;
43 var 0..m: I;
44 constraint foall(j in 0..m)(I == j <-> i[j]);
45
46Hay ventajas y desventajas para cada representación. Depende de qué operaciones en enteros se requieran en el modelo y cuál es preferible.
47
48Modelando Desigualdad
49---------------------
50
51Consideremos el modelado de un problema de cuadrados latinos. Un cuadrado latino es una matriz :math:`n \ times n` de números de :math:`1..n`, tal que cada número aparece exactamente una vez en cada fila y columna.
52Un modelo entero para cuadrados latinos se muestra en :numref:`ex-latin`.
53
54.. literalinclude:: examples/latin_es.mzn
55 :language: minizinc
56 :name: ex-latin
57 :caption: Modelo entero para los cuadrados latino (:download:`latin_es.mzn <examples/latin_es.mzn>`).
58
59La única limitación de los enteros es de hecho desigualdad, que se codifica en la restricción :mzn:`alldifferent`.
60La representación del valor es la mejor forma de representar la desigualdad.
61Un modelo solo booleano para cuadrados latinos se muestra en :numref:`ex-latinbool`.
62Tenga en cuenta cada elemento del conjunto de enteros :mzn:`a[i, j]` se reemplaza por un arreglo de booleanos.
63Utilizamos el predicado :mzn:`exactlyone` para codificar que cada valor se use exactamente una vez en cada fila y en cada columna, así como para codificar que exactamente uno de los Booleanos correspondiente al elemento de arreglo entero :mzn:`a[i, j]` es verdadero.
64
65.. literalinclude:: examples/latinbool_es.mzn
66 :language: minizinc
67 :name: ex-latinbool
68 :caption: Modelo booleano para los cuadrados latinos (:download:`latinbool_es.mzn <examples/latinbool_es.mzn>`).
69
70
71Modelando Cardinalidad
72----------------------
73
74Consideremos el modelado del rompecabezas de Light Up. El rompecabezas consiste en una cuadrícula rectangular de cuadrados que están en blanco, o llenos. Cada cuadrado lleno puede contener un número del 1 al 4, o puede no tener ningún número. El objetivo es colocar luces en los cuadrados en blanco para que
75
76- Cada casilla en blanco está "iluminada", es decir, puede ver una luz a través de una línea ininterrumpida de cuadrados en blanco.
77- No se pueden ver dos luces a si mismas.
78- El número de luces adyacentes a un cuadrado lleno numerado es exactamente el número en el cuadrado lleno.
79
80Un ejemplo de un rompecabezas de Light Up se muestra en :numref:`fig-lightup`
81con su solución en :numref:`fig-lightup-sol`.
82
83.. _fig-lightup:
84
85.. figure:: figures/lightup.*
86
87 Un ejemplo de un rompecabezas de Light Up
88
89.. _fig-lightup-sol:
90
91.. figure:: figures/lightup2.*
92
93 La solución completa del rompecabezas de Light Up
94
95Es natural modelar este problema usando variables booleanas para determinar qué cuadrados contienen una luz y cuáles no, pero hay algo de aritmética entera que considerar para los cuadrados llenos.
96
97.. literalinclude:: examples/lightup_es.mzn
98 :language: minizinc
99 :name: ex-lightup
100 :caption: Modelo SAT para el rompecabezas de Light Up (:download:`lightup_es.mzn <examples/lightup_es.mzn>`).
101
102A model for the problem is given in :numref:`ex-lightup`.
103A data file for the problem shown in :numref:`fig-lightup`
104is shown in :numref:`fig-lightupdzn`.
105
106Un modelo para el problema es dado en :numref:`ex-lightup`.
107Un archivo de datos para el problema :numref:`fig-lightup` se muestra en :numref:`fig-lightupdzn`.
108
109.. literalinclude:: examples/lightup_es.dzn
110 :language: minizinc
111 :name: fig-lightupdzn
112 :caption: El archivo de datos para la instancia del rompecabezas de Light Up se muestra en :numref:`fig-lightup`.
113
114El modelo hace uso de un predicado de suma booleana
115
116.. code-block:: minizinc
117
118 predicate bool_sum_eq(array[int] of var bool:x, int:s);
119
120que requiere que la suma de un arreglo de Boolean sea igual a un entero fijo. Existen varias formas de modelar tales restricciones de *cardinalidad* usando Booleanos.
121
122- Sumar redes: podemos usar una red de sumadores para construir una representación booleana binaria de la suma de los booleanos.
123- Redes de clasificación: podemos usar una red de clasificación para ordenar el arreglo de Booleanos para crear una representación unaria de la suma de los Booleanos.
124- Diagramas de decisiones binarias: podemos crear un diagrama de decisión binario (BDD) que codifica la restricción de cardinalidad.
125
126.. literalinclude:: examples/bboolsum_es.mzn
127 :language: minizinc
128 :name: ex-bboolsum
129 :caption: Restricciones de cardinalidad por las redes de sumador binarias (:download:`bboolsum_es.mzn <examples/bboolsum_es.mzn>`).
130
131.. literalinclude:: examples/binarysum_es.mzn
132 :language: minizinc
133 :name: ex-binarysum
134 :caption: Código para construir redes de adición binaria (:download:`binarysum_es.mzn <examples/binarysum_es.mzn>`).
135
136Podemos implementar :mzn:`bool_sum_eq` usando redes de sumador binarias usando el código que se muestra en :numref:`ex-bboolsum`.
137El predicado :mzn:`binary_sum` definido en :numref:`ex-binarysum` crea una representación binaria de la suma de :mzn:`x` al dividir la lista en dos, sumando cada mitad para crear una representación binaria y luego sumando estos dos números binarios usando :mzn:`binary_add`.
138Si la lista :mzn:`x` es impar, el último bit se guarda para usar como un complemento a la adición binaria
139
140.. \pjs{Add a picture of an adding network}
141
142.. literalinclude:: examples/uboolsum_es.mzn
143 :language: minizinc
144 :name: ex-uboolsum
145 :caption: Restricciones de Cardinalidad Clasificando Redes (:download:`uboolsum_es.mzn <examples/uboolsum_es.mzn>`).
146
147.. literalinclude:: examples/oesort_es.mzn
148 :language: minizinc
149 :name: ex-oesort
150 :caption: Odd-even Fusionar Redes de Clasificación (:download:`oesort_es.mzn <examples/oesort_es.mzn>`).
151
152Podemos implementar :mzn:`bool_sum_eq` utilizando redes de clasificación unaria utilizando el código que se muestra en :numref:` ex-uboolsum`.
153La restricción de cardinalidad se define expandiendo la entrada :mzn:`x` para tener una longitud de una potencia de 2 y clasificar los bits resultantes utilizando una red de clasificación de combinación de pares impares.
154El clasificador de combinación impar-par que se muestra en :mzn:`ex-oesort` funciona recursivamente mediante la divición de la lista de entrada en 2, ordenando cada lista y combinando las dos listas ya ordenadas.
155
156.. \pjs{Add much more stuff on sorting networks}
157
158
159
160.. \pjs{Add a picture of an adding network}
161
162.. literalinclude:: examples/bddsum_es.mzn
163 :language: minizinc
164 :name: ex-bddsum
165 :caption: Restricciones de cardinalidad por diagramas de decisión binarios (:download:`bddsum_es.mzn <examples/bddsum_es.mzn>`).
166
167Nosotros podemos implementar :mzn:`bool_sum_eq` usando diagramas de decición binaria usando el codigo que se muestra en :mzn:`ex:bddsum`.
168La restricción de cardinalidad se divide en dos casos: ya sea en el primer elemento :mzn:`x[1]` es :mzn:`true`, y la suma de los bits restantes es :mzn:`s-1`, o :mzn:`x[1]` es :mzn:`false` y la suma de los bits restantes es :mzn:`s`. Por eficiencia, esto se basa en la eliminación de la subexpresión común para evitar crear muchas restricciones equivalentes.
169
170.. \pjs{Add a picture of a bdd network network}