Solucionador multinúcleo SAT

Estoy tratando de resolver un problema SAT de 25k cláusulas 5k variables. Como ha estado funcionando durante una hora (precosat) y me gustaría resolver los más grandes después, estoy buscando un SAT-Solver multinúcleo.

Como parece haber muchos solucionadores SAT, estoy bastante perdido.

¿Alguien podría señalarme el mejor para mi caso?

También sería feliz si alguien me pudiera dar el tiempo aproximado (si es posible).

Echa un vistazo a los resultados de la competencia SAT 2013 de este año . En base a estos resultados, definitivamente pruebe Lingeling . Plingeling es la variante paralela de la misma.

Si no necesita demostrar su insatisfacción (tal vez sepa que la instancia es satisfactoria y solo necesita conocer una tarea que la haga SAT), también puede probar los métodos de búsqueda locales.

No estoy seguro de la existencia de prácticos solucionadores de satélite multinúcleo, pero hay algunos proyectos y documentos:

• Una breve descripción de los solucionadores de SAT paralelos modernos
• Solución asincrónica de SAT incremental multinúcleo
• cmcSAT - Un solucionador cooperativo SAT de múltiples núcleos
• Mejora de la eficiencia del solucionador SAT utilizando un enfoque cooperativo multinúcleo
• ManySAT: un solucionador paralelo SAT (sitio)
• PMSat: una versión paralela de minisat (descarga, manual)
• Plingeling (sitio)
• SArTagnan: un solucionador de SAT de cartera paralela con uso compartido de cláusulas físicas sin bloqueo (fuente)
• ppfolio (sitio)
• antom
• PMiniSat
• MiraXT , PaMiraXT: Solución paralela de SAT con hilos y paso de mensajes (binario)

También encontré este punto interesante: puede ejecutar un solucionador de satélites regular varias veces con diferentes semillas en el mismo problema en paralelo, para obtener un efecto multinúcleo.

Editar: Incorporando mis comentarios sobre la idea de vzn aquí:

Un método alternativo similar es simplemente elegir una sola variable, establecer su valor en verdadero y enviarlo a una instancia de solucionador. Establezca su valor en falso y envíelo a otra instancia de solucionador. Puede hacer esto para variables, y ejecutar procesos simultáneamente. Elegir las variables para establecer podría ser un poco complicado, es decir. si dependen directamente el uno del otro, entonces no tiene sentido elegir uno y luego otro. Puede ser necesario un paso de simplificación para tomar decisiones sucesivas / recursivas.2 $k$$2^k$

(También estaría contento si alguien me pudiera dar el tiempo aproximado (si es posible) para resolver un problema SAT de las variables X de las cláusulas Y).

Nadie puede darle un tiempo aproximado basado en variables, cláusulas, porque algunos problemas SAT son extremadamente difíciles de resolver (léase: no sucederán), incluso con un relativamente pequeño ; mientras que otras instancias enormes se pueden resolver relativamente rápido (y es para estas instancias que los solucionadores de satélites son útiles).n m , $m$$n$$m,n$

En realidad, hay una manera muy simple de convertir cualquier solucionador SAT en una versión paralela porque SAT es vergonzosamente paralelo en el siguiente sentido.

Elija un poder de dos para dividirlo por . Luego elija variables y asigne todos los valores booleanos posibles. Habrá fórmulas SAT resultantes después de las asignaciones. Resuelve cada uno por separado (en paralelo). Existe una solución general si existe una de las soluciones separadas y la solución completa es exactamente la unión de todas las soluciones separadas. n 2 $2^n$$n$$2^n$