Algorytm DPLL

DPLL

Po 5 bezowocnych próbach (kolor czerwony) wybranie przypisania zmiennej a =1, b =1 prowadzi po propagacji jednostek (dół) do sukcesu (kolor zielony) : lewy górny wzór CNF jest spełnialny.
Klasa	Boolowski problem spełnialności
Struktura danych	Drzewo binarne
Wydajność w najgorszym przypadku	${\ Displaystyle O (2 ^ {n})}$
Najlepsza wydajność	${\ Displaystyle O (1)}$ (stała)
Złożoność przestrzeni w najgorszym przypadku	${\ Displaystyle O (n)}$ (podstawowy algorytm)

W logice i informatyce algorytm Davisa -Putnama-Logemanna-Lovelanda ( DPLL ) jest kompletnym algorytmem przeszukiwania opartym na śledzeniu wstecznym do decydowania o spełnialności formuł logiki zdań w koniunkcyjnej postaci normalnej , tj. do rozwiązywania problemu CNF-SAT .

Został wprowadzony w 1961 roku przez Martina Davisa , George'a Logemanna i Donalda W. Lovelanda i jest udoskonaleniem wcześniejszego algorytmu Davisa-Putnama , który jest procedurą opartą na rozdzielczości , opracowaną przez Davisa i Hilary Putnamów w 1960 roku. Zwłaszcza w starszych publikacjach, Algorytm Davisa – Logemanna – Lovelanda jest często nazywany „metodą Davisa – Putnama” lub „algorytmem DP”. Inne popularne nazwy, które utrzymują to rozróżnienie, to DLL i DPLL.

Wdrożenia i aplikacje

Problem SAT jest ważny zarówno z teoretycznego, jak i praktycznego punktu widzenia. W teorii złożoności był to pierwszy problem, który okazał się NP-zupełny i może pojawić się w wielu różnych zastosowaniach, takich jak sprawdzanie modeli , automatyczne planowanie i harmonogramowanie oraz diagnostyka w sztucznej inteligencji .

W związku z tym pisanie wydajnych solwerów SAT jest tematem badań od wielu lat. GRASP (1996-1999) był wczesną implementacją wykorzystującą DPLL. W międzynarodowych zawodach SAT wdrożenia oparte na DPLL takie jak zChaff i MiniSat zajmowały pierwsze miejsca w konkursach w 2004 i 2005 roku.

Innym zastosowaniem, które często obejmuje DPLL, jest zautomatyzowane dowodzenie twierdzeń lub teorie modulo spełnialności (SMT), które są problemem SAT, w którym zmienne zdań są zastępowane formułami innej teorii matematycznej .

Algorytm

Podstawowy algorytm śledzenia wstecznego działa poprzez wybranie literału, przypisanie mu wartości logicznej , uproszczenie formuły, a następnie rekurencyjne sprawdzenie, czy uproszczona formuła jest spełnialna; w takim przypadku oryginalna formuła jest zadowalająca; w przeciwnym razie przeprowadzane jest to samo sprawdzanie rekurencyjne przy założeniu przeciwnej wartości logicznej. Nazywa się to regułą podziału , ponieważ dzieli problem na dwa prostsze podproblemy. Krok uproszczenia zasadniczo usuwa wszystkie klauzule, które stają się prawdziwe w ramach przypisania z formuły, oraz wszystkie literały, które stają się fałszywe z pozostałych klauzul.

Algorytm DPLL udoskonala algorytm cofania dzięki gorliwemu stosowaniu następujących reguł na każdym kroku:

Propagacja jednostkowa

Jeśli klauzula jest klauzulą ​​jednostkową , tj. zawiera tylko jeden nieprzypisany literał, klauzula ta może być spełniona jedynie poprzez przypisanie wartości niezbędnej do uczynienia tego literału prawdziwym. Zatem wybór nie jest konieczny. Propagacja jednostek polega na usunięciu każdej klauzuli zawierającej literał klauzuli jednostkowej i odrzuceniu dopełnienia literału klauzuli jednostkowej z każdej klauzuli zawierającej to uzupełnienie. W praktyce często prowadzi to do deterministycznej kaskady jednostek, co pozwala uniknąć dużej części naiwnej przestrzeni poszukiwań.

Czysta eliminacja literalna

Jeśli zmienna zdaniowa występuje tylko z jedną biegunowością we wzorze, nazywa się ją czystą . Czysty literał zawsze można przypisać w taki sposób, aby wszystkie zawierające go klauzule były prawdziwe. Tak więc, gdy jest przypisany w taki sposób, klauzule te nie ograniczają już wyszukiwania i można je usunąć.

