Por Huberto Ayanegui Santiago , José María Vega Ramos , Enrique Ayala Franco
 

                                                                                    ABSTRACT

Este trabajo de investigación tiene como finalidad presentar la aplicación de SAT en problemas NP-completos. Nuestro survey se orienta a resolver el problema de encontrar el número cromático X(G) del grafo G así como la coloración correcta de dicho grafo a través del problema de satisfactibilidad. Presentamos el proceso de reducción de un grafo a la forma normal conjuntiva así como la interpretación de la solución SAT al dominio de grafos. En resumen, presentamos como resolver el método de coloración de grafos a través de la solución de SAT por Davis & Putnam.

INTRODUCCIÓN AL PROBLEMA DE SATISFACTIBILIDAD

El estudio de algoritmos y problemas que giran alrededor de SAT es una de las áreas más fascinantes de la computación, debido a que el enfoque está basado en la solución de  problemas que demandan una búsqueda de estado(s) que satisfagan a ciertos eventos del problema.
El problema llamado SAT , es un problema concerniente a la Lógica Matemática. El enfoque de SAT es tratar con formulas lógicas que han sido abstraídas de problemas reales.  La solución de SAT consiste en satisfacer con un valor de verdad la conjunción de estas n cláusulas (Formulas Bien Formadas),  las cuales contienen i literales o proposiciones que pueden ser calificadas con un valor de verdad.

Podemos hacer una analogía con una ecuación de primer grado x+1=2 , donde el objetivo es averiguar el valor para x, el cual satisfaga el resultado que es 2. Esto es parecido a lo que es un problema SAT , nada mas que en SAT se busca encontrar asignaciones de verdad en la mayoría de los casos para muchas literales o proposiciones y los únicos valores que pueden ser asignados a estas literales son falso o verdadero.

 Para resolver los problemas SAT han sido propuestos infinidad de algoritmos los cuales han sido clasificados por su alcance principalmente en Completos: los que pueden probar Insatisfactibilidad, y los Incompletos: los que no pueden probar Insatisfactibilidad y por su eficiencia en las distintas áreas de aplicación. También se han diseñado técnicas de modelado para llevar un problema especifico de una área especifica a un problema SAT.

 El problema de satisfactibilidad fue el primer problema catalogado como NP-completo por Stephen Cook en 1971.
 

COLORACIÓN DE GRAFOS

EL problema de Coloración de Grafos consiste en la asignación de colores a un conjunto de n vértices, dado un grafo no dirigido con la única condición que para todo par de vértices adyacentes estos no sean coloreados del mismo color (véase figura 1) .

                                                                                Figura 1
 

DEFINICIÓN FORMAL

Considere un grafo G=(V,E) con el conjunto de vértices V y conjunto de aristas E. Una coloración-K de G es una partición de V en subconjuntos K, V1,....,Vk tal que no hay dos vértices en el mismo conjunto que son adyacentes. Es decir, si v,w pertenecen a Vi, 1<=i<=k entonces v,w no pertenecen a E. Los conjuntos V1,...,Vk se refieren como a clases de colores o colores. El número cromático X(G) es definido como el k mínimo para el cual G es coloreable. El problema de coloración puede definirse así: Dado un grafo G, encuentre X(G) y la coloración correspondiente. La coloración de grafos es conocida como un problema NP-completo [Garey-Johnson 1979, Littman, 1997].
 

APLICACIONES DE LA COLORACIÓN DE GRAFOS

Hay numerosas aplicaciones prácticas de coloración de grafos. Incluyendo: calendarización de exámenes [Wood, 1969]; El diseño y operación de Sistemas de Manufactura Flexible [Stecke, 1985], y cálculo de elementos Jacobianos dispersos por diferenciación finita en programación matemática [Coleman y More, 1983].
 

¿POR QUÉ RESOLVER EL PROBLEMA DE COLORACIÓN DE GRAFOS COMO UN PROBLEMA SAT?

La idea de atacar el Problema de Coloración de Grafos como un problema de Satisfactibilidad, viene de ilustrar la diversidad de aplicaciones en el contexto de SAT, en este caso, el problema de coloración de grafos. Además, existe infinidad de herramientas (algoritmos), que resuelven eficientemente el problema de Satisfactibilidad, de manera que si un problema puede ser mapeado a un problema SAT, simplemente aplicaremos un algoritmo ya existente para obtener resultados.
 Es claro que si tenemos un algoritmo que resuelve SAT, podremos solucionar entonces el problema de coloración de grafos, y como veremos más adelante, el proceso de reducción de un grafo a cláusulas es muy fácil. Por tanto, consideramos que esta forma de solucionar coloración de grafos es un método muy fácil de implementar y rápido.
 

