Enumerar todas las soluciones de un problema SAT

11

Todos los solucionadores de #SAT que conozco, por ejemplo, RelSat, C2D, solo devuelven el número de instancias satisfactorias. Pero quiero saber cada una de esas instancias?

¿Existe tal solucionador #SAT o cómo debo modificar un solucionador #SAT disponible para hacer esto?

Gracias.

lo.logic sat software qsp
fuente
77
Esto a menudo se llama un "solucionador SAT de todas las soluciones", pero no parece estar disponible en el estante. Las referencias que puedo encontrar hablan de modificaciones a MiniSAT y otros solucionadores, generalmente agregando cláusulas de bloqueo para excluir una solución cuando se encuentra. Por otro lado, la mayoría de los solucionadores de restricciones permiten generar todas las soluciones de forma estándar.
András Salamon
un enfoque es una conversión CNF → DNF para la cual hay mucha literatura
vzn

Respuestas:

13

Está buscando un solucionador de SAT ALL-SAT o todas las soluciones. Este es un problema diferente de #SAT. No tiene que enumerar todas las soluciones para contarlas.

No conozco una herramienta que resuelva su problema porque las personas agregan estos algoritmos además de los solucionadores SAT existentes, pero rara vez parecen lanzar estas extensiones. A continuación se presentan dos documentos que deberían ayudarlo a modificar un solucionador de CDCL para implementar ALL-SAT.

Solucionador SAT de memoria de todas las soluciones eficientes y su aplicación a la accesibilidad , O. Grumberg, A. Schuster, A. Yadgar, FMCAD 2004

Aquí hay un artículo reciente publicado en arXiv.

Ampliación de los solucionadores SAT modernos para enumerar todos los modelos , dijo Jabbour, Lakhdar Sais, Yakoub Salhi, 2013

Puede intentar ponerse en contacto con estos autores para su implementación.

Vijay D
fuente
Para el segundo artículo solo necesita hacer clic en la primera versión v1 para verlo.
Tayfun paga el
Este artículo reciente parece relacionado: homes.cs.washington.edu/~sudeepa/UAI2013-ModelCounting.pdf
Kaveh
1
@Kaveh, creo que el OP está pidiendo un solucionador ALLSAT o una forma de convertir un solucionador #SAT en un solucionador ALLSAT. Este es un documento sobre límites inferiores para #SAT. No estoy seguro de que ayude al OP.
Vijay D
2

Encontré un documento más reciente (2014) sobre All-SAT en una conferencia VLSI, por lo que definitivamente está orientado hacia el lado práctico (que parece estar en sintonía con la pregunta del OP aquí, aunque no tanto con cstheory.SE en general):

  • "Todo-SAT usando cláusulas de bloqueo mínimo" por Yinlei Yu, Pramod Subramanyan, Nestan Tsiskaridze, Sharad Malik, VLSI Design 2014. doi: 10.1109 / VLSID.2014.22 .

Para aquellos sin una suscripción a IEEE, hay una copia gratuita en la página web de Princeton de Subramanyan . (Utiliza un servicio de intercambio de archivos para almacenar / distribuir copias de sus documentos y no estoy seguro de cuán estables son esas URL, de ahí este enlace indirecto).

La esencia de este artículo parece ser:

Nuestra contribución, el algoritmo Dec-No Disjunto, genera cláusulas de bloqueo extremadamente cortas que no contienen ninguna de las variables implicadas en el solucionador. Tenga en cuenta que normalmente la mayoría de las variables en un término satisfactorio están implícitas. Las cláusulas de bloqueo cortas son muy beneficiosas para el rendimiento del solucionador como lo demuestra la evaluación.

Su implementación se basa en MiniSat. Sin embargo, el código fuente de su extensión no parece estar disponible públicamente. Por desgracia, esto parece ser un hábito en el campo de All-SAT, por lo que los documentos en esta área que contienen resultados experimentales simplemente configuran un algoritmo más o menos simple para vencer y rara vez se pueden comparar directamente (en términos de experimentación resultados) con cualquier otro algoritmo publicado para All-SAT. El artículo de Jabbour et al. mencionado por Vijay D también es de este tipo.

Como no lo veo mencionado en la otra respuesta (pero solo en el comentario de András Salamon), la técnica de cláusulas de bloqueo [bastante popular] se introdujo en:

Efervescencia
fuente