Niespełnialność danego przypisania cząstkowego jest wykrywana, gdy jedna klauzula staje się pusta, tzn. gdy wszystkie jej zmienne zostały przypisane w sposób powodujący, że odpowiednie literały są fałszywe. Spełnialność formuły jest wykrywana, gdy wszystkie zmienne są przypisane bez generowania pustej klauzuli lub, we współczesnych implementacjach, jeśli wszystkie klauzule są spełnione. Niespełnialność pełnej formuły można wykryć dopiero po wyczerpujących poszukiwaniach.

Algorytm DPLL można podsumować w następującym pseudokodzie, gdzie Φ jest formułą CNF :

 algorytmu  DPLL: Zestaw klauzul Φ. Dane wyjściowe: wartość logiczna wskazująca, czy Φ jest spełnialne.  

 
        
           funkcja  DPLL  (Φ)  podczas gdy  istnieje klauzula jednostkowa {  l  } w Φ  do  Φ ←  propagacja jednostkowa  (  l  , Φ);  podczas gdy  istnieje literał  l  , który występuje czysty w Φ  do  Φ ←  czysto-dosłowne-przypisanie  (  l  , Φ);  jeśli  Φ jest puste  , zwróć  prawdę  ;  jeśli  Φ zawiera pustą klauzulę,  to  zwróć  fałsz;  l  ←  literał wyboru  (Φ);  zwróć  DPLL  (Φ  ∧  {l})  lub  DPLL  (Φ  ∧  {not(l)}); 

• „←” oznacza przypisanie . Na przykład „ największy ← przedmiot ” oznacza, że ​​wartość największego zmienia się na wartość elementu .
• „ return ” kończy działanie algorytmu i wyświetla następującą wartość.

W tym pseudokodzie unit-propagate(l, Φ) i pure-literal-assign(l, Φ) są funkcjami, które zwracają wynik zastosowania odpowiednio propagacji jednostek i reguły czystego literału do literału l i wzoru Φ . Innymi słowy, we wzorze Φ zastępują każde wystąpienie l słowem „prawda”, a każde wystąpienie słowa „ nie l ” słowem „fałsz” i upraszczają wynikowy wzór. Lub w instrukcji return jest operatorem zwierającym . Φ ∧ ​​{l} oznacza uproszczony wynik podstawienia „prawdy” za l w Φ .

Algorytm kończy się w jednym z dwóch przypadków. Formuła CNF Φ jest pusta, tzn. nie zawiera klauzuli. Następnie jest spełniony przez dowolne przypisanie, ponieważ wszystkie jego klauzule są próżniowo prawdziwe. W przeciwnym razie, gdy formuła zawiera pustą klauzulę, klauzula jest próżniowo fałszywa, ponieważ alternatywa wymaga co najmniej jednego elementu, który jest prawdziwy, aby cały zbiór był prawdziwy. W tym przypadku istnienie takiej klauzuli implikuje, że formuła (oceniana jako koniunkcja wszystkich klauzul) nie może mieć wartości prawdziwej i musi być niespełnialna.

Funkcja pseudokodu DPLL zwraca tylko informację, czy ostateczne przypisanie spełnia formułę, czy nie. W rzeczywistej implementacji częściowe satysfakcjonujące zadanie jest zazwyczaj zwracane po pomyślnym wykonaniu; można to wywnioskować, śledząc rozgałęzione literały i przypisania dosłowne wykonane podczas propagacji jednostek i czystej eliminacji dosłownej.

Algorytm Davisa – Logemanna – Lovelanda zależy od wyboru literału rozgałęziającego , który jest literałem branym pod uwagę w kroku cofania. W rezultacie nie jest to dokładnie algorytm, ale raczej rodzina algorytmów, po jednym dla każdego możliwego sposobu wyboru literału rozgałęziającego. Na wydajność duży wpływ ma wybór literału rozgałęziającego: istnieją przypadki, dla których czas działania jest stały lub wykładniczy, w zależności od wyboru literału rozgałęziającego. Takie funkcje wyboru są również nazywane funkcjami heurystycznymi lub heurystykami rozgałęziającymi.

Wyobrażanie sobie

Davis, Logemann, Loveland (1961) opracowali ten algorytm. Niektóre właściwości tego oryginalnego algorytmu to:

