Encuesta de transformaciones relacionadas con el uso de solucionadores SAT

13

Estoy comenzando a investigar la posibilidad de confiar en un solucionador SAT para abordar un problema de optimización que me interesa, y actualmente estoy buscando una encuesta que presente ejemplos de transformaciones "inteligentes" a variantes de SAT (es decir, transformaciones que resultan en un problema de tamaño razonable, ya que no estoy interesado en probar resultados de dureza sino en resolver el problema), aproximadamente en el espíritu de lo que se puede encontrar en la encuesta sobre gráficos cúbicos de Greenlaw y Petreschi , si se puede hacer alguna comparación hecho entre los dos.

¿Me ha eludido una encuesta de este tipo porque no existe o porque me la perdí?

ds.algorithms reference-request sat optimization Anthony Labarre
fuente
¿Qué quieres decir exactamente con "variantes de SAT"?
Giorgio Camerani
k
44
No te preocupes, es la palabra correcta, debería haberlo entendido. Sin embargo, desde un punto de vista puramente práctico, no creo que importe (lo que más importa es lo parsimoniosa que es su codificación). ¿Podría proporcionar más detalles sobre el problema de optimización que está tratando de resolver? Estoy muy interesado en las aplicaciones prácticas de SAT y en los aspectos de ingeniería de la resolución de SAT.
Giorgio Camerani
Suena un poco confuso que estés hablando de un problema de optimización, pero al mismo tiempo sobre SAT. Por lo general, para optimizar, necesita algo más fuerte, por ejemplo, MAX-SAT. Tal vez podrías aclarar eso.
Mikolas
esta pregunta podría estar algo relacionada: cstheory.stackexchange.com/q/4314/4506
Mikolas

Respuestas:

9

No estoy seguro de si eso es lo que está buscando, pero aquí hay uno: JM Silva, Aplicaciones prácticas de satisfacción booleana .

Mikolas
fuente
2
No pude acceder a través de su enlace, aquí hay otro . A primera vista, el artículo parece bastante interesante, pero más centrado en las aplicaciones que en lo que estoy buscando.
Anthony Labarre
@Anthony, bueno, dijiste que estás interesado en el aspecto práctico :-) De todos modos, los solucionadores principales existentes realmente no diferencian entre los diferentes tipos de SAT. En el pasado, se ha trabajado en explotar cláusulas binarias, por ejemplo. Pero los solucionadores existentes solo usan DPLL + unidad prop + cláusula de aprendizaje. Sin embargo, algunos de los preprocesadores explotan la estructura. Pero, de nuevo, no desde el punto de vista de la complejidad. clasificación.
Mikolas
8

El Capítulo 2 del Manual de Satisfacción analiza los aspectos a tener en cuenta al diseñar esas transformaciones, así como una lista de referencias que responden a mi pregunta. Esto me ayudó a encontrar algunos ejemplos en los que uno puede echar un vistazo para familiarizarse con estas transformaciones:

Anthony Labarre
fuente