Resumen:
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.
Descripción:
The problem of model counting on a two conjunctive normal form (2-CNF) formula, denoted as #2SAT, is analyzed by its representation on series-parallel, grids, and cubic graphs.
At present, the model counting problem does not have an efficient method to solve it in general, then the way to approach it is done based on cases that have specific characteristics,
such as those mentioned above.
Each one of these graphs represents a formula in 2-CNF, in which the vertices represent
the variables and the edges the clauses. In this way, a logic problem such as model counting
is translated into a representation that can be worked on from a computational point of
view.
In this Thesis, new methods are proposed to count models on these types of graphs using
computational representations of them, such as: trees, matrices, vectors, and graphs labeled
in vertices and edges.
Theoretical results show that the counting models on formulas, whose graph representation
is series-parallel can be done in polynomial time and for grid graphs there is an algorithm
whose complexity is lower than the last reported in the literature. On the other hand, the
experimental results show that the counting models on formulas whose representation in
graphs is cubic, the proposed heuristic algorithm improves the result of the best proposal
reported in the literature.
Excepto si se señala otra cosa, la licencia del ítem se describe cómo openAccess