WalkSAT

En informática , GSAT y WalkSAT son algoritmos de búsqueda local para resolver problemas de satisfacibilidad booleana .

Ambos algoritmos trabajan con fórmulas de lógica booleana que están en forma normal conjuntiva o que han sido convertidas a ella . Comienzan asignando un valor aleatorio a cada variable de la fórmula. Si la asignación satisface todas las condiciones , el algoritmo finaliza y devuelve la asignación. De lo contrario, se invierte el valor de una variable y se repite el proceso hasta que se satisfagan todas las condiciones. WalkSAT y GSAT difieren en los métodos que utilizan para seleccionar qué variable invertir.

• GSAT realiza el cambio que minimiza el número de cláusulas insatisfechas en la nueva asignación, o bien elige una variable al azar con cierta probabilidad.
• WalkSAT primero selecciona una cláusula que no se satisface con la asignación actual y luego modifica una variable dentro de esa cláusula. La cláusula se elige al azar entre las cláusulas insatisfechas. Se selecciona la variable que resultará en la menor cantidad de cláusulas previamente satisfechas que pasarán a ser insatisfechas, con cierta probabilidad de elegir una de las variables al azar. Al elegir al azar, WalkSAT tiene garantizada al menos una probabilidad de una entre el número de variables en la cláusula para corregir una asignación actualmente incorrecta. Al elegir una variable que se supone óptima, WalkSAT requiere menos cálculos que GSAT porque considera menos posibilidades.

Ambos algoritmos pueden reiniciarse con una nueva asignación aleatoria si no se ha encontrado ninguna solución durante demasiado tiempo, como forma de salir de los mínimos locales en cuanto al número de cláusulas insatisfechas.

Existen muchas versiones de GSAT y WalkSAT. WalkSAT ha demostrado ser particularmente útil para resolver problemas de satisfacibilidad derivados de la conversión de problemas de planificación automatizada . El método de planificación que convierte problemas de planificación en problemas de satisfacibilidad booleana se denomina satplan .

MaxWalkSAT es una variante de WalkSAT diseñada para resolver el problema de satisfacibilidad ponderada , en el que cada cláusula tiene asociado un peso, y el objetivo es encontrar una asignación —que puede o no satisfacer la fórmula completa— que maximice el peso total de las cláusulas satisfechas por esa asignación.

• Henry Kautz y B. Selman (1996). Superando los límites: planificación, lógica proposicional y búsqueda estocástica . En Actas de la Decimotercera Conferencia Nacional sobre Inteligencia Artificial (AAAI'96) , páginas 1194–1201.
• Papadimitriou, Christos H. (1991), "Sobre la selección de una asignación de verdad satisfactoria", Actas del 32.º Simposio Anual sobre Fundamentos de la Informática , pp. 163–169 , doi : 10.1109/SFCS.1991.185365 , ISBN  978-0-8186-2445-2, S2CID 206559488 .
• Schöning, U. (1999), "Un algoritmo probabilístico para problemas de satisfacción de restricciones y k -SAT", Actas del 40.º Simposio Anual sobre Fundamentos de la Informática , pp. 410–414 , CiteSeerX 10.1.1.132.6306 , doi : 10.1109/SFFCS.1999.814612 , ISBN   978-0-7695-0409-4, S2CID 1230959 .
• B. Selman y Henry Kautz (1993). Extensión independiente del dominio para GSAT: resolución de grandes problemas de satisfacibilidad estructurada . En Actas de la Decimotercera Conferencia Internacional Conjunta sobre Inteligencia Artificial (IJCAI'93) , páginas 290–295.
• Bart Selman , Henry Kautz y Bram Cohen . «Estrategias de búsqueda local para pruebas de satisfacibilidad». La versión final aparece en Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge, 11-13 de octubre de 1993. David S. Johnson y Michael A. Trick , eds. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 26, AMS, 1996.
• B. Selman, H. Levesque y D. Mitchell (1992). Un nuevo método para resolver problemas de satisfacibilidad difíciles . En Actas de la Décima Conferencia Nacional sobre Inteligencia Artificial (AAAI'92) , páginas 440–446.

• Página principal de WalkSAT