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, ...