Piscifactoria

De WikiRA

Se trata de un problema con aplicaciones industriales en nuestro entorno socioeconómico.

En una piscifactoría se está considerando producir distintas especies de peces. Dependiendo de las especies, dos especies pueden compartir el mismo tanque o no. Cada tanque posee unas condiciones concretas que hace que sea o no adecuado para una especie dada. En ausencia de restricciones de capacidad,

¿es posible producir todas las especies en la piscifactoría?

Para ello, nos hemos basado en definir una función que reciba:

  • el número de tanques (m)
  • el número de especies (n)
  • las incompatibilidades tanque-especie
  • las incompatibilidades entre especies

Esta función devolverá una fórmula que expresa si las especies se pueden producir o no en la piscifactoría.


Contenido

Formalización en lógica proposicional

Fórmulas Atómicas

Cada una de las combinaciones que resultan de poner cada una de las especies en un tanque, ha sido representada por un número, teniendo en cuenta que las especies se numeran de 1...n y los tanques por su parte,1...m.

Por ejemplo, si tenemos 3 especies y 2 tanques, las combinaciones serían:

Fórmula Atómica Especie Tanque
1 1 1
2 1 2
3 2 1
4 2 2
5 3 1
6 3 2


Se ha implementado una función que codifique una combinación determinada por: el número de la especie, el número del tanque y el total de tanques.

;; Codifica un par ( especie tanque ) a una fórmula atómica
;; donde m es el número de tanques
(defun codifica (especie tanque m)
  (+ (* (- especie 1) m) tanque))

Es decir,

atomo = (especie - 1) * m + tanque\,


Para la obtención de esta fórmula nos hemos basado en la cantidad de posibilidades que hay antes de que se dé el par (especie, tanque), como se observa en la tabla anterior.

Por otro lado, para decodificar la fórmula atómica, nos serviremos de la ecuación anterior. Pero estamos en un sistema de 1 ecuación y dos incógnitas; es decir, necesitamos una ecuación más para poder resolverlo. Observando la tabla de nuevo, extraemos otra propiedad:

tanque = 1 + resto(atomo - 1, m)\,


Es decir, el tanque coincide siempre con 1 más el resto de dividir atomo − 1 / m. Ya tenemos un sistema de dos ecuaciones con dos incógnitas,


atomo = (especie - 1) * m + tanque\,
tanque = 1 + resto(atomo - 1, m)\,


Despejando las incógnitas se ha implementado la función decodifica:

;; Proceso contrario a codifica
;; a partir de una fórmula atómica
;; y el número de tanques
;; determina el par ( especie tanque )
(defun decodifica (atomo m)
  (let* (
         (tanque (+ 1 (mod (- atomo 1) m)))
         (especie (/ (+ atomo (- m tanque )) m)))
     (list especie tanque)))

Incompatibilidades

Para el manejo de las incompatibilidades, éstas se deberán expresar mediante listas de asociación.


En el caso de querer expresar que:

en el tanque 1 no se pueden producir la especie 2 ni la 3 \Rightarrow ( (1 2 3) )


Es decir, los elementos que conforman la lista de incompatibilidades tanque-especie, tienen siempre el mismo formato: el primer elemento representa la identificación del tanque, y la lista restante, se corresponde con las especies que no se pueden producir en dicho tanque.

Análogamente para las especies, por ejemplo:

la especie 1 no puede convivir con la 2 \Rightarrow ( (1 2) )


Con este ejemplo queremos reflejar que la lista de incompatibilidades no debe expresar todos los posibles conflictos en todos los sentidos; es decir, no es necesario incluir en la lista, la incompatibilidad de la especie 2 con la 1: ( (1 2) (2 1) ).

No obstante, si algún tanque o especie no presenta incompatibilidades, éste no aparecerá en la lista.

Forma Normal Conjuntiva (FNC)

La piscifactoría devolverá una lista de cláusulas en formato Lisp, que constituyen la forma normal conjuntiva que nos permitirá demostrar si se pueden producir las especies en la piscifactoría, teniendo en cuenta las restricciones mencionadas.

Esto nos permitirá comprobarlo directamente con el algoritmo DPLL y con SATO.

El esquema que nos devuelve la función piscifactoria se correspone con:

  • Cláusulas de incompatibilidades tanque-especie
  • Cláusulas de combinaciones especie-tanque
  • Cláusulas de incompatibilidades especie-especie

Es decir, un primer bloque de cláusulas que representan las incompatibilidades tanque-especie. Un segundo bloque con todas las posibilidades de estar las especies en los tanques. Y finalmente las cláusulas que expresan las incompatibilidades especie-especie.

El primer bloque es generado por genera-incomp-tanque-especie, el segundo genera-posibilidades y el tercero por genera-incomp-especie-especie. Además, se genera en forma normal conjuntiva. A continuación se demuestra cómo, para un ejemplo de 2 tanques y 3 especies.

Generación de ejemplares

Función principal

