Miesiąc: listopad 2021

Jak stwierdzono na początku rozdziału, agent logiczny działa poprzez wydedukowanie, co należy zrobić z bazy wiedzy zdań o świecie. Baza wiedzy składa się z aksjomatów – ogólnej wiedzy o tym, jak działa świat – i zdań percepcyjnych uzyskanych z doświadczenia agenta w określonym świecie. W tej części skupimy się na problemie wydedukowania obecnego stanu świata wumpusów – gdzie jestem, czy ten kwadrat jest bezpieczny i tak dalej. Agent wie, że na polu startowym nie ma dołu (¬P_1,1) ani wumpusa (¬W_1,1 ). Co więcej, dla każdego kwadratu wie, że jest przewiewny wtedy i tylko wtedy, gdy sąsiedni kwadrat ma dół; a kwadrat jest śmierdzący wtedy i tylko wtedy, gdy sąsiedni kwadrat ma wumpusa. W związku z tym zawieramy duży zbiór zdań o następującej postaci:

Agent wie też, że jest dokładnie jeden wumpus. Wyraża się to w dwóch częściach. Po pierwsze, musimy powiedzieć, że istnieje co najmniej jeden wumpus:

Następnie musimy powiedzieć, że jest co najwyżej jeden wumpus. Dla każdej pary lokacji dodajemy zdanie mówiące, że przynajmniej jedna z nich musi być wolna od wumpusa:

Jak na razie dobrze. Rozważmy teraz spostrzeżenia agenta. Używamy tego S_1,1 , aby powiedzieć, że w [1,1] jest smród; czy możemy użyć jednej propozycji, Stnech aby oznaczać, że agent wyczuwa smród? Niestety nie możemy: gdyby nie było smrodu w poprzednim kroku czasowym, to byłoby ¬Stench już stwierdzone, a nowe stwierdzenie spowodowałoby po prostu sprzeczność. Problem zostaje rozwiązany, gdy zdamy sobie sprawę, że percepcja stwierdza coś tylko o aktualnym czasie. Tak więc, jeśli krok czasowy wynosi 4, wtedy dodajemy  Stench do bazy wiedzy, a nie Strench – starannie unikając wszelkich sprzeczności z . To samo dotyczy percepcji wiatru, uderzenia, blasku i krzyku. Pomysł kojarzenia zdań z krokami czasowymi rozciąga się na każdy aspekt świata, który zmienia się w czasie. Na przykład początkowa baza wiedzy obejmuje  L⁰_1,1 –  agent jest w kwadracie [1,1] w czasie 0 – oraz  Facingeast⁰, HaveArrow⁰ , i WumpusAlive⁰ . Używamy rzeczownika fluent (z łac. fluens), aby odnieść się do zmieniającego się aspektu świata. „Płynna” jest synonimem „zmiennej stanu” w znaczeniu opisanym w omówieniu reprezentacji podzielonych na czynniki w Sekcji 2.4.7 na stronie 58. Symbole związane ze stałymi aspektami świata nie wymagają indeksu górnego czasu i są czasami nazywane atemporalnymi. zmienne. Możemy połączyć postrzeganie smrodu i wiatru bezpośrednio z właściwościami kwadratów, w których są one doświadczane w następujący sposób. Dla dowolnego kroku czasowego i dowolnego kwadratu [x,y] zapewniamy:

Teraz oczywiście potrzebujemy aksjomatów, które pozwolą agentowi śledzić biegle, takie jak L^t_x,y . Te biegłości zmieniają się w wyniku działań podejmowanych przez agenta, więc w terminologii rozdziału 3 musimy zapisać model przejściowy świata wumpus jako zbiór zdań logicznych. Najpierw potrzebujemy symboli propozycji dla wystąpień akcji. Podobnie jak w przypadku perceptów, te symbole są indeksowane według czasu; zatem Forward0 oznacza to, że agent wykonuje akcję Forward w czasie 0. Zgodnie z konwencją, percept dla danego kroku czasowego ma miejsce jako pierwszy, po nim następuje akcja dla tego kroku czasowego, a następnie następuje przejście do następnego kroku czasowego. Aby opisać, jak zmienia się świat, możemy spróbować napisać aksjomaty efektów, które określają wynik działania w następnym kroku czasowym. Na przykład, jeśli agent znajduje się w lokalizacji [1,1] zwrócony na wschód w czasie 0 i porusza się do przodu, wynikiem jest to, że agent znajduje się w kwadracie [2,1] i nie znajduje się już w t :

