Algorytm DPLL - DPLL algorithm

DPLL

We wzorze CNF-SAT : 1-Wybierz dosłowny 2-Przypisz mu wartość prawdy 3-Uprość formułę 4-Sprawdź satisfiablity; 5-Jeśli nie jesteś zadowolony, wykonaj cofanie
Klasa	Problem spełnialności logicznej
Struktura danych	Drzewo binarne
Wydajność w najgorszym przypadku	${\ Displaystyle O (2 ^ {n})}$
Wydajność w najlepszym przypadku	${\ Displaystyle O (1)}$ (stały)
Najgorsza złożoność przestrzeni	${\ Displaystyle O (n)}$ (podstawowy algorytm)

W logice i informatyce The Davis-Putnam-Logemann-Loveland ( DPLL ) algorytm jest kompletna , backtracking opartych algorytm wyszukiwania dla rozstrzygnięcia spełnialności z zdaniowych formuł logicznych w koniunkcyjnej postaci normalnej , czyli rozwiązywania CNF-SAT problem.

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 1960 roku. Algorytm Davisa-Logemanna-Lovelanda jest często określany jako „metoda Davisa-Putnama” lub „algorytm DP”. Inne popularne nazwy, które zachowują rozróżnienie, to DLL i DPLL.

Po ponad 50 latach procedura DPLL nadal stanowi podstawę najbardziej wydajnych kompletnych solwerów SAT. Ostatnio został rozszerzony o automatyczne dowodzenie twierdzeń dla fragmentów logiki pierwszego rzędu za pomocą algorytmu DPLL(T) .

Wdrożenia i aplikacje

Problem SAT jest ważna zarówno z teoretycznego 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 od wielu lat jest gorącym tematem w badaniach, a regularnie odbywają się konkursy między solwerami SAT . Nowoczesne wdrożenia firmy DPLL takie jak Chaff i zChaff , GRASP czy MiniSat zajmują pierwsze miejsca w konkursach ostatnich lat.

Inną aplikacją, która często wiąże się z DPLL, jest automatyczne dowodzenie twierdzeń lub teorie modulo spełnialności (SMT), które są problemem SAT, w którym zmienne zdaniowe są zastępowane formułami innej teorii matematycznej .

Algorytm

Podstawowy algorytm wycofywania działa, wybierając literał, przypisując mu wartość prawdy , upraszczając formułę, a następnie rekurencyjnie sprawdzając, czy uproszczona formuła jest spełnialna; jeśli tak jest, oryginalna formuła jest zadowalająca; w przeciwnym razie to samo sprawdzanie rekurencyjne jest wykonywane przy założeniu przeciwnej wartości logicznej. Jest to znane jako reguła podziału , ponieważ dzieli problem na dwa prostsze podproblemy. Krok upraszczania zasadniczo usuwa z formuły wszystkie klauzule, które stają się prawdziwe w ramach przypisania, oraz wszystkie literały, które stają się fałszywe z pozostałych klauzul.

Algorytm DPLL jest lepszy od algorytmu z wycofywaniem się poprzez gorliwe stosowanie 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 tylko przez przypisanie wartości niezbędnej, aby ten literał był prawdziwy. Dlatego wybór nie jest konieczny. Propagacja jednostkowa polega na usunięciu każdej klauzuli zawierającej literał klauzuli unit oraz odrzuceniu uzupełnienia literału klauzuli unit z każdej klauzuli zawierającej to uzupełnienie. W praktyce prowadzi to często do deterministycznych kaskad jednostek, unikając w ten sposób dużej części naiwnej przestrzeni poszukiwań.

Czysta dosłowna eliminacja

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

Niespełnienie danego przypisania częściowego jest wykrywane, gdy jedna klauzula staje się pusta, tj. jeśli wszystkie jej zmienne zostały przypisane w taki sposób, że odpowiednie literały są fałszywe. Spełnialność formuły jest wykrywana, gdy wszystkie zmienne są przypisane bez generowania pustej klauzuli lub, w nowoczesnych implementacjach, jeśli wszystkie klauzule są spełnione. Niespełnienie pełnej formuły można wykryć dopiero po wyczerpującym wyszukiwaniu.

Algorytm DPLL można streścić w następującym pseudokodzie, gdzie Φ jest wzorem CNF :

Algorithm DPLL
    Input: A set of clauses Φ.
    Output: A Truth Value.

function DPLL(Φ)
    if Φ is a consistent set of literals then
        return true;
    if Φ contains an empty clause then
        return false;
    for every unit clause {l} in Φ do
        Φ ← unit-propagate(l, Φ);
    for every literal l that occurs pure in Φ do
        Φ ← pure-literal-assign(l, Φ);
    l ← choose-literal(Φ);
    return DPLL(Φ ∧ {l}) or DPLL(Φ ∧ {not(l)});