Implementación
(defun piscifactoria (m n incomps-tanque-especie incomps-especie-especie)
 (append
  (genera-incomp-tanque-especie incomps-tanque-especie m)
  (append
   (genera-posibilidades m n)
   (genera-incomp-especie-especie (preprocesa-incomps-especie-especie incomps-especie-especie) m))))
Tests
;; Es consistente
(assert-event (equal (piscifactoria 3 3 '((1 1) (2 2) (3 3)) '((1 2 3)))
                  '((-1)
                   (-5)
                   (-9)
                   (1 2 3)
                   (4 5 6)
                   (7 8 9)
                   (-1 -4)
                   (-2 -5)
                   (-3 -6)
                   (-1 -7)
                   (-2 -8)
                   (-3 -9))))
;; Es inconsistente
(assert-event (equal (piscifactoria 3 3 '((1 1 2 3) (2 1 3) (3 1)) '())
                   '((-1)
                    (-4)
                    (-7)
                    (-2)
                    (-8)
                    (-3)
                    (1 2 3)
                    (4 5 6)
                    (7 8 9))))

Generar todas las posibilidades especie-tanque

Implementación
;;Función auxiliar: genera posibilidades para
; una especie a partir del tanque actual 
; 'tanque', y m el total de tanques
(defun posibilidades-especie (especie tanque m)
 (if (> tanque m)
     nil ;;No quedan tanques
     (cons
        (codifica especie tanque m)
        (posibilidades-especie especie (+ tanque 1) m))))
;; Función principal: generar posibilidades
;  para un total de especies 'n' y un total
;  de tanques 'm'
(defun genera-posibilidades (m n)
  (if (zp n)
      nil ;; No hay especies
      (if (zp m)
	  nil ;; No hay tanques
	  (append
	    (genera-posibilidades m (- n 1))
	    (list (posibilidades-especie n 1 m))))))