MÉTODO PROPUESTO PARA LA SOLUCIÓN A TRAVÉS DE SAT

 El método que proponemos para resolver el problema  de coloración de grafos, es solucionándolo a través de SAT. Es decir,  mostraremos la forma de traducir los vértices y aristas de un grafo (G) a un conjunto de cláusulas en la Forma Normal Conjuntiva (FNC). Una vez presentado en esta forma, aplicaremos un método completo para la solución de SAT, con el fin de hallar a los valores de verdad que satisfacen a la fórmula. Cuando hallemos este conjunto, lo que resta es regresar estos valores al contexto de grafos, a fin de obtener el número cromático X(G) así como los colores válidos en cada vértice.

La Figura 2, resume el procedimiento descrito anteriormente:

                                                                 Fig.2 Descripción del proceso completo.
 

 Una vez que hemos encontrado a X’(G), entonces ya tenemos el número cromático del grafo G (que es X’(G)). Para hallar la coloración de los vértices, proponemos obtener los colores de las cláusulas que indican el color de cada vértice, es decir Cij (donde j es el número de color del i-ésimo nodo). Este proceso se detallará más adelante.

A continuación comenzamos a describir detalladamente cada componente de la figura 2.
 

CONVERSIÓN DE UN GRAFO A FNC´s

Supongamos que tenemos el grafo de cuatro vértices de la figura 3.
 

Para este ejemplo, hacemos X’(G)=2 (si asignamos a 1 el posible número cromático el ejemplo no será poco ilustrativo). Ahora,  podríamos preguntarnos si ¿es posible colorear el grafo de la figura 3 con 2 colores?.

Para contestar a esa pregunta, comenzamos nuestro proceso convirtiendo el grafo a cláusulas en la forma normal conjuntiva.

En la siguientes notación, cada xi,j corresponde a la afirmación de que el vértice xi, ha sido coloreado con el color j.

Las siguientes cláusulas aseguran que cada vértice tiene al menos un color.

{x1,1, x1,2}
{x2,1, x2,2}
{x3,1, x3,2}
{x4,1, x4,2}

Las siguientes cláusulas especifican que ningún vértice tiene asignado los colores 1 y 2.

{~x1,1, ~x1,2}
{~x2,1, ~x2,2}
{~x3,1,~x3,2}
{~x4,1, ~x4,2}

El significado de las ocho cláusulas anteriores se puede traducir como: “Cada vértice ha sido coloreado en uno y solamente un color”.

Ahora, lo que hace falta traducir del grafo de la figura 3 son las restricciones inherentes al problema de coloración de grafos. Es decir, que ninguno de los extremos de una arista sea coloreado con un mismo color. Para esto, observando la figura 3 vemos que hay 4 aristas, donde la arista a tiene como extremos a x1 y x 3 , por tanto proponemos la siguiente cláusula:

{~x1,1,~x 3,1).

Planteando así todas estas cláusulas de las aristas a,b,c y d, tenemos:

{~x1,1,~x 3,1)
{~x1,2,~x 3,2)
{~x1,1,~x 2,1)
{~x1,2,~x 2,2)
{~x2,1,~x 4,1)
{~x2,2,~x 4,2)
{~x3,1,~x 4,1)
{~x3,2,~x 4,2)
 

Hasta aquí ya tenemos al conjunto de 16 cláusulas que se presentan en su forma normal conjuntiva:

(1)
{x1,1, x1,2},{x2,1, x2,2},x3,1, x3,2},{x4,1, x4,2},{~x1,1, ~x1,2},{~x2,1, ~x2,2},{~x3,1,~x3,2},{~x4,1, ~x4,2},{~x1,1,~x 3,1),{~x1,2,~x 3,2),{~x1,1,~x 2,1),{~x1,2,~x 2,2),{~x2,1,~x 4,1),{~x2,2,~x 4,2),{~x3,1,~x 4,1) ,{~x3,2,~x 4,2)
 

APLICACIÓN DE UN MÉTODO COMPLETO SAT

Ahora aplicaremos a la fórmula (1) un método completo para solucionar el problema de SAT. Existen varios métodos completos como son:

