WalkSAT
W informatyce GSAT i WalkSAT to lokalne algorytmy wyszukiwania do rozwiązywania logicznych problemów spełnialności .
Oba algorytmy działają na formułach w logice boolowskiej , które są w koniunkcyjnej postaci normalnej lub zostały do niej przekształcone . Rozpoczynają od przypisania losowej wartości każdej zmiennej w formule. Jeśli przypisanie spełnia wszystkie warunki , algorytm kończy działanie, zwracając przypisanie. W przeciwnym razie zmienna jest odwracana, a powyższe jest następnie powtarzane, aż wszystkie klauzule zostaną spełnione. WalkSAT i GSAT różnią się metodami wyboru zmiennej do odwrócenia.
- GSAT dokonuje zmiany, która minimalizuje liczbę klauzul niespełnionych w nowym przydziale lub z pewnym prawdopodobieństwem wybiera zmienną losowo.
- WalkSAT najpierw wybiera klauzulę, która nie jest spełniona przez bieżące przypisanie, a następnie odwraca zmienną w tej klauzuli. Klauzula jest wybierana losowo spośród klauzul niespełnionych. Wybierana jest zmienna, która spowoduje, że najmniej spełnionych wcześniej klauzul stanie się niespełnionymi, z pewnym prawdopodobieństwem losowego wybrania jednej ze zmiennych. Podczas wybierania losowego WalkSAT ma zagwarantowaną przynajmniej jedną szansę z liczby zmiennych w klauzuli naprawienia aktualnie błędnego przypisania. Wybierając zmienną, która ma być optymalna, WalkSAT musi wykonać mniej obliczeń niż GSAT, ponieważ bierze pod uwagę mniej możliwości.
Oba algorytmy mogą ponownie uruchomić się z nowym losowym przypisaniem, jeśli żadne rozwiązanie nie zostało znalezione przez zbyt długi czas, jako sposób na wyjście z lokalnych minimów liczby klauzul niespełnionych.
Istnieje wiele wersji GSAT i WalkSAT. WalkSAT okazał się szczególnie przydatny w rozwiązywaniu problemów spełnialności powstałych w wyniku konwersji z problemów z automatycznym planowaniem . Podejście do planowania, które przekształca problemy planowania w boolowskie problemy spełnialności, nazywa się satplan .
MaxWalkSAT jest wariantem WalkSAT przeznaczonym do rozwiązywania problemu spełnialności ważonej , w którym każda klauzula jest powiązana z wagą, a celem jest znalezienie zadania — takiego, które może, ale nie musi, spełniać całą formułę — które maksymalizuje całkowitą wagę klauzule spełnione przez tę cesję.
- Henry Kautz i B. Selman (1996). Przesuwanie koperty: planowanie, logika zdań i wyszukiwanie stochastyczne . W Proceedings of the XIII National Conference on Artificial Intelligence (AAAI'96) , strony 1194–1201.
- Papadimitriou, Christos H. (1991), „O wyborze satysfakcjonującego zadania prawdy”, Proceedings of the 32. Annual Symposium on Foundations of Computer Science , s. 163–169, doi : 10.1109 / SFCS.1991.185365 , ISBN 978-0-8186 -2445-2 .
- Schöning, U. (1999), „Algorytm probabilistyczny dla k -SAT i problemów z spełnianiem ograniczeń”, Proceedings of 40th Annual Symposium on Foundations of Computer Science , s. 410–414, CiteSeerX 10.1.1.132.6306 , doi : 10.1109/ SFFCS.1999.814612 , ISBN 978-0-7695-0409-4 .
- B. Selman i Henry Kautz (1993). Niezależne od domeny rozszerzenie GSAT: rozwiązywanie problemów z dużą strukturą spełnialności . W Proceedings of the trzynasta międzynarodowa wspólna konferencja na temat sztucznej inteligencji (IJCAI'93) , strony 290–295.
- Bart Selman , Henry Kautz i Bram Cohen . „Lokalne strategie wyszukiwania do testowania satysfakcji”. Ostateczna wersja pojawia się w Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge, 11–13 października 1993. David S. Johnson i Michael A. Trick , wyd. Seria DIMACS w matematyce dyskretnej i informatyce teoretycznej, tom. 26, AMS, 1996.
- B. Selman, H. Levesque i D. Mitchell (1992). Nowa metoda rozwiązywania trudnych problemów spełnialności . W Proceedings of the X National Conference on Artificial Intelligence (AAAI'92) , strony 440–446.