• Opiera się na wyszukiwaniu.
• Jest podstawą prawie wszystkich nowoczesnych solwerów SAT.
• Nie wykorzystuje uczenia się ani nie-chronologicznego cofania się (wprowadzone w 1996 r.).

Przykład z wizualizacją algorytmu DPLL z chronologicznym cofaniem:

• 

  Wszystkie klauzule tworzące formułę CNF

• 

  Wybierz zmienną

• 

  Podejmij decyzję, zmienna a = Fałsz (0), więc zielone klauzule staną się Prawdą

• 

  Po podjęciu kilku decyzji znajdujemy wykres implikacji , który prowadzi do konfliktu.

• 

  Teraz wróć do natychmiastowego poziomu i siłą przypisz przeciwną wartość tej zmiennej

• 

  Ale wymuszona decyzja wciąż prowadzi do kolejnego konfliktu

• 

  Wróć do poprzedniego poziomu i podejmij wymuszoną decyzję

• 

  Podjąć nową decyzję, ale prowadzi to do konfliktu

• 

  Podjąć wymuszoną decyzję, ale znowu prowadzi to do konfliktu

• 

  Powrót do poprzedniego poziomu

• 

  Kontynuuj w ten sposób i końcowy wykres implikacji

Powiązane algorytmy

Od 1986 r. Binarne diagramy decyzyjne (zredukowane uporządkowane) są również używane do rozwiązywania SAT.

W latach 1989-1990 została zaprezentowana i opatentowana metoda weryfikacji receptur firmy Stålmarck. Znalazł pewne zastosowanie w zastosowaniach przemysłowych.

DPLL został rozszerzony o automatyczne dowodzenie twierdzeń dla fragmentów logiki pierwszego rzędu za pomocą algorytmu DPLL(T) .

W dekadzie 2010-2019 prace nad ulepszeniem algorytmu doprowadziły do ​​znalezienia lepszych zasad wyboru literałów rozgałęziających i nowych struktur danych, aby algorytm był szybszy, zwłaszcza część dotycząca propagacji jednostek . Jednak głównym ulepszeniem był potężniejszy algorytm, Conflict-Driven Clause Learning (CDCL), który jest podobny do DPLL, ale po osiągnięciu konfliktu „uczy się” głównych przyczyn (przypisań do zmiennych) konfliktu i wykorzystuje te informacje wykonać nie-chronologiczne cofanie się (znane również jako backjumping ), aby uniknąć ponownego dotarcia do tego samego konfliktu. Większość najnowocześniejszych solwerów SAT jest oparta na platformie CDCL od 2019 r.

Stosunek do innych pojęć

Przebiegi algorytmów opartych na DPLL na niezadowalających instancjach odpowiadają dowodom obalenia rozdzielczości drzewa .

Zobacz też

• Złożoność dowodu
• Herbrandyzacja

Ogólny

•   Davies, Martin ; Putnam, Hilary (1960). „Procedura obliczeniowa dla teorii kwantyfikacji” . Dziennik ACM . 7 (3): 201–215. doi : 10.1145/321033.321034 . S2CID 31888376 .
•   Davis, Martin; Logemann, George; Loveland, Donald (1961). „Program maszynowy do udowadniania twierdzeń” . Komunikaty ACM . 5 (7): 394–397. doi : 10.1145/368273.368557 . hdl : 2027/mdp.39015095248095 . S2CID 15866917 .
• Ouyang, Ming (1998). „Jak dobre są reguły rozgałęziania w DPLL?” . Dyskretna matematyka stosowana . 89 (1–3): 281–286. doi : 10.1016/S0166-218X(98)00045-6 .
•   Johna Harrisona (2009). Podręcznik praktycznej logiki i automatycznego wnioskowania . Wydawnictwo Uniwersytetu Cambridge. s. 79–90. ISBN 978-0-521-89957-4 .

Konkretny

Dalsza lektura

•   malajski Ganai; Aarti Gupta; Dr Aarti Gupta (2007). Skalowalne rozwiązania do weryfikacji formalnej oparte na SAT . Skoczek. s. 23–32. ISBN 978-0-387-69166-4 .
•   Gomes, Carla P.; Kautz, Henry; Sabharwal, Ashish; Selman, Bart (2008). „Rozwiązywacze spełnialności”. W Van Harmelen, Frank; Lifschitz, Włodzimierz; Porter, Bruce (red.). Podręcznik reprezentacji wiedzy . Podstawy sztucznej inteligencji. Tom. 3. Elsevier. s. 89–134. doi : 10.1016/S1574-6526(07)03002-7 . ISBN 978-0-444-52211-5 .