Diseño de un algoritmo para el conteo de modelos de formulas booleanas en dos forma normal conjuntiva

Abstract

El conteo de modelos sobre fórmulas booleanas es el problema conocido como #SAT, el cual forma parte de los problemas catalogados como #P-Completos. #2SAT es una restricción a #SAT, donde las cláusulas que componen una fórmula contienen a lo m as dos variables, uno de los métodos usados para resolver este problema es la descomposición de la fórmula, la cual puede realizarse por la asignación de valores de verdad a una variable o a una cláusula. La descomposición de una fórmula por variable requiere un procedimiento de selección para la variable o cláusula a eliminar, el método m as utilizado es seleccionar la variable que tiene una mayor aparición en la fórmula, de esta forma se puede reducir el número de cláusulas dado el número de apariciones de la variable seleccionada. Por otro lado, la descomposición de una fórmula por cláusula requiere un método para seleccionar la cláusula m as viable a eliminar, este segundo método permite reducir la cantidad de procesos de descomposición de la fórmula con respecto a la descomposición por variable. Si se quieren eliminar dos variables por el primer procedimiento es necesario generar cuatro subfórmulas, sin embargo, con el segundo procedimiento es posible generar tres subfórmulas aprovechando la relación existente entre las dos variables que se encuentran dentro de la cláusula. El objetivo de la descomposición de la fórmula es aplicar el método de forma iterativa hasta encontrar subfórmulas que puedan ser resueltas en tiempo polinomial. Una clase de fórmulas en las cuales existe un procedimiento polinomial para calcular #2SAT es aquella en la cual sus variables aparecen a lo m as cuatro veces en la fórmula. En esta tesis se estudian clases de fórmulas cuyo conteo de modelos puede realizarse en tiempo polinomial, además se desarrollan métodos para resolverlas basados en la topología inducida por su gr a ca signada. Las topologías para las cuales se presentan algoritmos polinomiales se conocen como cactus y outerplanar. As mismo, demostramos experimentalmente que los algoritmos obtenidos son competitivos respecto a la herramienta más reciente reportada en la literatura que es sharpSAT tanto en fórmulas cactus y outerplanar como en instancias generales.