Algoritmos SAT no basados ​​en DPLL

Respuestas:

21

La búsqueda de resolución (solo aplicando la regla de resolución con algunas buenas heurísticas) es otra estrategia posible para los solucionadores de SAT. Teóricamente es exponencialmente más poderoso (es decir, existen problemas para los que tiene pruebas exponenciales más cortas) que DPLL (que solo hace la resolución de árbol, aunque puede aumentarlo sin un buen aprendizaje para aumentar su poder, ya sea que lo haga tan poderoso como la resolución general todavía es abierto hasta donde yo sé) pero no sé de una implementación real que funcione mejor.

Si no se limita a completar la búsqueda, WalkSat es un solucionador de búsqueda local que puede utilizarse para encontrar soluciones satisfactorias y supera en muchos casos la búsqueda basada en DPLL. Sin embargo, no se puede usar para demostrar la insatisfacción a menos que se almacene en caché todas las tareas que han fallado, lo que significaría requisitos de memoria exponenciales.

Editar: Olvidé agregar: los planos de corte también se pueden usar (reduciendo SAT a un programa entero). En particular, los cortes de Gomory son suficientes para resolver cualquier programa entero a la óptima. Nuevamente, en el peor de los casos, puede ser necesario un número exponencial. Creo que el libro de Complejidad Computacional de Arora & Barak tiene algunos ejemplos más de sistemas de prueba que uno podría en teoría usar para algo como la resolución SAT. Nuevamente, realmente no he visto una implementación rápida de nada aparte de los métodos basados ​​en DPLL o en la búsqueda local.

Optar
fuente
99
DPLL con cláusula de aprendizaje (o buen aprendizaje, como lo llama) y reinicios ha demostrado ser equivalente a la resolución general.
Jan Johannsen
1
@ JanJohannsen, ¿es este el papel al que te refieres? arxiv.org/abs/1107.0044
Radu GRIGore
55
Sí, también hay una mejora en el siguiente documento: Knot Pipatsrisawat y Adnan Darwiche. Sobre el poder de los solucionadores de SAT de aprendizaje de cláusulas como motores de resolución. Inteligencia Artificial 175 (2), 2011, pp. 512-525. dx.doi.org/10.1016/j.artint.2010.10.002
Jan Johannsen
3
Mientras que el artículo de Beame et al. vinculado por Radu Grigore muestra que la resolución general es simulada p por un algoritmo DPLL con una estrategia particular de aprendizaje artificial, el documento anterior lo muestra para las estrategias de aprendizaje natural que realmente se utilizan.
Jan Johannsen el
12

La propagación de encuestas es otro algoritmo que se ha utilizado con éxito en algunos tipos de problemas SAT, en particular instancias SAT aleatorias. Al igual que WalkSAT, no se puede usar para demostrar la insatisfacción, pero se basa en ideas muy diferentes (algoritmos de paso de mensajes) de WalkSAT.

Timothy Chow
fuente
10

Hay solucionadores SAT basados ​​en la búsqueda local. Ver, por ejemplo, este artículo para exposición.

ilyaraz
fuente
7

También puede decir que todos los solucionadores de CSP también son solucionadores de SAT. Y hasta donde yo sé, hay dos métodos utilizados en CSP:

  • Exhaustivo DFS con eliminación del espacio de búsqueda y comprobación de la consistencia del arco, posiblemente utilizando el afeitado para garantizar que la consistencia se mantenga lo antes posible.
  • Métodos locales (búsqueda tabú, recocido simulado)
malejpavouk
fuente
4

Monte Carlo Tree Search (MCTS) recientemente ha logrado algunos resultados impresionantes en juegos como Go. La idea básica aproximada es entrelazar la simulación aleatoria con la búsqueda de árboles. Es liviano y fácil de implementar, la página del centro de investigación que vinculé contiene muchos ejemplos, documentos y algunos códigos también.

Previti y col. [1] hizo una investigación preliminar de MCTS aplicado a SAT. Llaman al algoritmo de búsqueda basado en MCTS UCTSAT ("límites de confianza superiores aplicados a los árboles SAT", si lo desea). Compararon el rendimiento de DPLL y UCTSAT en instancias del repositorio SATLIB, con el objetivo de ver si UCTSAT produciría árboles de búsqueda significativamente más pequeños que DPLL.

Para las instancias aleatorias uniformes de coloración 3-SAT y de gráfico plano de diferentes tamaños, no hubo diferencias significativas. Sin embargo, UCTSAT funcionó mejor para instancias del mundo real. El tamaño promedio de los árboles (en términos de la cantidad de nodos) para cuatro instancias diferentes de análisis de fallas de circuito SSA fue de varios miles para DPLL, mientras que siempre fue inferior a 200 para UCTSAT.


[1] Previti, Alessandro, Raghuram Ramanujan, Marco Schaerf y Bart Selman. "La búsqueda de UCT estilo Montecarlo para la satisfacción booleana". En AI * IA 2011: Inteligencia artificial alrededor del hombre y más allá, pp. 177-188. Springer Berlin Heidelberg, 2011.

Juho
fuente
-4

DPLL no especifica estrictamente el orden de visitas variables y hay mucha investigación interesante que analiza estrategias óptimas de ataque de orden variable. parte de esto se incorpora a la lógica de selección variable en los algoritmos SAT. en cierto sentido, parte de esta investigación es preliminar, ya que muestra que diferentes órdenes de ataque variable conducen a una restricción secuencial diferente (que está altamente correlacionada con la dureza de la instancia), y el diseño de las heurísticas o estrategias más efectivas para explotar esta visión aparentemente clave parece ser en las primeras etapas de la investigación.

vzn
fuente
44
¿Entiendes que he pedido algoritmos no basados ​​en DPLL ?
Anónimo el
2
¿Entiendes lo que significa "basado" ? Te dije : ¡no uses mis preguntas para comentar sobre lo que quieras comentar!
Anónimo el
77
usted mismo dice que están basados ​​en DPLL. para mí parece que esto es como decir que diferentes reglas de pivote para simplex le dan un algoritmo que no es un algoritmo simplex
Sasho Nikolov
77
Estoy de acuerdo con Sasho. Además, la investigación sobre la heurística de pedidos variables definitivamente no se encuentra en las primeras etapas. La importancia se ha dado cuenta hace mucho tiempo (imagine las consecuencias de un oráculo perfecto), y se ha dedicado mucho tiempo a analizarlas. Las heurísticas de los pedidos de valor se vuelven más interesantes en los solucionadores de CSP, y por alguna razón, no creo que la investigación sobre ellos haya sido tan próspera como para el pedido variable.
Juho
44
Para ser más específicos, la investigación inicial sobre la heurística de pedidos variables se remonta a los años 70. Si está interesado, puedo desenterrar las referencias relevantes para usted.
Juho