W tym pseudokod, unit-propagate(l, Φ)i pure-literal-assign(l, Φ)są to funkcje zwraca wynik stosowania propagacji jednostkowej i czystą zasadę dosłownego, odpowiednio, dosłownym li wzoru Φ. Innymi słowy, zastępują każde wystąpienie słowa l„prawda” i każde wystąpienie not l„fałszem” w formule Φi upraszczają wynikową formułę. orW returnoświadczeniu jest operator zwarcie . oznacza uproszczony wynik podstawienia „prawda” za in . Φ ∧ {l}lΦ

Algorytm kończy się w jednym z dwóch przypadków. Albo wzór CNF Φokazuje się zawierać spójnego zestawu literałach -to znaczy, że nie jest l, a ¬ldla każdego dosłownym lo wzorze (nie tylko czyste literałami). W takim przypadku zmienne można w trywialny sposób zaspokoić, ustawiając je w wartościowaniu zgodnie z polaryzacją literału obejmującego. W przeciwnym razie, gdy formuła zawiera pustą klauzulę, klauzula ta jest bezwzględnie fałszywa, ponieważ alternatywa wymaga co najmniej jednego elementu członkowskiego, który jest prawdziwy, aby cały zestaw był prawdziwy. W tym przypadku istnienie takiego zdania implikuje, że formuła (oceniana jako koniunkcja wszystkich zdań) nie może zostać oceniona jako prawdziwa i musi być niezaspokojona.

Funkcja DPLL pseudokodu zwraca tylko to, czy końcowe przypisanie spełnia formułę, czy nie. W prawdziwej implementacji częściowe satysfakcjonujące zadanie zazwyczaj jest również zwracane w przypadku powodzenia; można to wyprowadzić ze spójnego zestawu literałów pierwszej ifinstrukcji funkcji.

Algorytm Davisa-Logemanna-Lovelanda zależy od wyboru literału rozgałęziającego , który jest literałem rozważanym na etapie cofania. W rezultacie nie jest to dokładnie algorytm, ale raczej rodzina algorytmów, po jednym na każdy możliwy sposób wyboru literału rozgałęziającego. Na wydajność silnie wpływa 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łów rozgałęziających. Takie funkcje wyboru są również nazywane funkcjami heurystycznymi lub heurystykami rozgałęziającymi.

Wyobrażanie sobie

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

• Opiera się na wyszukiwaniu.
• Jest podstawą prawie wszystkich nowoczesnych solwerów SAT.
• To nie używać nauki lub wycofywania non-chronologiczny (wprowadzone w 1996 roku).

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

• 

  Wszystkie klauzule tworzące formułę CNF

• 

  Wybierz zmienną

• 

  Podejmij decyzję, zmienna a = False (0), więc zielone zdania stają się True

• 

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

• 

  Teraz cofnij się do bezpośredniego poziomu i siłą przypisz przeciwną wartość do tej zmiennej

• 

  Ale wymuszona decyzja wciąż prowadzi do kolejnego konfliktu

• 

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

• 

  Podejmij nową decyzję, ale prowadzi to do konfliktu

• 

  Podejmij wymuszoną decyzję, ale znowu prowadzi to do konfliktu

• 

  Wróć do poprzedniego poziomu

• 

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

Aktualna praca

W latach 2010 prace nad udoskonaleniem algorytmu prowadzono na trzech kierunkach:

1. Definiowanie różnych zasad wyboru literałów rozgałęziających.
2. Definiowanie nowych struktur danych w celu przyspieszenia algorytmu, zwłaszcza części dotyczącej propagacji jednostek .
3. Definiowanie wariantów podstawowego algorytmu cofania. Ten ostatni kierunek obejmuje niechronologiczne wycofywanie się (tzw. backjumping ) i uczenie się klauzul . Te udoskonalenia opisują metodę wycofywania się po osiągnięciu klauzuli konfliktu, która „uczy się” przyczyn źródłowych (przypisania do zmiennych) konfliktu, aby uniknąć ponownego osiągnięcia tego samego konfliktu. Uzyskane rozwiązania SAT oparte na konfliktach oparte na uczeniu się klauzul są najnowocześniejsze w 2014 roku.

Nowszym algorytmem z 1990 roku jest metoda Stålmarcka . Również od 1986 r. (zredukowane uporządkowanie) binarne diagramy decyzyjne są również używane do rozwiązywania SAT.

Związek z innymi pojęciami

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

Zobacz też

• Dowód złożoności
• Herbrandyzacja

Bibliografia

Generał

• Davis, Marcin ; Putnam, Hilary (1960). „Procedura obliczeniowa dla teorii kwantyfikacji” . Dziennik ACM . 7 (3): 201–215. doi : 10.1145/321033.321034 .
• Davisa, Martina; Logemann, George; Loveland Donald (1961). „Program maszynowy do dowodzenia twierdzeń” . Komunikaty ACM . 5 (7): 394–397. doi : 10.1145/368273.368557 . hdl : 2027/mdp.39015095248095 .
• 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. Numer ISBN 978-0-521-89957-4.

Konkretny

Dalsza lektura

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