DISEÑO DE UN ALGORITMO PARA EL CONTEO DE MODELOS DE FORMULAS BOOLEANAS EN 2 FORMA NORMAL CONJUNTIVA

Abstract

El problema de conteo de modelos en dos forma normal conjuntiva (2-FNC), denominado #2SAT se estudia a través de su representación en gráficas de tipo serial-paralelo, mallas y cúbicas. Hasta el momento, este problema de conteo de modelos no tiene un método eficiente que pueda resolverlo de manera general, por lo que la forma de abordarlo se realiza con base en casos que tienen características específicas, como las antes mencionadas. Cada una de estas gráficas representa una fórmula en 2-FNC, en la que los vértices representan las variables y las aristas las cláusulas. De esta forma, se traduce un problema de la lógica como el conteo de modelos a una representación sobre la que se trabaja desde él punto de vista computacional. En esta Tesis se proponen nuevos métodos para realizar el conteo de modelos sobre estos tipos de gráficas utilizando representaciones computacionales de ellos, como lo son: ´árboles, matrices, vectores, gráficas etiquetadas tanto en vértices como en aristas. Los resultados teóricos muestran que el conteo de modelos de fórmulas cuya representación en gráficas es serial-paralelo se puede realizar en tiempo polinomial y para gráficas tipo malla existen un algoritmo cuya complejidad es menor a la reportada en la literatura. Por otro lado los resultados experimentales muestran que el conteo de modelos sobre f´ormulas cuya representaci´on en gr´aficas es cúbica el algoritmo heur´ıstico propuesto mejora el resultado de la mejor propuesta reportada tambien en la literatura.