W tej sekcji pokazujemy, jak tworzyć plany za pomocą logicznego wnioskowania. Podstawowa idea jest bardzo prosta:
- Skonstruuj zdanie, które zawiera
- Init0 , kolekcja twierdzeń o stanie początkowym;
- Transition1 … Transitiont , aksjomaty stanu następcy dla wszystkich możliwych działań w każdym czasie do pewnego maksymalnego czasu t;
- twierdzenie, że cel został osiągnięty w czasie t : HaeGoldt Λ ClimbeOutt
- Przedstaw całe zdanie osobie rozwiązującej SAT. Jeśli solver znajdzie satysfakcjonujący model, cel jest osiągalny; jeśli zdanie jest niezadowalające, problem jest nie do rozwiązania.
- Zakładając, że model został znaleziony, wyodrębnij z modelu te zmienne, które reprezentują działania i są przypisane true. Razem reprezentują plan osiągnięcia celów.
Procedura planowania propozycji, SATPLAN, jest pokazana na rysunku . Realizuje podstawową ideę właśnie podaną, z jednym zwrotem akcji. Ponieważ agent nie wie, ile kroków musi wykonać, aby osiągnąć cel, algorytm próbuje każdą możliwą liczbę kroków t, aż do pewnej maksymalnej możliwej długości planu Tmax. W ten sposób gwarantuje się znalezienie najkrótszego planu, jeśli taki istnieje. Ze względu na sposób, w jaki SATPLAN szuka rozwiązania, to podejście nie może być stosowane w częściowo obserwowalnym środowisku; SATPLAN po prostu ustawi nieobserwowalne zmienne na wartości potrzebne do stworzenia rozwiązania.
Kluczowym krokiem w korzystaniu z SATPLAN jest budowa bazy wiedzy. Mogłoby się wydawać, po przypadkowym przyjrzeniu się, że aksjomaty świata wumpus w Sekcji 7.7.1 wystarczą dla kroków 1(a) i 1(b) powyżej. Istnieje jednak znacząca różnica między wymaganiami dotyczącymi pociągania (testowane przez ASK) a wymaganiami spełnialności. Rozważmy na przykład lokalizację agenta, początkowo [1,1] i załóżmy, że mało ambitnym celem agenta jest bycie w [2,1] w czasie 1. Początkowa baza wiedzy zawiera L01,1, a celem jest L12,1 . Używając ASK, możemy udowodnić L12,1, czy Forward0 jest potwierdzony, i, co uspokaja, nie możemy udowodnić L1,2,1, jeśli, powiedzmy, Shoot0 jest potwierdzony zamiast tego. Teraz SATPLAN znajdzie plan [Forward0]; jak na razie dobrze. Niestety SATPLAN również znajduje plan [Shoot0]. Jak to możliwe? Aby się tego dowiedzieć, sprawdzamy model, który konstruuje SATPLAN: zawiera on przypisanie L02,1 , czyli agent może być w [2,1] w czasie 1, będąc tam w czasie 0 i strzelając. Ktoś mógłby zapytać: „Czy nie mówiliśmy, że agent jest w [1,1] w czasie 0?” Tak, zrobiliśmy, ale nie powiedzieliśmy agentowi, że nie może być w dwócha miejsca na raz! Bo implikacja L02,1jest nieznana i dlatego nie może być użyta w dowodzie; z drugiej strony spełnialność L02,1 jest nieznana i dlatego może być ustawiona na dowolną wartość, która pomaga w urzeczywistnieniu celu. SATPLAN jest dobrym narzędziem do debugowania baz wiedzy, ponieważ ujawnia miejsca, w których brakuje wiedzy. W tym konkretnym przypadku możemy naprawić bazę wiedzy, stwierdzając, że na każdym kroku czasu agent znajduje się dokładnie w jednym miejscu, używając zbioru zdań podobnych do tych, które są używane do stwierdzenia istnienia dokładnie jednego wumpusa. Alternatywnie możemy potwierdzić ¬L02,1dla wszystkich lokalizacji innych niż [1,1]; aksjomat stanu następcy dla lokalizacji zajmuje się kolejnymi krokami czasowymi. Te same poprawki działają również w celu upewnienia się, że agent ma jedną i tylko jedną orientację na raz. SATPLAN ma jednak w zanadrzu więcej niespodzianek. Po pierwsze, znajduje modele z niemożliwymi akcjami, takimi jak strzelanie bez strzały. Aby zrozumieć dlaczego, musimy dokładniej przyjrzeć się temu, co aksjomaty stanów następczych (takie jak Równanie (7.3) ) mówią o działaniach, których warunki wstępne nie są spełnione. Aksjomaty właściwie przewidują, że nic się nie stanie, gdy taka akcja zostanie wykonana, ale nie mówią, że akcja nie może być wykonana! Aby uniknąć generowania planów z niedozwolonymi akcjami, musimy dodać aksjomaty warunków wstępnych Aksjomaty warunków wstępnych stwierdzające, że wystąpienie akcji wymaga spełnienia warunków wstępnych. , że
Gwarantuje to, że jeśli plan w dowolnym momencie wybierze akcję Strzelaj, agent musi mieć w tym czasie strzałkę. Drugą niespodzianką SATPLAN jest tworzenie planów z wieloma jednoczesnymi działaniami. Na przykład może wymyślić model, w którym oba Forward0 i Shoot0 są prawdziwe, co jest niedozwolone. Aby wyeliminować ten problem, wprowadzamy aksjomaty wykluczenia akcji: dla każdej pary akcji Ati i Atj dodajemy aksjomat
Można zauważyć, że chodzenie do przodu i strzelanie w tym samym czasie nie jest takie trudne, podczas gdy, powiedzmy, jednoczesne strzelanie i chwytanie jest raczej niepraktyczne. Nakładając aksjomaty wykluczenia działań tylko na pary działań, które naprawdę wzajemnie ze sobą kolidują, możemy zezwolić na plany obejmujące wiele jednoczesnych działań – a ponieważ SATPLAN znajduje najkrótszy plan prawny, możemy być pewni, że skorzysta z tej możliwości . Podsumowując, SATPLAN znajduje modele dla zdania zawierającego stan początkowy, cel, aksjomaty stanu następcy, aksjomaty warunków wstępnych i aksjomaty wykluczenia działania. Można wykazać, że ten zbiór aksjomatów jest wystarczający w tym sensie, że nie ma już żadnych fałszywych „rozwiązań”. Każdy model spełniający zdanie zdaniowe będzie poprawnym planem dla pierwotnego problemu. Nowoczesna technologia rozwiązywania SAT sprawia, że podejście jest całkiem praktyczne. Na przykład solver w stylu DPLL nie ma trudności z wygenerowaniem rozwiązania dla instancji wumpus world.
W tej sekcji opisano deklaratywne podejście do konstrukcji agenta: agent działa poprzez połączenie asercji zdań w bazie wiedzy i wnioskowania logicznego. To podejście ma pewne słabości ukryte w wyrażeniach, takich jak „za każdy czas” i „dla każdego kwadratu [x,y] ”. Dla każdego praktycznego agenta te frazy muszą być zaimplementowane przez kod, który automatycznie generuje instancje ogólnego schematu zdań w celu wstawienia do bazy wiedzy. W wumpusowym świecie o rozsądnych rozmiarach — porównywalnym z niewielką grą komputerową — możemy potrzebować planszy 100 x 100 i 1000 kroków czasowych, prowadzących do baz wiedzy z dziesiątkami lub setkami milionów zdań. Nie tylko staje się to raczej niepraktyczne, ale także ilustruje głębszy problem: wiemy coś o świecie wumpusów – mianowicie, że „fizyka” działa w ten sam sposób we wszystkich kwadratach i krokach czasowych – czego nie możemy wyrazić bezpośrednio w język logiki zdań. Aby rozwiązać ten problem, potrzebujemy bardziej wyrazistego języka, w którym wyrażenia typu „za każdy czas” i „za każdy kwadrat [x,y]” można zapisać w naturalny sposób. Takim językiem jest logika pierwszego rzędu, opisana w rozdziale 8; W logice pierwszego rzędu świat Wumpusa o dowolnej wielkości i czasie trwania można opisać za pomocą około dziesięciu zdań logicznych, a nie dziesięciu milionów czy dziesięciu bilionów.