Ajuste de rectángulo en sintaxis SMT (solucionador Z3)

Answer

1. 

   davy.ai

   July 12, 2023 at 7:41 pm

   Como experto en TI especializado en booleanos, z3, smt y sat, puedes formular el problema de colocar N bloques rectangulares con tamaños diferentes en una grilla como un Problema de Satisfacción de Restricciones (CSP, por sus siglas en inglés). Para hacer esto, necesitas identificar las variables, dominios y restricciones del problema.

   Las variables en el problema son las coordenadas de la esquina superior izquierda de cada bloque en la grilla. Los dominios de las variables son el conjunto de todas las posiciones posibles en la grilla donde se puede colocar cada bloque sin superponerse con ningún otro bloque. Las restricciones son las condiciones que deben cumplirse para una solución válida. Estas restricciones incluyen:

   • Los bloques no deben superponerse entre sí.
   • Los bloques pueden tocarse en los bordes.
   • Puede haber lugares vacíos en la grilla.

   Para generar la fórmula para el CSP, puedes utilizar un solucionador SMT como Z3. Necesitas definir las variables, dominios y restricciones en la sintaxis SMT. Aquí tienes un ejemplo de cómo colocar 4 bloques rectangulares de tamaño 2×2 en una grilla de 8×8 usando SMT:

   from z3 import *
   
   # Definir variables
   x = [Int('x{}'.format(i)) for i in range(4)]
   y = [Int('y{}'.format(i)) for i in range(4)]
   
   # Definir dominios
   s = Solver()
   for i in range(4):
       s.add(x[i] >= 0, x[i] <= 8-2)
       s.add(y[i] >= 0, y[i] <= 8-2)
   
   # Definir restricciones
   for i in range(3):
       for j in range(i+1, 4):
           s.add(Or(x[i]+2 <= x[j], x[i] >= x[j]+2, y[i]+2 <= y[j], y[i] >= y[j]+2))
   
   # Resolver el problema
   if s.check() == sat:
       m = s.model()
       print([(m[x[i]], m[y[i]]) for i in range(4)])
   else:
       print('¡No se encontró ninguna solución!')
   

   En este ejemplo, definimos las variables x e y para representar las coordenadas de la esquina superior izquierda de cada bloque en la grilla. Definimos los dominios de las variables como el conjunto de todas las posiciones posibles en la grilla donde se puede colocar cada bloque sin superponerse con ningún otro bloque. Las restricciones se definen utilizando cláusulas Or que aseguran que los bloques no se superpongan entre sí.

   Cuando ejecutamos el solucionador, muestra las posiciones donde cada bloque debe colocarse en la grilla. Puedes cambiar el número de bloques, los tamaños de los bloques y el tamaño de la grilla para resolver diferentes instancias del problema.

Comments are closed.