Algorytm Davisa-Putnama

Algorytm Davisa-Putnama został opracowany przez Martina Davisa i Hilary Putnam w celu sprawdzania poprawności formuły logicznej pierwszego rzędu przy użyciu procedury decyzyjnej opartej na rozdzielczości dla logiki zdań . Ponieważ zbiór prawidłowych formuł pierwszego rzędu jest rekurencyjnie przeliczalny , ale nie rekurencyjny , nie istnieje żaden ogólny algorytm 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 opartej na rezolucjach ( procedura Davisa – Putnama ), która jest w rzeczywistości tylko jednym z etapów oryginalnego algorytmu.

Przegląd

Dwa przebiegi procedury Davisa-Putnama na przykładowych zdaniowych przypadkach podstawowych. Od góry do dołu, po lewej: zaczynając od wzoru $\ Displaystyle (a \ lor b \ lor c) \ land (b \ lor \ lnot c \ lor \ lnot f) \ land (\ lnot b \ lor e)}$ , algorytm rozstrzyga na ${\ displaystyle b}$ , a następnie na ${\ displaystyle c}$ . Ponieważ dalsza rozdzielczość nie jest możliwa, algorytm zatrzymuje się; ponieważ pustej klauzuli , wynikiem jest „ satisfiable ”. Po $prawej$ : rozwiązanie podanej formuły na $,$ na $a$ na daje pustą klauzulę; stąd algorytm zwraca „ niezadowalający ”.

Procedura opiera się na twierdzeniu Herbranda , z którego wynika, że ​​niespełnialna formuła ma niezadowalający przypadek podstawowy , oraz na fakcie, że formuła jest ważna wtedy i tylko wtedy, gdy jej negacja jest niespełnialna. Podsumowując, fakty te sugerują, że aby udowodnić ważność φ, wystarczy udowodnić, że podstawowa instancja ¬φ jest niespełnialna. Jeśli φ nie jest poprawne, to poszukiwanie niezadowalającej instancji naziemnej nie zostanie zakończone.

Procedura sprawdzania ważności wzoru φ składa się z grubsza z trzech części:

• zapisz formułę ¬φ w formie prenex i wyeliminuj kwantyfikatory
• generować wszystkie instancje naziemne zdań, jeden po drugim
• sprawdź, czy każda instancja jest zadowalająca.
  • Jeśli jakaś instancja jest niezadowalająca, zwróć, że φ jest poprawna. W przeciwnym razie kontynuuj sprawdzanie.

Ostatnia część to solver SAT oparty na rozdzielczości (jak widać na ilustracji), z gorliwym wykorzystaniem propagacji jednostek i czysto literalnej eliminacji (eliminacja klauzul ze zmiennymi, które występują tylko pozytywnie lub tylko negatywnie w formule).

 Algorytm  DP SAT solver Dane wejściowe: Zbiór klauzul Φ. Dane wyjściowe: Wartość logiczna: prawda, jeśli Φ może być spełnione, w przeciwnym razie fałsz.  

        
        
       
            
       
           
            
             funkcja  DP-SAT(Φ)  powtórz  //  propagacja jednostek:  podczas gdy  Φ zawiera klauzulę jednostkową {  l  }  do  Φ ←  usuń-z-formuły  ({  l  }, Φ);  dla każdego  zdania  c  w Φ, które zawiera ¬  l  do  Φ ←  usuń-z-formuły  (  c  , Φ); Φ ←   dodać do wzoru  (  c  \ {¬  l  }, Φ); //   wyeliminuj klauzule nie w normalnej formie:  dla każdej  klauzuli  c  w Φ, która zawiera zarówno literał  l,  jak i jego zaprzeczenie ¬l  do  Φ  ←  usuń-z-formuły  (  c  , Φ); //   czysta eliminacja literalna:  podczas gdy  istnieje literał  l  , który występuje czysty w Φ  do  dla każdej  klauzuli  c  w Φ, która zawiera  l  do  Φ ←  usuń-z-formuły  (  c  , Φ); //   warunki zatrzymania:  jeśli  Φ jest puste  , zwróć  prawdę  ;  jeśli  Φ zawiera pustą klauzulę,  to  zwróć  fałsz; //   Procedura Davisa-Putnama:  wybierz literał  l  występujący z obiema polaryzacjami w Φ  dla każdej  klauzuli  c  w Φ zawierającej  l  i każdej klauzuli  n  w Φ zawierającej jej negację ¬  l  do  //  rozwiąż c z n:  r  ← (  c  \ {  l  }) ∪ (  n  \ {¬  l  }); Φ ←   dodatek do wzoru  (  r  , Φ);  dla każdego  zdania  c  zawierającego  l  lub ¬l  do  Φ  ←  usuń-z-formuły  (  c  , Φ); 

• „←” 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ść.

Na każdym etapie solwera SAT wygenerowana formuła pośrednia jest równospełnialna , ale prawdopodobnie nie równoważna , z pierwotną formułą. Krok rozwiązania prowadzi do wykładniczego powiększenia rozmiaru formuły w najgorszym przypadku.

Algorytm Davisa – Putnama – Logemanna – Lovelanda to udoskonalenie z 1962 r. Kroku spełnialności zdań procedury Davisa – Putnama, który w najgorszym przypadku wymaga tylko liniowej ilości pamięci. Unika rozwiązania reguły podziału : algorytm śledzenia wstecznego, który wybiera literał l , a następnie rekurencyjnie sprawdza, czy uproszczona formuła, której l ma przypisaną wartość prawdziwą, jest spełniona, czy też uproszczona formuła, której l ma przypisaną wartość fałsz. Nadal stanowi podstawę dla dzisiejszych (od 2015 r.) Najbardziej wydajnych kompletnych rozwiązań SAT .

Zobacz też

• Herbrandyzacja

• Davis, Martin; Putnam, Hilary (1960). „Procedura obliczeniowa dla teorii kwantyfikacji” . Dziennik ACM . 7 (3): 201–215. doi : 10.1145/321033.321034 .
• Davis, Martin; Logemann, George; Loveland, Donald (1962). „Program maszynowy do udowadniania twierdzeń” . Komunikaty ACM . 5 (7): 394–397. doi : 10.1145/368273.368557 . hdl : 2027/mdp.39015095248095 .
• R. Dechtera; Irlandczyk. „Rozdzielczość kierunkowa: procedura Davisa-Putnama, powtórka”. W J. Doyle i E. Sandewall oraz P. Torasso (red.). Zasady reprezentacji wiedzy i rozumowania: Proc. IV Międzynarodowej Konferencji (KR'94) . Kaufmanna. s. 134–145.
•   Johna Harrisona (2009). Podręcznik praktycznej logiki i automatycznego wnioskowania . Wydawnictwo Uniwersytetu Cambridge. s. 79 –90. ISBN 978-0-521-89957-4 .