Potrzebowalibyśmy jednego takiego zdania dla każdego możliwego kroku czasowego, dla każdego z 16 kwadratów i każdej z czterech orientacji. Potrzebowalibyśmy również podobnych zdań dla innych akcji: Chwyć, Strzelaj, Wspinaj się, Skręć w lewo i Skręć w prawo. Załóżmy, że agent decyduje się ruszyć Naprzód w czasie 0 i potwierdza ten fakt w swojej bazie wiedzy. Mając aksjomat efektu w połączeniu z początkowymi twierdzeniami o stanie w czasie 0, agent może teraz wywnioskować, że jest w [2,1]. To jest,  ASK(KB,L¹_,2,1) = true . Jak na razie dobrze. Niestety, jeśli my ASK(KB,HaveArrow¹), odpowiedź jest fałszywa, to znaczy agent nie może udowodnić, że nadal ma strzałę; ani nie może udowodnić, że jej nie ma! Informacja została utracona, ponieważ aksjomat efektu nie określa tego, co pozostaje niezmienione w wyniku działania. Konieczność zrobienia tego powoduje powstanie problemu z ramą. Jednym z możliwych rozwiązań problemu ramy byłoby dodanie aksjomatów ramy, wyraźnie potwierdzających wszystkie zdania, które pozostają takie same.Na przykład za każdym razem mielibyśmy miejsce, w którym wyraźnie wymienimy każde zdanie, które pozostaje niezmienione od czasu t do czasu t+1 w ramach akcji Naprzód. Chociaż agent teraz wie, że nadal ma strzałę po przejściu do przodu i że wumpus nie umarł ani nie wrócił do życia, mnożenie aksjomatów ramowych wydaje się wyjątkowo nieefektywne. W świecie o m różnych działaniach i n biegach, zbiór aksjomatów ramy będzie miał rozmiar O(m,n). Ta konkretna manifestacja problemu ramek jest czasami nazywana problemem ram reprezentacyjnych. Problem odegrał znaczącą rolę w historii sztucznej inteligencji; omówimy to dalej w uwagach na końcu.

Problem ram reprezentacyjnych jest o tyle istotny, że świat rzeczywisty ma bardzo wiele biegłości, delikatnie mówiąc. Na szczęście dla nas, ludzi, każde działanie zwykle zmienia nie więcej niż niewielka liczba k tych płynnych ruchów – świat wykazuje lokalność. Rozwiązanie problemu ramy reprezentacyjnej wymaga zdefiniowania modelu przejścia za pomocą zestawu aksjomatów rozmiaru O(m,k) , a nie rozmiaru O(m,n). Istnieje również problem z ramą inferencyjną: problem przewidywania w czasie wyników t-krokowego planu działania w czasie O(kt), a nie O(n,t)

Rozwiązanie problemu polega na zmianie skupienia z pisania aksjomatów o działaniach na pisanie aksjomatów o biegłościach. Tak więc dla każdego płynnego F , będziemy mieli aksjomat, który definiuje wartość logiczną prawda  F^t+1 w kategoriach płynnych (w tym samo F) w czasie t i działań, które mogły mieć miejsce w czasie t . Teraz wartość prawdziwości F^t+1 można ustawić na jeden z dwóch sposobów: albo działanie w czasie t powoduje, że F jest prawdziwe w t+1 , albo F było już prawdziwe w czasie t i działanie w czasie t nie powoduje, że jest fałszywe. Aksjomat o tej postaci nazywa się aksjomatem następcy stanu i ma postać:

Jednym z najprostszych aksjomatów stanu następcy jest ten dla HaveArrow. Ponieważ nie ma akcji przeładowania, część ActionCausesF^t znika i zostajemy z

W przypadku lokalizacji agenta aksjomaty stanów następczych są bardziej rozbudowane. Na przykład, L^t+1_1,1jest prawdą, jeśli: (a) agent przesunął się do przodu z [1,2], gdy jest skierowany na południe, lub z [2,1], gdy jest skierowany na zachód; lub (b) L^t_1,1 było już prawdziwe, a akcja nie spowodowała ruchu (albo dlatego, że akcja nie była Naprzód, albo uderzyła w ścianę). Napisane w logice zdań, staje się to

Mając kompletny zestaw aksjomatów stanów następców i innych aksjomatów wymienionych na początku tej sekcji, agent będzie w stanie ZAPYTAĆ i odpowiedzieć na wszelkie pytania dotyczące aktualnego stanu świata. Na przykład początkowa sekwencja percepcji i działań to:

W tym momencie mamy  ASK(KB, L⁶_1,2) = true  więc agent wie, gdzie to jest. Ponadto, ASK(KB, W_1,3) = true i  ASK(KB, P ₃,_1,) = true, więc agent znalazł wumpusa i jeden z dołów. Najważniejszym pytaniem dla agenta jest to, czy kwadrat jest w porządku, aby przenieś się do – to znaczy, czy kwadrat jest wolny od dołu lub żywego wumpusa. Wygodnie jest dodać do tego aksjomaty, które mają postać

Na koniec ASK(KB, OK⁶_2,2) = true , więc przejście do kwadratu [2,2] jest OK. W rzeczywistości, mając do dyspozycji solidny i kompletny algorytm wnioskowania, taki jak DPLL, agent może odpowiedzieć na każde pytanie, na które można odpowiedzieć, które kwadraty są w porządku – i może to zrobić w ciągu zaledwie kilku milisekund dla małych i średnich światów wumpus. Rozwiązanie problemów z ramami reprezentacyjnymi i inferencyjnymi jest dużym krokiem naprzód, ale zgubny problem pozostaje: musimy potwierdzić, że wszystkie niezbędne warunki wstępne działania są spełnione, aby miało ono zamierzony skutek. Powiedzieliśmy, że akcja Naprzód przesuwa agenta do przodu, chyba że na drodze stoi ściana, ale istnieje wiele innych niezwykłych wyjątków, które mogą spowodować niepowodzenie akcji: agent może się potknąć i upaść, doznać ataku serca, zostać niesionym przez gigantyczne nietoperze itp. Określanie wszystkich tych wyjątków nazywa się problemem kwalifikacji. W logice nie ma kompletnego rozwiązania; projektanci systemów muszą kierować się rozsądkiem przy podejmowaniu decyzji o tym, jak szczegółowe chcą być w określaniu swojego modelu, a jakie szczegóły chcą pominąć. W rozdziale 12 zobaczymy, że teoria prawdopodobieństwa pozwala nam podsumować wszystkie wyjątki bez wyraźnego ich nazywania.

