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:
- 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.
- 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.
- 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.
- 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.
- 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 Xi 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.