¿Hay algún algoritmo para la resolución SAT que no esté basado en DPLL? ¿O todos los algoritmos utilizados por los solucionadores SAT están basados en DPLL?
ds.algorithms
reference-request
sat
Anónimo
fuente
fuente
Respuestas:
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.
fuente
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.
fuente
Hay solucionadores SAT basados en la búsqueda local. Ver, por ejemplo, este artículo para exposición.
fuente
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:
fuente
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.
fuente
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.
Guía para la resolución de SAT en el mundo real con descomposición dinámica del separador de hipergrafía Li, van Beek
Descomponer problemas de satisfacción o Usar gráficos para obtener una mejor idea de los problemas de satisfacción Herwig
La restricción filo de cuchillo (1998) Walsh
fuente