Hacer competidores de SAT competitivos con algoritmos especializados

11

¿Cuáles son los obstáculos para hacer que los solucionadores SAT sean competitivos con algoritmos gráficos especializados? En otras palabras, ¿es factible esperar solucionadores de SAT que puedan reemplazar el rol de diseñador de algoritmos, es decir, poder reconocer automáticamente la estructura del problema y luego resolverlo tan rápido como un algoritmo especializado?

Aquí algunos ejemplos que creo son desafiantes para los solucionadores de SAT de hoy:

  • Contando conjuntos independientes de tamaño . La codificación "x es un conjunto independiente de tamaño k" proporciona una fórmula grande que es difícil de resolver. Un solucionador de SAT ideal reconocería que este problema es fácil en el gráfico de ancho de árbol acotado con la adición de una variable adicional de "conteo" para bolsas.k

  • Encontrar el árbol mínimo de Steiner. Nuevamente, el "árbol Steiner" tiene una restricción global, sin embargo, un algoritmo especializado (como aquí ) facilita la tarea al agregar una variable adicional

  • Cualquier problema que se reduzca a combinaciones perfectas planas.

Yaroslav Bulatov
fuente
¿No está pasando esto ya? Es un truco popular para reducir un problema a SAT y luego ejecutar un solucionador.
Suresh Venkat
Sí, pero ¿son competitivos? Me pregunto si hay algún solucionador SAT que pueda tomar un conjunto simple de restricciones que describan el subgrafo euleriano de un gráfico plano, y hacer #SAT en tiempo polinómico
Yaroslav Bulatov

Respuestas:

7

Hay un buen artículo que ayuda a visualizar la estructura interna de las instancias de SAT. Consulte Visualización de instancias SAT y ejecuciones del algoritmo DPLL por Carsten Sienz (aparecido en SAT 2004). Básicamente, dibuja un gráfico que el autor llama "gráfico de interacción variable" (de acuerdo con algunas reglas) para visualizar la relación entre las cláusulas satisfechas. El autor muestra esto mediante varias ejecuciones parciales de DPLL.

La afirmación principal es que estas técnicas de visualización podrían usarse para detectar la estructura y diseñar un algoritmo apropiado para ella. Sin embargo, todavía no está claro cómo podemos detectar eficientemente estructuras como la presentada en el documento. Es bien sabido que los algoritmos SAT para un problema específico se comportan mal en otros problemas. Por lo tanto, hay "no-free-lunch", aunque este reclamo no se puede establecer formalmente hasta donde yo sé.

Marcos Villagra
fuente
Creo que el teorema relevante de "no almuerzo gratis" es el "no almuerzo libre para la búsqueda" no-free-lunch.org . Básicamente, no podemos permitirnos buscar en todas las posibles estructuras problemáticas, y tenemos que sesgar nuestra búsqueda hacia estructuras particulares. Creo que está bien ya que los diseñadores de algoritmos humanos ya lo hacen
Yaroslav Bulatov