WalkSAT
Inom datavetenskap är GSAT och WalkSAT lokala sökalgoritmer för att lösa booleska tillfredsställelseproblem .
Båda algoritmerna fungerar på formler i boolesk logik som är i eller har omvandlats till konjunktiv normalform . De börjar med att tilldela ett slumpmässigt värde till varje variabel i formeln. Om tilldelningen uppfyller alla klausuler avslutas algoritmen och returnerar tilldelningen. Annars vänds en variabel och ovanstående upprepas sedan tills alla satser är uppfyllda. WalkSAT och GSAT skiljer sig åt i metoderna som används för att välja vilken variabel som ska vändas.
- GSAT gör ändringen som minimerar antalet otillfredsställda klausuler i den nya tilldelningen, eller med viss sannolikhet väljer en variabel slumpmässigt.
- WalkSAT väljer först en sats som inte är uppfylld av den aktuella tilldelningen och vänder sedan en variabel inom den satsen. Klausulen väljs slumpmässigt bland otillfredsställda satser. Variabeln väljs som kommer att resultera i att de minsta tidigare uppfyllda klausulerna blir otillfredsställda, med viss sannolikhet att välja en av variablerna slumpmässigt. När man plockar slumpmässigt garanteras WalkSAT minst en chans på en av antalet variabler i klausulen för att fixa en för närvarande felaktig tilldelning. När man väljer en gissad variabel, måste WalkSAT göra mindre beräkningar än GSAT eftersom den överväger färre möjligheter.
Båda algoritmerna kan starta om med en ny slumpmässig tilldelning om ingen lösning har hittats för länge, som ett sätt att komma ur lokala minima av antal otillfredsställda satser.
Det finns många versioner av GSAT och WalkSAT. WalkSAT har visat sig vara särskilt användbar för att lösa tillfredsställelseproblem som skapas av konvertering från automatiserade planeringsproblem . Tillvägagångssättet för planering som omvandlar planeringsproblem till booleska tillfredsställelsesproblem kallas satplan .
MaxWalkSAT är en variant av WalkSAT designad för att lösa det viktade tillfredsställbarhetsproblemet , där varje klausul har associerats med en vikt, och målet är att hitta en uppgift – en som kanske eller kanske inte uppfyller hela formeln – som maximerar den totala vikten av de klausuler som det uppdraget uppfyller.
- Henry Kautz och B. Selman (1996). Pushing the enveloppe: planering, propositionell logik och stokastisk sökning . I Proceedings of the Thirteenth National Conference on Artificiell Intelligens (AAAI'96), sidorna 1194–1201.
- Papadimitriou, Christos H. (1991), "On selecting a satisfying truth assignment", Proceedings of the 32nd Annual Symposium on Foundations of Computer Science , s. 163–169, doi : 10.1109 /SFCS.1991.185365 818 ISBN 816 816 -2445-2 .
- Schöning, U. ( 1999), "A probabilistic algorithm for k -SAT and constraint satisfaction problems", Proceedings of 40th Annual Symposium on Foundations of Computer Science , s. 410–414, CiteSeerX 10.1.1.132.6306 , doi . SFFCS.1999.814612 , ISBN 978-0-7695-0409-4 .
- B. Selman och Henry Kautz (1993). Domänoberoende tillägg till GSAT: Lösning av stora strukturerade tillfredsställelseproblem . I Proceedings of the Thirteenth International Joint Conference on Artificiell Intelligens (IJCAI'93), sidorna 290–295.
- Bart Selman , Henry Kautz och Bram Cohen . "Lokala sökstrategier för tillfredsställelsetestning." Den slutliga versionen visas i Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge, 11–13 oktober 1993. David S. Johnson och Michael A. Trick , red. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 26, AMS, 1996.
- B. Selman, H. Levesque och D. Mitchell (1992). En ny metod för att lösa svåra tillfredsställbarhetsproblem . I Proceedings of the Tenth National Conference on Artificiell Intelligens (AAAI'92), sidorna 440–446.