W tej sekcji łączymy to, czego nauczyliśmy się do tej pory, aby skonstruować agentów świata wumpus, które wykorzystują logikę zdań. Pierwszym krokiem jest umożliwienie agentowi wydedukowania, na ile to możliwe, stanu świata, biorąc pod uwagę jego historię percepcji. Wymaga to spisania pełnego logicznego modelu efektów działań. Następnie pokazujemy, jak wnioskowanie logiczne może być użyte przez agenta w świecie wumpusa. Pokazujemy również, jak agent może sprawnie śledzić świat bez wchodzenia w historię percepcji dla każdego wnioskowania. Na koniec pokazujemy, w jaki sposób agent może wykorzystać logiczne wnioskowanie do konstruowania planów, które gwarantują osiągnięcie jego celów, pod warunkiem, że jego baza wiedzy jest prawdziwa w rzeczywistym świecie.

Niektóre problemy z SAT są trudniejsze niż inne. Proste problemy można rozwiązać dowolnym starym algorytmem, ale ponieważ wiemy, że SAT jest NP-zupełny, przynajmniej niektóre instancje problemów muszą wymagać wykładniczego czasu wykonywania. W rozdziale 6 zobaczyliśmy zaskakujące odkrycia dotyczące pewnych rodzajów problemów. Na przykład problem n-królowych – uważany za dość skomplikowany dla algorytmów wyszukiwania z nawrotem – okazał się banalnie łatwy dla lokalnych metod wyszukiwania, takich jak min-konflikty. Dzieje się tak, ponieważ rozwiązania są bardzo gęsto rozmieszczone w przestrzeni przydziałów, a każde początkowe przypisanie gwarantuje, że znajdzie rozwiązanie w pobliżu. Tak więc n-królowe jest łatwe, ponieważ nie jest ograniczone. Kiedy przyjrzymy się problemom spełnialności w spójnej postaci normalnej, problem niedostatecznie ograniczony to taki, w którym stosunkowo niewiele klauzul ogranicza zmienne. Na przykład, oto losowo wygenerowane zdanie 3-CNF z pięcioma symbolami i pięcioma klauzulami:

Szesnaście z 32 możliwych przypisań to modele tego zdania, więc średnio potrzeba tylko dwóch losowych zgadnięć, aby znaleźć model. Jest to łatwy problem spełnialności, podobnie jak większość takich problemów z niepełnym ograniczeniem. Z drugiej strony problem nadmiernie ograniczony ma wiele klauzul odnoszących się do liczby zmiennych i prawdopodobnie nie będzie miał rozwiązań. Nadmiernie ograniczone problemy są często łatwe do rozwiązania, ponieważ ograniczenia szybko prowadzą albo do rozwiązania, albo do ślepego zaułka, z którego nie ma ucieczki. Aby wyjść poza te podstawowe intuicje, musimy dokładnie określić, w jaki sposób generowane są losowe zdania. Notacja  CNF_k(m,n)oznacza zdanie k-CNF z m klauzulami i n symbolami, gdzie klauzule są wybierane jednolicie, niezależnie i bez zamiany spośród wszystkich klauzul z k różnymi literałami, które są losowo dodatnie lub ujemne. (Symbol nie może pojawić się dwa razy w zdaniu, ani zdanie nie może pojawić się dwa razy w zdaniu). Mając źródło losowych zdań, możemy zmierzyć prawdopodobieństwo spełniania. Rysunek (a) przedstawia prawdopodobieństwo wystąpienia CNF₃(m,50) , czyli zdań z 50 zmiennymi i 3 literałami na zdanie, jako funkcję stosunku zdanie/symbol, . Jak się spodziewamy, dla małych m/n prawdopodobieństwo spełniania jest bliskie 1, a dla dużych m/n  jest bliskie 0. Prawdopodobieństwo dość gwałtownie spada wokół m/n = 4.3 . Empirycznie stwierdzamy, że „klif” pozostaje mniej więcej w tym samym miejscu (dla k = 3 ) i staje się coraz ostrzejszy wraz ze wzrostem n.

Teoretycznie hipoteza progu spełnialności mówi, że dla każdego k ≥ 3 , istnieje stosunek progowy r_k taki, że jeśli n dąży do nieskończoności prawdopodobieństwo że  CNF_k(rn,n) jest spełnialne wynosi 1 dla wszystkich wartości poniżej progu i 0 dla wszystkich wartości powyżej. Przypuszczenie pozostaje niesprawdzone, nawet w szczególnych przypadkach, takich jak k = 3 . Niezależnie od tego, czy jest to twierdzenie, czy nie, ten rodzaj progowania jest z pewnością powszechny, w przypadku problemów spełnialności, jak również innych rodzajów problemów NP-trudnych. Teraz, gdy mamy już dobry pomysł, gdzie znajdują się problemy dające się zaspokoić, a gdzie nie, następne pytanie brzmi: gdzie są problemy trudne? Okazuje się, że często są one również na progu. Rysunek (b) pokazuje, że 50-symbolowe problemy przy wartości progowej 4,3 są około 20 razy trudniejsze do rozwiązania niż te o stosunku 3,3. Problemy o ograniczonych ograniczeniach są najłatwiejsze do rozwiązania (ponieważ tak łatwo jest odgadnąć rozwiązanie); problemy z nadmiernymi ograniczeniami nie są tak łatwe, jak problemy z niedoborem ograniczeń, ale nadal są znacznie łatwiejsze niż te tuż przy progu.

