Descarga de #SAT Solver

21

¿Alguien podría señalar uno o más sitios web donde sea posible descargar una implementación funcional de un solucionador #SAT? Estoy interesado en aquellos que devuelven el recuento exacto de la solución, no una aproximación.

ds.algorithms sat software Giorgio Camerani
fuente
2
Hola Walter, tu pregunta está cerca del límite de lo que oficialmente sería "sobre el tema" para este sitio. Sin embargo, si no tiene otro lugar para hacer esta pregunta y podemos responderla, tal vez no sea tan malo ... (Dado que el sitio aún está en desarrollo, creo que estamos siendo más abiertos que otros sitios). que el objetivo de este comentario no es "regañar" o "advertir", es solo un aviso amistoso.
Ryan Williams
Hola Ryan, gracias por tu aviso. Lo siento si esta pregunta está cerca de la frontera. Busqué en la web y no encontré nada: solo algunos solucionadores SAT, pero no solucionadores #SAT. Por eso he preguntado aquí. Por supuesto, sé que puedo escribir mi propio código que usa un solucionador SAT como motor para contar soluciones, pero estaba buscando algo ya hecho y listo para usar.
Giorgio Camerani
12
Me gustaría estar en desacuerdo. Creo que tales preguntas están dentro del alcance, ¡y deberían estarlo!
Suresh Venkat
de acuerdo en su alcance. digo / no es demasiado práctico construir un solucionador #SAT a partir de un solucionador SAT a menos que uno tenga el código fuente e incluso en ese caso, no es tan práctico, excepto por fórmulas muy pequeñas, debido a una explosión exponencial muy mala. generalmente se requerirían técnicas especiales exclusivas de #SAT y no SAT ...
vzn

Respuestas:

16

Puede hacer esto con SAT4J , simplemente iterando sobre todos los modelos: http://www.sat4j.org/howto.php#models . Me imagino que la mayoría de los solucionadores de SAT tienen esta habilidad.

Dave Clarke
fuente
Hola supercooldave, gracias por tu puntero. No sabía que SAT4J tenía esta habilidad.
Giorgio Camerani
16

También puede probar el solucionador #SAT "sharpSAT" ( sitio web , github ) para contar el número de asignaciones satisfactorias de fórmulas CNF.

Holger
fuente
11

Una opción es usar una biblioteca BDD, como JavaBDD . Todas estas bibliotecas tienen una función que cuenta las soluciones rápidamente o, al menos, facilitan la escritura de dicha función. La desventaja, sin embargo, es que la construcción del BDD será lenta en muchos casos y puede requerir mucha memoria.

metronorteO(metronorte)∼metro+norte

Radu GRIGore
fuente
7

Tema relacionado: Mejor solucionador SAT .

MS Dousti
fuente
1
Gracias sadeq El tema que indicó parece tener una orientación teórica. Enumera varios documentos sobre la disminución del límite superior. Es muy interesante, pero estaba buscando una implementación de trabajo lista para usar.
Giorgio Camerani
2
De nada. Entre los enlaces citados allí, había uno que era puramente práctico: satcompetition.org . Creo que puedes encontrar muy buenas implementaciones allí.
MS Dousti
7

Lo mejor que encontré es "compilador c2d". http://reasoning.cs.ucla.edu/c2d/

Utiliza d-DNNF y necesita la opción -count .

Leon Leon
fuente
c2d resuelve mucho más CNF que sharpsat. Para propósitos de juguete , el solucionador de sat "relsat" también lo hará.
Leon Leon
7

El MBound Solver que se proporciona aquí http://www.cs.cornell.edu/~sabhar/ puede proporcionar recuentos de modelos con garantías probabilísticas. Es mucho más rápido que enumerar todas las soluciones.

Optar
fuente
5

Escribí un modelo pequeño / enumerador implicante principal . Esto ya se puede usar para el conteo de modelos con la enumeración de modelos, pero eso no es muy práctico. Si alguien está interesado, puedo extenderlo para que cuente modelos de implicantes principales.

Mikolas
fuente
2

El sitio web BeyondNP contiene un buen inventario de las herramientas existentes para resolver #SAT (y otros problemas difíciles relacionados con las fórmulas CNF). También puede encontrar una lista de herramientas para el conteo aproximado de modelos y la compilación de conocimientos (la tarea de transformar el CNF en una estructura de datos con suerte sucinta que a menudo admite el conteo de modelos de tiempo polinomiales).

También puede encontrar una lista de herramientas para preprocesar fórmulas CNF que pueden ser útiles para mejorar el rendimiento de los contadores de modelos y varios puntos de referencia .

holf
fuente