Algorytm Davisa-Putnama - Davis–Putnam algorithm

Algorytm Davis-Putnam został opracowany przez Martin Davis i Hilary Putnam do sprawdzania ważności pierwszej kolejności logicznej formuły przy użyciu rozdzielczości -na procedurę decyzyjną dla rachunku zdań . Ponieważ zbiór prawidłowych formuł pierwszego rzędu jest rekurencyjnie przeliczalny, ale nie rekurencyjny , nie istnieje ogólny algorytm do rozwiązania tego problemu. Dlatego algorytm Davisa-Putnama kończy się tylko na prawidłowych formułach. Obecnie termin „algorytm Davisa-Putnama” jest często używany jako synonim procedury decyzyjnej zdaniowej opartej na rozdzielczości (procedura Davisa-Putnama ), która w rzeczywistości jest tylko jednym z etapów oryginalnego algorytmu.

Przegląd

Dwa przebiegi procedury Davisa-Putnama na przykładowych instancjach zdaniowych. Od góry do dołu, od lewej: począwszy od formuły algorytm jest rozwiązywany na , a następnie na . Ponieważ dalsze rozwiązanie nie jest możliwe, algorytm zatrzymuje się; ponieważ pusta klauzula nie może być wyprowadzona, wynikiem jest " satisfiable ". Dobrze: rozwiązanie podanej formuły on , następnie on , następnie on daje pustą klauzulę; stąd algorytm zwraca „ niezaspokojony ”.${\ Displaystyle (a \ lor b \ lor c) \ ziemi (b \ lor \ nie c \ lor \ nie f) \ ziemi (\ nie b \ lor e)}$${\displaystyle b}$${\displaystyle c}$${\displaystyle b}$${\displaystyle a}$${\displaystyle c}$

Procedura opiera się na twierdzeniu Herbranda , z którego wynika, że niespełnialna formuła ma niespełnialną instancję podstawową , oraz na fakcie, że formuła jest ważna wtedy i tylko wtedy, gdy jej negacja jest niesatysfakcjonowana. Podsumowując, fakty te sugerują, że aby udowodnić słuszność φ , wystarczy udowodnić, że podstawowa instancja ¬φ jest niezadowalająca. Jeśli φ jest niepoprawne, wyszukiwanie niezadowalającej instancji podstawowej nie zostanie zakończone.

Procedura sprawdzania poprawności formuły φ składa się z grubsza z tych trzech części:

• umieścić wzór ¬φ w prenex formie i wyeliminować kwantyfikatorów
• wygeneruj wszystkie zdaniowe instancje podstawowe, jedna po drugiej
• sprawdź, czy każda instancja jest satisfiable.
  • Jeśli jakaś instancja jest niezadowalająca, zwróć, że φ jest poprawne. W przeciwnym razie kontynuuj sprawdzanie.

Ostatnia część to solwer SAT oparty na rozdzielczości (jak widać na ilustracji), z gorliwym wykorzystaniem propagacji jednostkowej i czystej eliminacji dosłownej (eliminacja klauzul ze zmiennymi tylko o jednej biegunowości we wzorze).

Algorithm DP SAT solver
    Input: A set of clauses Φ.
    Output: A Truth Value: true if Φ can be satisfied, false otherwise.

function DP-SAT(Φ)
    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, Φ);
    // Davis-Putnam procedure:
    for every literal l that occurs in both polarities in Φ do
       for every clause c containing l and every clause n containing the negation of l in Φ do
           r ← resolve(c, n);
           Φ ← add-to-formula(r, Φ);
       Φ ← remove-from-formula(c, n, Φ);        
    return DP-SAT(Φ)

Na każdym etapie solwera SAT generowana formuła pośrednia jest równoważna , ale prawdopodobnie nie jest równoważna z oryginalną formułą. Etap rozwiązywania prowadzi do najgorszego przypadku wykładniczego zwiększenia rozmiaru formuły.

Algorytm Davis-Putnam-Logemann-Loveland jest 1962 udoskonalenie zdań etapie spełnialności procedury Davis-Putnam który wymaga jedynie liniową ilość pamięci, w najgorszym przypadku. Unika rozwiązania reguły dzielenia : algorytm wsteczny, który wybiera literał l , a następnie rekurencyjnie sprawdza, czy uproszczona formuła z l przypisaną wartością true jest spełnienie, czy też uproszczona formuła z l przypisaną wartością fałsz jest. Nadal stanowi podstawę dla dzisiejszych (od 2015) najbardziej wydajnych kompletnych solwerów SAT .

Zobacz też

• Herbrandyzacja

Bibliografia

• Davisa, Martina; 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 (1962). „Program maszynowy do dowodzenia twierdzeń” . Komunikaty ACM . 5 (7): 394–397. doi : 10.1145/368273.368557 . hdl : 2027/mdp.39015095248095 .
• R. Dechtera; Irlandczyk. „Rozdzielczość kierunkowa: procedura Davisa-Putnama, Revisited” . W J. Doyle i E. Sandewall i P. Torasso (red.). Zasady Reprezentacji Wiedzy i Wnioskowania: Proc. IV Międzynarodowej Konferencji (KR'94) . Kaufmanna. s. 134–145.
• Johna Harrisona (2009). Podręcznik praktycznej logiki i automatycznego wnioskowania . Wydawnictwo Uniwersytetu Cambridge. str.  79 -90. Numer ISBN 978-0-521-89957-4.

Ten formalny artykuł dotyczący metod jest skrótem . Możesz pomóc Wikipedii, rozwijając ją .

• v
• T
• mi