Sobre algunas clases polinomiales de satisfacibilidad: aplicaciones a la resolución de problemas geométricos

• Autores: Jose Inacio de Jesus Rodrigues
• Directores de la Tesis: José Ramón Portillo Fernández (dir. tes.)
• Lectura: En la Universidad de Sevilla ( España ) en 2009
• Idioma: español
• Tribunal Calificador de la Tesis: Eladio Domínguez Murillo (presid.) , Pedro Jorge Sequeira Cardoso (secret.) , José Cáceres González (voc.) , Alberto Márquez Pérez (voc.) , María de los Angeles Garrido Vizuete (voc.)
• Enlaces
  • Tesis en acceso abierto en: Idus
• Resumen

  • La Geometría Computacional posee un vasto campo de aplicaciones en las áreas de las Ciencias de Información Geográfica, Electrónica y Computación, entre muchas otras. En estos campos, los problemas de etiquetado de mapas, trazados de circuitos integrados o creación de diagramas de flujos y organigramas son ejemplos particulares de problemas cuyas instancias son en muchos casos reducibles al problema de satisfacibilidad proposicional (SAT). Es decir, su resolución puede ser conseguida a partir de la resolución de determinadas instancias de SAT.

    SAT es un problema NP-completo muy estudiado, fundamental en Ciencias de la Computación. A pesar de su intratabilidad, se conocen varias (sub)clases del problema que son resolubles en tiempo polinomial. En el presente trabajo presentamos una nueva clase de satisfacibilidad polinomial: PURL (PropUnit Removable Literal). La cual es, en cierto sentido, una superclase respecto a las clases de satisfacibilidad polinomiales identificadas como bien conocidas en el trabajo de Franco y van Gelder sobre este tipo de clases [FG03]. A partir de esta nueva clase se define una jerarquía de clases de satisfacibilidad, PURL C'2PURL C'�C' kPURL, en la línea de los trabajos sobre jerarquías de Gallo y Scutella.

    PURL se define a partir del concepto de literal p-eliminable. Mediante este concepto se pueden simplificar las cláusulas de una fórmula proposicional. Dado que la fórmula simplificada y la original son lógicamente equivalentes, el procedimiento de identificación y exclusión de literales eliminables puede ser adoptado como preprocesamiento para cualquier instancia de SAT. Como los literales p-eliminables son reconocibles en tiempo lineal, el preprocesamiento opera en tiempo polinomial.

    Con una codificación adecuada mediante variables lógicas de Boole, se reducen las instancias del problema UC-4P de etiquetado de puntos alineados con etiquetas cuadradas a SAT obteniéndose la clase UC-4PSAT, subclase de PURL. Por otro lado, reduciendo las instancias del problema EOSC de emparejamiento ortogonal simple en el cilindro se obtiene la clase de satisfacibilidad EOSC-SAT, subclase de 2PURL. Además del interés específico de estos problemas, la técnica utilizada puede ser adoptada para la resolución en tiempo polinomial de otros problemas.

    Las principales contribuciones del presente trabajo son, entre otras, la definición de una nueva clase de satisfacibilidad polinomial y la aplicación del concepto de literal p-eliminable a la resolución de problemas prácticos. La clase PURL contiene propiamente a todas las clases polinomiales bien conocidas. La metodología desarrollada a partir del concepto del literal p-eliminable para la resolución de las instancias de PURL, (y, por tanto, del problema de satisfacibilidad proposicional de las instancias de todas estas clases) constituye un abordaje unificador.

    En el presente trabajo también se muestra que el algoritmo de reconocimiento y eliminación de literales p-eliminables puede ser utilizado eficientemente en la resolución de algunas instancias del problema general de satisfacibilidad proposicional.

    Para concluir, en la parte final de la memoria se utiliza el concepto de literal p-eliminable para la resolución de dos problemas geométricos irresueltos hasta ahora. La misma metodología puede aplicarse en la resolución de problemas similares, de naturaleza geométrica o no.