¿Se puede usar un solucionador de SAT para encontrar todas las soluciones?

Question

Escribí una respuesta a lo que pensé que era un quite interesting question, pero lamentablemente la pregunta fue eliminada por su autor antes de que pudiera publicar. Estoy publicando un resumen de la pregunta y mi respuesta aquí en caso de que pueda ser útil para cualquier otra persona.

Supongamos que tengo un solucionador de SAT que, dada una fórmula booleana en forma normal conjuntiva, devuelve una solución (una asignación de variable que satisface la fórmula) o la información de que el problema es insatisfactorio.

¿Puedo usar este solucionador para encontrar todas las soluciones?

Answer 1

Definitivamente hay una manera de usar el solucionador SAT que describió para encontrar todas las soluciones de un problema SAT, aunque puede que no sea la manera más eficiente.

Simplemente use el solucionador para encontrar una solución a su problema original, agregue una cláusula que no haga nada excepto descartar la solución que acaba de encontrar, use el solucionador para encontrar una solución al nuevo problema, y ​​así sucesivamente. Continúa hasta que obtengas un problema insatisfactorio.

---

Por ejemplo, supongamos que desea satisfacer (X or Y) and (X or Z). Hay cinco soluciones:

• Cuatro con X cierto, Y y Z arbitraria.

• Uno con X falso, Y y Z true.

Así se ejecuta el programa de solución, y digamos que le da la solución (X, Y, Z) = (T, F, F). Puede descartar esta solución --- y sólo esta solución --- con la restricción

not (X and (not Y) and (not Z)) 

Esta restricción puede ser reescrita como la cláusula

(not X) or Y or Z 

Así que ahora puede ejecutar su programa de solución de la nuevo problema

(X or Y) and (X or Z) and ((not X) or Y or Z) 

y así sucesivamente.

---

Como dije, esta es una forma de hacer lo que quiera, pero probablemente no sea la manera más eficiente. Cuando su solucionador de SAT está buscando una solución, aprende mucho sobre el problema, pero no le devuelve toda esa información, solo le brinda la solución que encontró. Cuando ejecuta de nuevo el solucionador, tiene que volver a aprender toda la información que se descartó.

Answer 2

Sure it can.Cuando MINISAT [1] encuentra una solución

s SATISFIABLE 
v 1 2 -3 0 

(solución 1 = True, 2 = True, 3 = False), entonces usted tiene que poner en el original CNF [2] una cláusula que prohíbe esta solución:

-1 -2 3 0 

(lo que significa que, o bien 1 o 2 deben ser False o 3 deben ser True). Entonces resuelves nuevamente. Haga esto hasta que el solucionador devuelva UNSAT, es decir, que no haya más soluciones para el problema. Insertará una cláusula para cada iteración, y cada cláusula tendrá el mismo formato que la solución, excepto que está todo invertido y tiene un 0 al final

Es mucho más rápido hacerlo utilizando la interfaz C++ de MiniSat, como luego puede guardar datos intermedios y las iteraciones serán más rápidas.

[1] http://minisat.se/

[2] http://fairmut3x.wordpress.com/2011/07/29/cnf-conjunctive-normal-form-dimacs-format-explained/