Jak dotąd w tej książce widzieliśmy kilka lokalnych algorytmów wyszukiwania, w tym HILL-CLIMBING i SIMULATED-ANNEALING. Algorytmy te można zastosować bezpośrednio do problemów spełnialności, pod warunkiem, że dobierzemy odpowiednią funkcję oceny. Ponieważ celem jest znalezienie przypisania, które spełnia każdą klauzulę, funkcja oceny, która zlicza liczbę niespełnionych klauzul, wykona zadanie. W rzeczywistości jest to dokładnie miara używana przez algorytm MIN-CONFLICTS dla CSP (strona 198). Wszystkie te algorytmy wykonują kroki w przestrzeni pełnych przypisań, odwracając wartość logiczną jednego symbolu na raz. Przestrzeń zawiera zwykle wiele minimów lokalnych, przed którymi trzeba uciec, od których wymagane są różne formy losowości. W ostatnich latach przeprowadzono wiele eksperymentów, aby znaleźć dobrą równowagę między zachłannością a przypadkowością. Jeden z najprostszych i najskuteczniejszych algorytmów, jaki wyłonił się z całej tej pracy, nazywa się WALKSAT.

W każdej iteracji algorytm wybiera klauzulę niespełnioną i wybiera symbol w klauzuli do odwrócenia. Wybiera losowo jeden z dwóch sposobów wyboru symbolu do odwrócenia: (1) krok „min-konfliktów”, który minimalizuje liczbę niespełnionych klauzul w nowym stanie i (2) krok „losowego spaceru”, który losowo wybiera symbol.

Kiedy WALKSAT zwraca model, zdanie wejściowe jest rzeczywiście spełnialne, ale gdy zwraca niepowodzenie, możliwe są dwie przyczyny: albo zdanie jest niespełnialne, albo musimy dać algorytmowi więcej czasu. Jeśli ustawimy max_flips = ∞ i P > 0 , WALKSAT w końcu zwróci model (jeśli taki istnieje), ponieważ kroki błądzenia losowego w końcu dotrą do rozwiązania. Niestety, jeśli max_flips to nieskończoność, a zdanie jest niezadowalające, to algorytm nigdy się nie kończy! Z tego powodu WALKSAT jest najbardziej przydatny, gdy oczekujemy rozwiązania — na przykład problemy omówione w rozdziałach 3 i 6 zwykle mają rozwiązania. Z drugiej strony WALKSAT nie zawsze może wykryć niespełnienie, które jest wymagane do podjęcia decyzji o pociągnięciu. Na przykład agent nie może niezawodnie użyć WALKSAT, aby udowodnić, że kwadrat jest bezpieczny w świecie Wumpusa. Zamiast tego może powiedzieć: „Myślałem o tym przez godzinę i nie mogłem wymyślić możliwego świata, w którym plac nie jest bezpieczny”. To może być dobry wskaźnik empiryczny że plac jest bezpieczny, ale na pewno nie jest to dowód.

Pierwszy rozważany przez nas algorytm jest często nazywany algorytmem Davisa-Putnama, po przełomowej pracy Martina Davisa i Hilary Putnam (1960). Algorytm jest w rzeczywistości wersją opisaną przez Davisa, Logemanna i Lovelanda (1962), więc nazwiemy go DPLL po inicjałach wszystkich czterech autorów. DPLL przyjmuje jako dane wejściowe zdanie w spójnej formie normalnej – zbiór klauzul. Podobnie jak BACKTRACKING-SEARCH i TT-ENTAILS?, jest to zasadniczo rekurencyjne, ukierunkowane na głębię wyliczanie możliwych modeli. Zawiera trzy ulepszenia w stosunku do prostego schematu TT-ENTAILS?:

* WCZEŚNIEJSZE ZAKOŃCZENIE: Algorytm wykrywa, czy zdanie musi być prawdziwe czy fałszywe, nawet przy częściowo wypełnionym modelu. Zdanie jest prawdziwe, jeśli jakikolwiek literał jest prawdziwy, nawet jeśli inne literały nie mają jeszcze wartości prawdziwości; stąd zdanie jako całość można uznać za prawdziwe nawet przed ukończeniem modelu. Na przykład zdanie (A V B) Λ (A V C)  jest prawdziwe, jeśli A jest prawdziwe, niezależnie od wartości  B i C . Podobnie zdanie jest fałszywe, jeśli jakakolwiek klauzula jest fałszywa, co ma miejsce, gdy każdy z jego literałów jest fałszywy. Ponownie, może to nastąpić na długo przed ukończeniem modelu. Wczesne zakończenie pozwala uniknąć badania całych poddrzew w przestrzeni wyszukiwania.

