Na ciência da computação, GSAT e WalkSat são algoritmos de busca local para resolver Problemas de Satisfatibilidade Booleana.
Ambos os algoritmos trabalham com fórmulas da lógica booleana que estão na, ou foram convertidas para a, forma normal conjuntiva. Começa-se pela atribuição de um valor aleatório para cada variável na fórmula. Se a atribuição satisfaz todas as cláusulas, o algoritmo termina, retornando a atribuição. Caso contrário, uma variável é substituída e repete-se o passo anterior até que todas as cláusulas sejam satisfeitas. WalkSAT e GSAT diferem-se nos métodos utilizados para selecionar quais variáveis serão substituidas.
GSAT faz mudanças nas variáveis buscando minimizar o número de cláusulas não satisfeitas com a nova atribuição, ou escolhe aleatoriamente uma variável com alguma probabilidade.
WalkSAT escolhe uma cláusula que não está sendo satisfeita pela atribuição atual e então substitui uma variável dentro dessa cláusula. A cláusula é escolhida aleatoriamente entre as cláusulas não satisfeitas. A variável escolhida, tornará não satisfeitas o menor número de cláusulas anteriormente satisfeitas. Essa variável também é escolhida de forma aleatória, com alguma probabilidade. Quando se escolhe de forma aleatória, WalkSAT garante pelo menos uma chance de fixar uma atribuição atualmente incorreta dentro do número de variáveis na cláusula. Ao escolher uma variavel ideal de forma aleatória, WalkSAT irá fazer menos cálculos do que GSAT pois considerará uma quantidade menor de possibilidades.
O algoritmo poderá reiniciar com uma nova atribuição aleatória se não for encontrada uma solução por muito tempo. Essa é uma forma de escapar dos mínimos locais das cláusulas não satisfeitas.
Existem muitas versões da GSAT e WalkSAT. WalkSAT se mostrou particularmente útil na resolução de problemas de satisfabilidade produzidos pela conversão dos problemas de planejamento automatizado. A abordagem para o planejamento que converte problemas de planejamento em problemas de satisfatibilidade booleana é chamado satplan.
MaxWalkSat é uma variante do WalkSAT projetado para resolver o problema de satisfatibilidade ponderada, em que para cada cláusula tem um peso associado, e o objetivo é encontrar uma atribuição—uma que pode ou não satisfazer toda a fórmula—a qual maximizará o peso total das cláusulas satisfeitas por essa atribuição.
Referências
- Henry Kautz e B. Selman (1996). Pushing the envelope: planning, propositional logic, and stochastic search. Em Actas da Xiii Conferência Nacional de Inteligência Artificial (AAAI'96), páginas 1194-1201.
- Papadimitriou, Christos H. (1991), «On selecting a satisfying truth assignment», Proceedings of the 32nd Annual Symposium on Foundations of Computer Science, pp. 163–169, doi:10.1109/SFCS.1991.185365 .
- Schoning, U. (1999), «A probabilistic algorithm for k-SAT and constraint satisfaction problems», Proceedings of 40th Annual Symposium on Foundations of Computer Science, pp. 410–414, doi:10.1109/SFFCS.1999.814612 .
- B. Selman e Henry Kautz (1993). Domain-Independent Extension to GSAT: Solving Large Structured Satisfiability Problems. Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence (IJCAI'93), pp. 290-295.
- Bart Selman, Henry Kautz, e Bram Cohen."Local Search Strategies for Satisfiability Testing." Versão Final apresentada em Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge, 11-13 de outubro de 1993. David S. Johnson e Michael A. Trick, ed. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 26, AMS, 1996.
- B. Selman, H. Levesque, e D. Mitchell (1992). A new method for solving hard satisfiability problems. No Proceedings of the Tenth National Conference on Artificial Intelligence, páginas 440-446.
Ligações externas