· Davis&Putman(1960)
· Principio de Resolución de Robinson (J.A. Robinson 1965)
· N Literales (JFS)
· 2 Literales (Adrian Ruiz)
· Petrolani (1993)
· GRASP (por Joao P. Marques da Silva)
· NTAB (por James Crawford's )
· POSIT (por Jon W. Freeman)
· REL_SAT (por Roberto Bayardo)
· SATO (por Hantao Zhang)
· Satz213 (por Chu-Min Li)
· Satz-rand (por Henry Kautz)

Para este trabajo hemos escogido el conocido método de Davis & Putnam, el cual describimos a continuación:
Consiste en el uso iterativo de cuatro reglas que permiten realizar la comprobación de la insatisfactibilidad de un conjunto de cláusulas. Estas reglas permiten ir reduciendo la cantidad de cláusulas hasta llegar al punto en que se tiene un formula que es valida o que es insatisfactible y que contiene el mínimo numero de cláusulas.

A continuación se describe cada una de estas reglas:
Sea S un conjunto de cláusulas instanciadas en el universo de Herbrand.

1. Regla de la Tautología
Borre todas las cláusulas aterrizadas de S que son tautologías. El conjunto resultante S’ es insatisfactible si y solo si lo es.

2. Regla de la Literal Unitaria
Si existe una cláusula aterrizada unitaria L en S, obtenga S’ de S al borrar aquellas cláusulas en S que contengan L. Si S’ esta vació, S es satisfactible. De los contrario, obtenga un conjunto  S’’ de S’ al borrar >> L. S’’ es insatisfactible si y solo si S lo es. Note que si >> L es una cláusula aterrizada unitaria, entonces la cláusula se convierte a una cláusula vacía cuando >> L es borrada de la cláusula.

3. Regla de la Literal Pura
Una literal L en una cláusula aterrizada de S, se dice que es pura en S si y solo si la literal >> L no aparece en ninguna cláusula aterrizada en S. Si una literal L es pura en S, borre todas las cláusulas aterrizadas que contengan L. El conjunto S’ que resulta de esto, es satisfactible si y solo si S lo es.

4. Regla de Expansión
Si el conjunto S puede ser puesto en la forma (A1_L)^:::^(Am_L)^(B1_>>L)^:::^(Bn_>>L)^R, donde Ai;Bi; y R están libres de L y >> L, entonces obtenemos los conjunto S1 = A1^:::Am^R y S2 = B1^:::Bn^R. S es insatisfactible si y solo si (S1_S2) es insatisfactible, esto significa que S1 y S2 también lo son.
 

PROCESO DE INTERPRETACIÓN

De esta manera, aplicamos este método completo a la fórmula (1) y si hay valores de verdad que satisfacen a dicha fórmula,  entonces habremos encontrado una parte de lo que buscamos: el número cromático X’(G) para el cual se obtuvo satisfactibilidad en la fórmula normal conjuntiva.

 Para obtener la segunda parte de la solución, es decir, la coloración correcta de cada vértice xi, proponemos hacer una búsqueda en (1) de proposiciones xi,j que sean verdaderas. Esto significa, encontrar el color j del vértice i.

 Con esto damos por terminado el proceso de solución al problema de coloración de grafos a través de SAT.
 

CONCLUSIONES

 Hemos presentado una de las aplicaciones de SAT  a un problema NP-completo. Vemos que es posible reducir un grafo a cláusulas en la forma normal conjuntiva para ser solucionado a través de un método completo (Davis-Putnam). La solución nos indica tanto el número cromático como la coloración de cada vértice. Por tanto, es claro que si logramos abstraer un problema del mundo real y plantearlo como un problema SAT, entonces podemos hallar la solución (si existe) como un problema de decisión, y encontrar los valores de las proposiciones, como un problema de optimización.

 Han habido muchos resultados de investigación en métodos que solucionan el problema SAT, por eso creemos que el proceso de reducción de un problema a SAT tiene grandes ventajas. Una desventaja clara es la complejidad de esta reducción sea la representación a cláusulas en su forma normal conjuntiva sin descuidar al tiempo como un factor clave involucrado en este proceso.
 
 

BIBLIOGRAFÍA

 Coleman, T. F. y J.J. More (1983) “Estimation of Sparse Jacobina Matrices and Graph Coloring Problems”, SIAM J. Numer. Anal., vol. 20, no. 1, pp.187-209
 Stecke, K [1985], “Design Planning, Scheduling and Control Problems of Flexible Manufacturing”. Annals of Operation Research, vol. 3., pp.3-12
 Wood D.C. (1969) “A Technique for Coloring a Graph Applicable to Large Scale Timetable Problems”, Computer Journal, vol. 12, pp.317-322.
M.Garey, D.Johnson.(1979) Computers and intractability. A guide to the theory of NP-completeness. W.H. Freeman New York, 1979.

Littman, Michael L.
http://www.cs.duke.edu/~mlittman/courses/Archive/cps13097/lectures/lect23/node16.html