* CZYSTY SYMBOL HEURYSTYCZNY: czysty symbol to symbol, który zawsze pojawia się z tym samym „znakiem” we wszystkich klauzulach. Na przykład w trzech zdaniach (A V ¬B) , (¬B V ¬C) i  (C  V A), symbol A jest czysty, ponieważ pojawia się tylko literał dodatni, B jest czysty, ponieważ pojawia się tylko literał ujemny a C jest nieczysty. Łatwo zauważyć, że jeśli zdanie ma model, to ma model z przypisanymi czystymi symbolami, aby ich literały były prawdziwe, ponieważ takie postępowanie nigdy nie sprawi, że zdanie będzie fałszywe. Należy zauważyć, że przy określaniu czystości symbolu algorytm może zignorować klauzule, o których wiadomo już, że są prawdziwe w dotychczas skonstruowanym modelu. Na przykład, jeśli model zawiera  B  = false , to klauzula (¬B  V ¬ C) jest już prawdziwa, a w pozostałych klauzulach C pojawia się tylko jako literał dodatni; dlatego staje się czysty.

* KLAUZULA JEDNOSTKOWA HEURYSTYCZNA : Klauzula jednostkowa została wcześniej zdefiniowana jako klauzula zawierająca tylko jeden literał. W kontekście DPLL oznacza to również klauzule, w których wszystkie literały oprócz jednego są już przypisane przez model jako fałsz. Na przykład, jeśli model zawiera   B = true, wtedy (¬B ∨ ¬C)  upraszcza się do ¬C  , co jest klauzulą ​​jednostkową. Oczywiście, aby ta klauzula była prawdziwa, C musi być ustawiona na fałsz. Heurystyka klauzuli jednostkowej przypisuje wszystkie takie symbole przed rozgałęzieniem na resztę. Jedną z ważnych konsekwencji heurystyki jest to, że każda próba udowodnienia (poprzez obalanie) dosłowności, która już znajduje się w bazie wiedzy, zakończy się natychmiastowym sukcesem. Zauważ również, że przypisanie jednej klauzuli jednostki może stworzyć inną klauzulę jednostki – na przykład, gdy C jest ustawiona na false, (C ∨ A)  staje się klauzulą ​​jednostki, powodując przypisanie true do A . Ta „kaskada” wymuszonych przydziałów nazywana jest propagacją jednostek. Przypomina proces przekazywania łańcuchów do przodu z klauzulami określonymi, i rzeczywiście, jeśli wyrażenie CNF zawiera tylko określone klauzule, DPLL zasadniczo replikuje łańcuchowanie w przód. Algorytm DPLL daje podstawowy szkielet procesu wyszukiwania bez szczegółów implementacji

To, czego nie widać, to sztuczki, które umożliwiają rozwiązującym SAT skalowanie do dużych problemów. Interesujące jest to, że większość z tych sztuczek jest w rzeczywistości dość ogólna i widzieliśmy je wcześniej pod innymi postaciami:

1. Analiza komponentów (jak widać z Tasmanii w CSP): Ponieważ DPLL przypisuje wartości logiczne do zmiennych, zbiór klauzul może zostać podzielony na rozłączne podzbiory, zwane komponentami, które nie współdzielą nieprzypisanych zmiennych. Biorąc pod uwagę skuteczny sposób wykrywania tego, kiedy to nastąpi, solver może znacznie przyspieszyć, pracując nad każdym komponentem osobno.
2. Kolejność zmiennych i wartości (jak widać w sekcji 6.3.1 dla dostawców CSP): Nasza prosta implementacja protokołu DPLL wykorzystuje arbitralną kolejność zmiennych i zawsze sprawdza wartość prawda przed fałszem. Heurystyka stopni sugeruje wybór zmiennej, która pojawia się najczęściej nad wszystkimi pozostałymi zdaniami.
3. Inteligentne cofanie: Wiele problemów, których nie można rozwiązać w ciągu godzin pracy z chronologicznym cofaniem, można rozwiązać

w ciągu kilku sekund dzięki inteligentnemu śledzeniu wstecznemu, które wykonuje kopię zapasową aż do odpowiedniego punktu konfliktu. Wszystkie solvery SAT, które wykonują inteligentne śledzenie wstecz, wykorzystują jakąś formę uczenia klauzul konfliktu, aby rejestrować konflikty, aby nie powtórzyły się później w wyszukiwaniu. Zwykle utrzymywany jest zestaw konfliktów o ograniczonym rozmiarze, a rzadko używane są usuwane.

4. Losowe restarty (jak widać na stronie 113 dla wspinaczki pod górę): Czasami wydaje się, że bieg nie robi postępów. W takim przypadku możemy zacząć od początku drzewa wyszukiwania, zamiast próbować kontynuować. Po ponownym uruchomieniu dokonywane są różne losowe wybory (w wyborze zmiennej i wartości). Klauzule wyuczone podczas pierwszego uruchomienia są zachowywane po ponownym uruchomieniu i mogą pomóc w oczyszczeniu przestrzeni wyszukiwania. Ponowne uruchomienie nie gwarantuje szybszego znalezienia rozwiązania, ale zmniejsza wariancję czasu do rozwiązania.
5. Sprytne indeksowanie (jak widać w wielu algorytmach): Metody przyspieszające stosowane w samym DPLL, a także triki stosowane w nowoczesnych solwerach, wymagają szybkiego indeksowania takich rzeczy, jak „zbiór klauzul, w których zmienna X_i pojawia się jako dodatni literał ”. Zadanie to komplikuje fakt, że algorytmy są zainteresowane tylko klauzulami, które nie zostały jeszcze spełnione przez poprzednie przypisania do zmiennych, dlatego struktury indeksujące muszą być dynamicznie aktualizowane w miarę postępu obliczeń.