Tests
(assert-event (equal (genera-posibilidades 2 3)
  '((1 2) (3 4) (5 6))))
(assert-event (equal (genera-posibilidades 3 3)
  '((1 2 3) (4 5 6) (7 8 9))))
(assert-event (equal (genera-posibilidades 3 1)
  '((1 2 3))))

Generar incompatibilidades tanque-especie

Implementación
;;Función auxiliar: genera las incompatibilidades
; para un tanque 'tanque', donde m es el total
; de tanques
(defun incompatibilidades-tanque (tanque incomp-tanque m)
  (if (endp incomp-tanque)
      nil ;;No quedan incompatibilidades
      (cons (list (- (codifica (car incomp-tanque) tanque m)))
	    (incompatibilidades-tanque tanque (cdr incomp-tanque) m))))
;; Función principal: generar incompatibilidades
;  tanque-especie dadas por la lista de asociacion
;  incomp-tanques para un total de tanques 'm'
(defun genera-incomp-tanque-especie (incomp-tanques m)
  (if (endp incomp-tanques)
      nil ;; No hay más incompatibilidades
     (append
       (incompatibilidades-tanque (car (car incomp-tanques)) (cdr (car incomp-tanques)) m)
        (genera-incomp-tanque-especie (cdr incomp-tanques) m))))
Tests
(assert-event (equal (genera-incomp-tanque-especie '() 3)
   NIL))
(assert-event (equal (genera-incomp-tanque-especie '((1 2 3) (3 1)) 3)
   '((-4) (-7) (-3))))
(assert-event (equal (genera-incomp-tanque-especie '((1 2 3) (3 1)) 4)
   '((-5) (-9) (-3))))
(assert-event (equal (genera-incomp-tanque-especie '((2 3) (3 1)) 4)
   '((-10) (-3))))

Generar incompatibilidades entre especies

Implementación
;;Función auxiliar: genera una incompatibilidad
; que describe que todas las especies de 'especies'
; no pueden estar en el mismo tanque 'tanque'.
; Donde m es el total de tanques
(defun incomp-especies-tanque (especies tanque m)
  (if (endp especies)
      nil ;;No quedan especies
      (cons (- (codifica (car especies) tanque m))
       (incomp-especies-tanque (cdr especies) tanque m))))
;;Función auxiliar: genera las incompatibilidades
; que describen que el grupo de especies 'especies'
; no pueden estar en los mismos tanques, comprendidos
; de 'tanque' a 'm'. Donde m es el total de tanques
(defun incomp-especies-tanques (especies tanque m)
  (if (> tanque m)
      nil ;;No quedan especies
      (cons
           (incomp-especies-tanque especies tanque m)
           (incomp-especies-tanques especies (+ tanque 1) m))))
;; Función principal: generar incompatibilidades
;  especie-especie dadas por la lista de asociacion
;  incomp-especies para un total de tanques 'm'
(defun genera-incomp-especie-especie (incomp-especies m)
 (if (endp incomp-especies)
     nil ;;No quedan incompatibilidades
    (append
     (incomp-especies-tanques (car incomp-especies) 1 m)
     (genera-incomp-especie-especie (cdr incomp-especies) m))))
Tests
(assert-event (equal (genera-incomp-especie-especie '() 3)
		     nil))
(assert-event (equal (genera-incomp-especie-especie '((1 2) (1 3)) 3)
		     '((-1 -4)
		       (-2 -5)
		       (-3 -6)
		       (-1 -7)
		       (-2 -8)
		       (-3 -9))))
(assert-event (equal (genera-incomp-especie-especie '((1 2) (1 3) (3 4) (3 5) (4 5)) 3)
		     '((-1 -4)
		       (-2 -5)
		       (-3 -6)
		       (-1 -7)
		       (-2 -8)
		       (-3 -9)
		       (-7 -10)
		       (-8 -11)
		       (-9 -12)
		       (-7 -13)
		       (-8 -14)
		       (-9 -15)
		       (-10 -13)
		       (-11 -14)
		       (-12 -15))))

Análisis de pruebas

A continuación se efectuarán una serie de pruebas. Comprobaremos si el funcionamiento del sistema implementado para resolver el problema de la piscifactoría es correcto. Emplearemos para ello diferentes restricciones entre tanque-especie y especie-especie que permitan obtener resultados del tipo:

  • Satisfacible
  • Insatisfacible

Satisfacible

Ejemplo 1
(piscifactoria 3 3 ’((1 1) (2 2) (3 3)) ’((1 2 3)))
  • Tanques: m = 3
  • Especies: n = 3


Salida SATO Salida DPLL

SATO nos dice que ha encontrado el modelo compuesto por los átomos 2, 4 y 7. Si aplicamos la función decodifica para saber a qué combinación hacen referencia obtenemos:

Fórmula Atómica Especie Tanque
2 1 2
4 2 1
7 3 1

Efectivamente las 3 especies se han podido distribuir en tanques. Las especies 2 y 3 se sitúan ambas en el tanque 1, ya que no existen restricciones entre ellas.

Ejemplo 2
(piscifactoria 3 3 ’((1 1 2 3) (2 2) (3 3)) ’((2 3)))
  • Tanques: m = 3
  • Especies: n = 3
Salida SATO Salida DPLL

SATO nos dice que ha encontrado el modelo compuesto por los átomos 2, 3, 6 y 8. Este camino es el único que se puede dar. Procedemos de forma similar para comprobar la validez:

Fórmula Atómica Especie Tanque
2 1 2
3 1 3
6 2 3
8 3 2

Las 3 especies se han podido distribuir entre los diferentes tanques. Podemos comprobar que las especies 2 y 3 no pueden estar juntas en el mismo tanque, es por ello que están en el 3 y 2, respectivamente.

Insatisfacible

Ejemplo 1
(piscifactoria 3 3 '((1 1 2 3) (2 3) (3 3)) '((1 2 3) (2 3)))
  • Tanques: m = 3
  • Especies: n = 3


Salida SATO Salida DPLL

SATO y DPLL nos dicen que no han encontrado ningún modelo (insatisfacible). Luego no se pueden producir las especies en la piscifactoría. Veámos que ocurre:

Restricciones tanque-especie.
Restricciones especie-especie.

En la primera de las figuras (restricciones tanque-especies) se aprecia claramente que en el tanque 1 no pueden existir especies. En el tanque 2 pueden estar las especies 1 y 2. En el tanque 3 pueden estar las especies 1 y 2.

En la segunda figura, tenemos en cuenta las restricciones entre especies y comprobamos que la 1 y la 2 no pueden estar juntas en el mismo tanque, así que suprimimos una especie en cada tanque. También sería una solución insertar en el tanque 2 la especie 1 y en el tanque 3 la especie 2, sería igual de válida.


Ejemplo 2
(piscifactoria 3 3 '((1 1 2 3) (2 1 3) (3 1)) '())
  • Tanques: m = 3
  • Especies: n = 3


Salida SATO Salida DPLL

SATO de nuevo nos dice que no ha encontrado ningún modelo. Y por tanto, no se pueden producir las especies en la piscifactoría. Vamos a ver que sucede:

Restricciones tanque-especie.

En este caso no hay restricciones entre especies. En el tanque 1, como sucedía anteriormente, no se puede utilizar ninguna especie. En el tanque 2 no se pueden emplear las especies 1 y 3, así que se producirá la 2. En el tanque 3 no se puede producir la especie 1, pero sí las especies 2 y 3.

Podemos comprobar que la especie 1 no aparece en ningún tanque, luego esta distribución es insatisfacible (no están todas las especies en la piscifactoría).

Pruebas costosas

Emplearemos 25 especies y 7 tanques para poner a prueba el sistema implementado en DPLL. En primer lugar usaremos una distribución que haga el problema satisfacible. Posteriormente, haremos que las 25 especies sean incompatibles entre sí, siendo imposible una distribución entre tan solo 7 tanques.

Satisfacibilidad
Salida SATO Salida DPLL

La salida de SATO es inmediata. DPLL demora algo más, unos 14 segundos, pero consigue mostrar el resultado.

Insatisfacibilidad
Salida SATO Salida DPLL

La salida de SATO es inmediata nuevamente. DPLL emplea tanto tiempo que la ejecución ha tenido que ser abortada, ya que no podemos obtener un resultado para el mismo en un tiempo prudencial estipulado.

Herramientas personales