Implementación de un algoritmo para el conteo de modelos de fórmulas boleadas en 2-FNC

Abstract

En esta tesis, se propone una estrategia para el conteo de modelos convirtiendo la fórmula de entrada en un grafo. En [12] se mostró como contar modelos en tiempo polinomial en grafos cuya forma es un camino o un árbol, por lo que se tomará el procedimiento como referencia para mostrar como contar en otro tipo de grafos. Así mismo, se estudiaran fórmulas booleanas para las cuales las implementaciones existentes son computacionalmente mas costosos (en tiempo o espacio) que la que se propondrá.