Dzięki tym ulepszeniom współczesne solvery mogą obsługiwać problemy z dziesiątkami milionów zmiennych. Zrewolucjonizowały takie obszary, jak weryfikacja sprzętu i weryfikacja protokołu bezpieczeństwa, które wcześniej wymagały żmudnych, ręcznie prowadzonych odbitek próbnych.

W tej sekcji opisujemy dwie rodziny wydajnych algorytmów do ogólnego wnioskowania o zdarzeniu opartego na sprawdzaniu modelu: jedno podejście oparte na przeszukiwaniu wstecznym, a drugie na przeszukiwaniu lokalnego wznoszenia. Algorytmy te są częścią „technologii” logiki zdań. Opisane przez nas algorytmy służą do sprawdzania spełnialności: problem SAT. (Jak zauważono, przeprowadzenie testów α|= β można przeprowadzić testując niespełnienie wyników α Λ ¬β beta.

Wspomnieliśmy o związku między znalezieniem satysfakcjonującego modelu dla zdania logicznego a znalezieniem rozwiązania problemu spełniania ograniczeń, więc być może nie jest zaskakujące, że dwie rodziny algorytmów spełnialności zdań bardzo przypominają algorytmy wycofywania i lokalne algorytmy wyszukiwania. Są one jednak same w sobie niezwykle ważne, ponieważ wiele kombinatorycznych problemów w informatyce można sprowadzić do sprawdzenia spełnialności zdania zdaniowego. Każde ulepszenie algorytmów spełnialności ma ogromne konsekwencje dla naszej ogólnej zdolności do radzenia sobie ze złożonością.

Algorytm łańcuchowania w przód PL-FC-ENTAILS?(KB,q) określa, czy pojedynczy symbol zdania q – zapytanie – jest związany z bazą wiedzy o określonych klauzulach. Zaczyna się od znanych faktów (dosłownych literałów) w bazie wiedzy. Jeżeli znane są wszystkie przesłanki implikacji, to jej wniosek dodaje się do zbioru znanych faktów. Na przykład, L1,1jeśli i Breeze są znane, a (L₁₁ Λ Breeze) =>B_1,1 znajduje się w bazie wiedzy, wtedy można dodać B_1,1. Proces ten trwa do momentu dodania zapytania q lub do momentu, gdy nie będzie można wykonać dalszych wnioskowań. Algorytm pokazano na rysunku ; głównym punktem do zapamiętania jest to, że biegnie w czasie liniowym.

Najlepszym sposobem zrozumienia algorytmu jest przykład i obraz. Rysunek (a) przedstawia prostą bazę wiedzy o klauzulach Horna ze znanymi faktami A  i B . Rysunek (b) pokazuje tę samą bazę wiedzy narysowaną jako wykres AND–OR.

Na wykresach AND–OR wiele krawędzi połączonych łukiem wskazuje na koniunkcję – każda krawędź musi zostać udowodniona — podczas gdy wiele krawędzi bez łuku wskazuje na alternatywę – można udowodnić dowolną krawędź. Na wykresie łatwo jest zobaczyć, jak działa łańcuchowanie w przód. Znane liście (tutaj A i B ) są ustawiane, a wnioskowanie propaguje wykres tak daleko, jak to możliwe. Gdziekolwiek pojawia się koniunkcja, propagacja czeka na poznanie wszystkich koniunkcji przed kontynuowaniem. Zachęcamy czytelnika do szczegółowego przeanalizowania przykładu. Łatwo zauważyć, że łańcuchowanie w przód jest słuszne: każde wnioskowanie jest zasadniczo zastosowaniem Modus Ponens. Łączenie w przód jest również kompletne: każde zdanie atomowe entailed zostanie wyprowadzone. Najprostszym sposobem, aby to zobaczyć, jest rozważenie końcowego stanu wnioskowanej tabeli (po osiągnięciu przez algorytm ustalonego punktu, w którym nie są możliwe nowe wnioskowania). Tabela zawiera prawdę dla każdego symbolu wywnioskowanego podczas procesu i fałsz dla wszystkich innych symboli. Możemy zobaczyć tabelę jako model logiczny; co więcej, w tym modelu prawdziwe są wszystkie określone klauzule w oryginalnym KB. Aby to zobaczyć, załóż coś przeciwnego, a mianowicie, że w modelu jakieś zdanie  a₁ Λ … Λ a_k => b jest fałszywe. Wtedy a₁ Λ … Λ a_k musi być  prawdą w modelu a b musi być fałszem w modelu. Ale to jest sprzeczne z naszym założeniem, że algorytm osiągnął ustalony punkt, ponieważ mielibyśmy teraz licencję na dodawanie b do KB. Możemy zatem wnioskować, że zbiór zdań atomowych wywnioskowanych w punkcie stałym definiuje model oryginalnego KB. Co więcej, każde zdanie atomowe q, które pociąga za sobą KB, musi być prawdziwe we wszystkich jego modelach, a w szczególności w tym modelu. Dlatego każde zdanie atomowe q musi być wywnioskowane przez algorytm.

Forward chaining jest przykładem ogólnej koncepcji wnioskowania opartego na danych – to znaczy wnioskowania, w którym uwaga zaczyna się od znanych danych. Może być używany w agencie do wyciągania wniosków z nadchodzących percepcji, często bez konieczności kierowania konkretnym zapytaniem. Na przykład agent wumpus może PRZEKAZYWAĆ swoje spostrzeżenia do bazy wiedzy za pomocą przyrostowego algorytmu łańcucha do przodu, w którym nowe fakty mogą być dodawane do programu, aby zainicjować nowe wnioskowania. U ludzi pewna ilość rozumowania opartego na danych pojawia się, gdy pojawiają się nowe informacje. Na przykład, jeśli jestem w domu i słyszę, że zaczyna padać deszcz, może mi się wydawać, że piknik zostanie odwołany. Ale chyba nie przyjdzie mi do głowy, że siedemnasty płatek największej róży w ogrodzie sąsiada zmoknie; ludzie trzymają łańcuchy naprzód pod ścisłą kontrolą, aby nie pogrążyć ich w nieistotnych konsekwencjach.

Algorytm wstecznego łańcucha, jak sama nazwa wskazuje, działa wstecz od zapytania. Jeśli wiadomo, że zapytanie q jest prawdziwe, nie jest wymagana żadna praca. W przeciwnym razie algorytm znajduje te implikacje w bazie wiedzy, której wnioskiem jest q . Jeśli wszystkie przesłanki jednej z tych implikacji można udowodnić (poprzez łańcuchowanie wstecz), to q jest prawdziwe. Po zastosowaniu do zapytania Q na powyższym rysunku, działa ono w dół wykresu, aż dotrze do zbioru znanych faktów, A i B, które stanowią podstawę dowodu. Algorytm jest zasadniczo identyczny z algorytmem AND-LUB-GRAPH-SEARCH . Podobnie jak w przypadku łączenia w przód, wydajna implementacja przebiega w czasie liniowym. Łańcuchy wsteczne to forma rozumowania ukierunkowanego na cel. Przydaje się do odpowiadania na konkretne pytania, takie jak „Co mam teraz zrobić?” i „Gdzie są moje klucze?” Często koszt tworzenia łańcucha wstecznego jest znacznie mniejszy niż liniowy w odniesieniu do rozmiaru bazy wiedzy, ponieważ proces dotyczy tylko istotnych faktów.

Kompletność rozwiązania sprawia, że ​​jest to bardzo ważna metoda wnioskowania. Jednak w wielu praktycznych sytuacjach nie jest potrzebna pełna moc rozdzielczości. Niektóre bazy wiedzy ze świata rzeczywistego spełniają pewne ograniczenia dotyczące formy zawartych w nich zdań, co umożliwia im stosowanie bardziej ograniczonego i wydajnego algorytmu wnioskowania. Jedną z takich ograniczonych form jest zdanie określone, które jest alternatywą literałów, z których dokładnie jeden jest pozytywny. Na przykład zdanie (¬L_1,1 V ¬Breeze V B_1,1)jest zdaniem określonym, podczas gdy (¬B_1,1 V P_1,2 V P_2,1 )nie jest, ponieważ zawiera dwie zdania pozytywne. Nieco ogólniejsza jest klauzula Horn, będąca alternatywą dosłownych, z których co najwyżej jeden jest pozytywny. Zatem wszystkie zdania określone są zdaniami Horna, podobnie jak zdania bez literałów dodatnich; są to tak zwane klauzule bramkowe. Klauzule rogów są zamykane po rozwiązaniu: jeśli rozpatrzysz dwie klauzule rogów, otrzymasz z powrotem klauzulę rogów. Jeszcze jedna klasa to zdanie k-CNF, które jest zdaniem CNF, w którym każda klauzula ma co najwyżej k literałów.

Bazy wiedzy zawierające tylko zdania określone są interesujące z trzech powodów:

1. Każde zdanie określone można zapisać jako implikację, której przesłanką jest koniunkcja literałów pozytywnych, a zakończeniem jest pojedynczy literał pozytywny. Na przykład zdanie (¬L_1,1 ∨ ¬Breeze ∨ B_1,1) określone może być zapisane jako implikacja (L_1,1 ∧ Breeze) ⇒ B_1,1 . W formie implikacyjnej zdanie jest łatwiejsze do zrozumienia: mówi, że jeśli agent jest w [1,1] i istnieje przewiewny percept, to [1,1] jest przewiewny. W formie Horn założenie nazywa się ciałem, a zakończenie nazywa się głową. Zdanie składające się z jednego pozytywnego literału, takiego jak L1,1, nazywa się faktem. Można go również napisać w formie implikacji jako True ⇒ L_1,1 ale prościej jest napisać po prostu L_1,1 .
2. Wnioskowanie z klauzulami Horna można wykonać za pomocą algorytmów łączenia w przód i wstecz, które wyjaśnimy dalej. Oba te algorytmy są naturalne, ponieważ kroki wnioskowania są oczywiste i łatwe do naśladowania dla ludzi. Ten rodzaj wnioskowania jest podstawą programowania logicznego
3. Decydowanie o pociągnięciu za pomocą klauzul Horna można przeprowadzić w czasie, który jest liniowy w wielkości bazy wiedzy – miła niespodzianka.

Kończąc naszą dyskusję na temat rozdzielczości, pokazujemy teraz, dlaczego PL-RESOLUTION jest kompletne. Aby to zrobić, wprowadzamy zamknięcie rozdzielczości RC(S) zbioru klauzul , który jest zbiorem wszystkich klauzul, które można wyprowadzić przez wielokrotne zastosowanie reguły rozwiązywania do klauzul w S lub ich pochodnych. Zamknięcie rozdzielczości jest tym, co PL-RESOLUTION oblicza jako końcową wartość klauzul zmiennych. Łatwo zauważyć, że RC(S) musi być skończony: dzięki etapowi rozkładania na czynniki istnieje tylko skończenie wiele odrębnych klauzul, które można skonstruować z symboli P1 … Pk występujących w S . Dlatego PL-RESOLUTION zawsze się kończy.

Twierdzenie o zupełności dla rozwiązania w logice zdań nazywa się twierdzeniem o rozdzielczości podstawowej: Jeśli zbiór klauzul jest niezadowalający, to zamknięcie rozdzielczości tych klauzul zawiera pustą klauzulę.

Twierdzenie to jest udowodnione przez wykazanie jego przeciwieństwa: jeśli domknięcie RC(S) nie zawiera pustego zdania, to S jest spełnialne. W rzeczywistości możemy skonstruować model dla S z odpowiednimi wartościami prawdy dla P₁ … P_k. Procedura budowy wygląda następująco:

Dla od 1 do k ,

– Jeśli klauzula w RC(S) zawiera literał ¬Pi i wszystkie inne literały są fałszywe w ramach przypisania wybranego dla P₁ … P_i-1 , przypisz false do Pi.

 – W przeciwnym razie przypisz true do Pi .

To przypisanie do P₁ … P_k  jest modelem  S . Aby to zobaczyć, załóżmy odwrotnie – że na pewnym etapie sekwencji przypisanie symbolu Pi powoduje, że pewna klauzula C staje się fałszywa. Aby tak się stało, musi być tak, że wszystkie inne literały w C muszą już zostać sfałszowane przez przypisania do Pi … Pi-1. Tak więc C musi teraz wyglądać albo (false V false V false … false V Pi) albo jak (false V false V false … false V ¬). Jeśli tylko jedna z tych dwóch klauzul jest w RC(S), algorytm przypisze odpowiednią wartość prawdy do Pi aby C była prawdziwa, więc C może zostać sfalsyfikowana tylko wtedy, gdy obie te klauzule są w RC(S). Teraz, ponieważ RC(S) jest zamykany podczas rozwiązywania, będzie zawierał rezolucję z tych dwóch klauzul, a ta rezolucja będzie miała wszystkie swoje literały już sfalsyfikowane przez przypisania do Pi…P_i-1 . Przeczy to naszemu założeniu, że pierwsze zdanie sfalsyfikowane pojawia się na etapie. Dlatego udowodniliśmy, że konstrukcja nigdy nie fałszuje zdania w RC(S); to znaczy tworzy model RC(S). Wreszcie, ponieważ S jest zawarty w RC(S), każdy model RC(S) jest modelem samego siebie S

Procedury wnioskowania oparte na rezolucji działają z wykorzystaniem wprowadzonej na stronie 223 zasady dowodu przez sprzeczność. To znaczy, aby to pokazać KB |= α , pokazujemy, że (KB Λ ¬α) jest to niezadowalające. Robimy to, udowadniając sprzeczność. Algorytm rozdzielczości pokazano tu

Najpierw (KB Λ ¬α)  jest konwertowany na CNF. Następnie do powstałych klauzul stosuje się zasadę resolution. Każda para, która zawiera literały komplementarne, jest rozwiązywana w celu utworzenia nowej klauzuli, która jest dodawana do zestawu, jeśli jeszcze nie istnieje. Proces trwa, dopóki nie wydarzy się jedna z dwóch rzeczy:

* nie ma nowych klauzul, które można dodać, w tym przypadku KB nie pociąga to za sobą ; lub,

* dwie klauzule dają pustą klauzulę, w tym przypadku KB pociąga za sobą α

Zdanie puste — alternatywa braku rozłączeń — jest równoważne z fałszem, ponieważ alternatywa jest prawdziwa tylko wtedy, gdy przynajmniej jedno z jej rozłączeń jest prawdziwe. Co więcej, pusta klauzula powstaje tylko w wyniku rozwiązania dwóch sprzecznych klauzul jednostkowych, takich jak P i ¬P . Możemy zastosować procedurę rozwiązywania do bardzo prostego wnioskowania w świecie wumpusa. Gdy agent jest w [1,1], nie ma wiatru, więc nie może być dołów na sąsiednich polach. Odpowiednią bazą wiedzy jest

i chcemy udowodnić , czyli powiedzmy ¬P_1,2 . Kiedy konwertujemy (KB Λ ¬α)do CNF, otrzymujemy klauzule pokazane na górze rysunku

Drugi wiersz rysunku pokazuje klauzule uzyskane przez rozwiązywanie par w pierwszym wierszu. Następnie, gdy P1,2 zostanie rozwiązany z ¬P1,2 , otrzymujemy pustą klauzulę, pokazaną jako mały kwadrat. Analiza rysunku pokazuje, że jakiekolwiek kroki w celu rozwiązania problemu są bezcelowe. Na przykład klauzula B1.1 V ¬B1,1 V P1.2  jest równoważna z True V P1,2 co jest równoważne z True. Wnioskowanie, że prawda jest prawdziwa, nie jest zbyt pomocne. Dlatego każda klauzula, w której pojawiają się dwa uzupełniające się literały, można odrzucić.