En ciencias de la computación , GSAT y WalkSAT son algoritmos de búsqueda local para resolver problemas de satisfacibilidad booleanos .
Ambos algoritmos funcionan con fórmulas en lógica booleana que están o se han convertido en forma normal conjuntiva . Comienzan asignando un valor aleatorio a cada variable en la fórmula. Si la asignación satisface todas las cláusulas , el algoritmo termina y devuelve la asignación. De lo contrario, se invierte una variable y luego se repite lo anterior hasta que se cumplan todas las cláusulas. WalkSAT y GSAT difieren en los métodos utilizados para seleccionar qué variable voltear.
GSAT realiza el cambio que minimiza el número de cláusulas insatisfechas en la nueva asignación o, con cierta probabilidad, elige una variable al azar.
WalkSAT primero elige una cláusula que no está satisfecha con la asignación actual, luego cambia una variable dentro de esa cláusula. La cláusula se elige al azar entre las cláusulas insatisfechas. Se elige la variable que dará como resultado que la menor cantidad de cláusulas previamente satisfechas queden insatisfechas, con alguna probabilidad de elegir una de las variables al azar. Al seleccionar al azar, WalkSAT tiene garantizada al menos una posibilidad de una de las variables en la cláusula de corregir una asignación actualmente incorrecta. Al elegir una variable supuestamente óptima, WalkSAT tiene que hacer menos cálculos que GSAT porque está considerando menos posibilidades.
El algoritmo puede reiniciarse con una nueva asignación aleatoria si no se ha encontrado una solución durante demasiado tiempo, como una forma de salir de los mínimos locales de números de cláusulas insatisfechas.
Existen muchas versiones de GSAT y WalkSAT. WalkSAT ha demostrado ser particularmente útil para resolver problemas de satisfacción producidos por la conversión de problemas de planificación automatizados . El enfoque de planificación que convierte los problemas de planificación en problemas de satisfacibilidad booleanos se llama satplan .
MaxWalkSAT es una variante de WalkSAT diseñada para resolver el problema de satisfacibilidad ponderado , en el que cada cláusula se ha asociado con un peso, y el objetivo es encontrar una asignación, una que pueda o no satisfacer la fórmula completa, que maximice el peso total de las cláusulas satisfechas por esa cesión.
Referencias
- Henry Kautz y B. Selman (1996). Ir más allá: 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 , págs. 163-169, doi : 10.1109 / SFCS.1991.185365 , ISBN 978-0-8186-2445-2.
- Schöning, U. (1999), "Un algoritmo probabilístico para k -SAT y problemas de satisfacción de restricciones", Actas del 40º Simposio Anual sobre Fundamentos de la Ciencia de la Computación , págs. 410–414, CiteSeerX 10.1.1.132.6306 , doi : 10.1109 / SFFCS.1999.814612 , ISBN 978-0-7695-0409-4.
- B. Selman y Henry Kautz (1993). Extensión independiente de dominio a GSAT: solución de grandes problemas de satisfacción estructurada . En Actas de la Decimotercera Conferencia Conjunta Internacional sobre Inteligencia Artificial (IJCAI'93) , páginas 290–295.
- Bart Selman , Henry Kautz y Bram Cohen . "Estrategias de búsqueda local para pruebas de satisfacción". La versión final aparece en Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge, del 11 al 13 de octubre de 1993. David S. Johnson y Michael A. Trick , eds. Serie DIMACS en Matemáticas Discretas e Informática Teórica, vol. 26, AMS, 1996.
- B. Selman, H. Levesque y D. Mitchell (1992). Un nuevo método para resolver problemas difíciles de satisfacción . En Actas de la Décima Conferencia Nacional sobre Inteligencia Artificial (AAAI'92) , páginas 440–446.