Algorytm Stalmarcka

Spis treści:

Problem sprawdzania czy formuła jest tautologią

Dana jest formuła zawierająca: Chcemy się dowiedzieć czy formuła jest tautologią. Na to pytanie odpowiada algorytm Stalmarcka, próbując tautologię udowodnić niewprost: przypuszczamy, że nią nie jest i probujemy dojść do sprzeczności.

Małe przypomnienie z Logiki

Wartościowanie formuły to przypisanie zmiennym wartości TRUE lub FALSE. Formuła spełnialna to taka, dla której istnieje wartościowanie, przy którym przyjmuje ona wartość TRUE. Tautologia - formuła prawdziwa przy każdym wartościowaniu.
Problem co-NP to taki, że jego dopełnienie jest problemem NP (można je zweryfikować w czasie wielomianowym). Analogicznie jak dla problemów NP, definiujemy klasę problemów co-CP-zupełnych. Nie jest znana relacja między klasami co-NP i NP (patrz Cormen).
Problem spełnialności formuł SAT jest problemem NP-zupełnym (nawet spełanialność formuł postaci 3-CNF jest NP-zupełna). Szkic dowodów można znaleźć w Cormenie. Problem weryfikacji tautologii jest zatem problemem co-NP i to co-NP-zupełnym.

Jest wiele metod do badania formuł, np. budowanie tabeli prawdy i przekształcanie formuły do CNF-u, lecz wszystkie te metody mają pesymistyczny koszt wykładniczy względem rozmiaru zadanej formuły. Celem algorymu Stalmarcka jest udowodnienie tautologii w czasie wielomianowym, stosując heurystyki oczywiście.

Algorytm Stalmarcka

UW. Spis reguł i przykład wykonania algorytmu Stalmarcka można znaleźć tutaj.

Etap 0 - Wstępna kanonizacja (ang. Canonisation)
Wstępna obróbka formuły, pozwalająca w późniejszych etapach uniknąć redundancji. Polega na przekształceniu formuły do formuły prostszej i równoważnej formule wyjściowej (konkretna metoda jest mało istotna, aby tylko była niedroga i żeby nie zwiększała radykalnie rozmiaru formuły).
Przykładowo - aplikujemy gdzie się da określony zbiór reguł. Te sprytne reguły umożliwiają pozbycie się z formuły alternatyw i implikacji, a pozostawienie tylko negacji, koniunkcji i równoważności. Jeśli dostaniemy od razu TRUE lub FALSE to koniec. Jeśli nie - męczymy tę formułę dalej.

Etap I - Redukcja do trójek (ang. Reduction to triplets)
Przekształcamy formułę do zbioru "równań", dokładniej trójek typu 
     x <-> y • z
gdzie x, y, z - literały, a &bull - koniunkcja lub równoważność.
UW. Traktujemy TRUE (T) jak zmienną dla wygody, czyli piszemy v = TRUE zamiast v.

Etap II - 0-Saturacja (ang. 0-Saturation)
Stosujemy zbiór prostych reguł (ang. simple rules), żeby uprościć zbiór równań i wywnioskować nowe równania. Jeśli dostaniemy sprzeczność, to koniec. Jeśli nie, pracujemy dalej.
UW. Zakładamy, że równania symetryczne są tożsame, tj. jak mamy w zbiorze x = y to nie generujemy już y = x.

Etap III - 1-Saturacja (ang. 1-Saturation)
Używamy reguły dylematu (ang. dilemma rule), aby rozdzielić bieżący zbiór równań na dwa względem wybranej zmiennej.
Działamy tak: jeśli 0-Saturacja wygenerowała zbiór równań S, to wybieramy zmienną v, a następnie:
  • wykonujemy 0-Saturację dla zbioru S + {v = T} i dostajemy zbiór S(T)
  • wykonujemy 0-Saturację dla zbioru S + {v = ¬T} i otrzymujemy zbiór S(¬T)
    Jeżeli którykolwiek z nich jest sprzeczny, to za nowe S przyjmujemy ten niesprzeczny, a w przeciwnym razie 
         S := S(+) przecięte z S(-)
    Tę procedurę wykonujemy dla wszystkich zmiennych dopóki dostajemy nowe równania. Jeśli dostaniemy sprzeczność, to koniec. Wpr. saturujemy się dalej.

    Etap IV, V, ... -n-Saturacja (ang.n-Saturation)
    Gdy 1-Saturacja nie pomogła, stosujemy 2-Saturację, tj. rozdzielamy zbiór S równań względem par zmiennych, tj. 
        S(T, T) := S + {v = T, z = T}
    i postępujemy analigocznie do kroku III. Saturacje można wykonać dla dowolnej liczby zmiennych.

    • Cechy:

    Czas wykonania?

    DEF. Tautologia n-łatwa (ang. n-easy) - tautologia, która może być udowodniona za pomocą n-Saturacji. Analogicznie formuła n-trudna (ang. n-hard) - taka, która nie może być udowodniona za pomocą (n-1)-Saturacji.

    Czas wykonania algorytmu Stalmarcka zależy głównie od stopnia trudności tautologii. Stalmarck wykazał:

    Jeśli tautologia A rozmiaru |A| jest n-łatwa => istnieje jej dowód rozmiaru O(|A|^(n+1)). Ponadto, algorytm n-saturacji na pewno znajdzie dowód tej tautologii i to w czasie O(|A|^(2n+1)).

    Czas jest wielomianowy, ale potencjalnie dużego stopnia. Czy o nie za dużo, żeby stosować algorytm w praktyce?
    Rzeczywiście, dla dużych formuł już 2-Saturacja trwa niepraktycznie długo. Okazuje się jednak, że w większości przypadków 1-Saturacja wystarcza.

    Zarys implementacji algorytmu Stalmarcka

    Dostępnych implementacji nie ma wiele, ani nie są zrobione naprawdę wydajnie. Przykładową implementację można pobrać     stąd. W [2] zaproponowano dwie implementacje: bezpośrednią oraz bazującą na logice wyższego rzędu HOL (po dokładniejsze informacje parz [2]).
    Logika wyższego rzędu (ang. HOL - Higher order logic) - logika(i) zaprojektowana dla programów dowodzących twierdzenia (ang. theorem provers). Dokładniejsze informacje można znaleźć tutaj, ale na potrzeby tego referatu możemy mysleć o HOL jako o logice pierwszego rzędu, albo nawet o rachunku predykatów.

    Przechowywanie równań

    Dla każdej zmiennej (także tych sztucznie wyprodukowanych) alokujemy liczbę całkowitą dodatnią jako identyfikator. Negację zmiennej reprezentujemy jako liczbę ujemną (nie można używać 0 oczywiście). TRUE i FALSE reprezentujemy jako 1 i -1. Każdej zmiennej przyisujemy: albo 1/-1 jeśli można, albo listę innych zmiennych do niej przypisanych, tj. wziętych z równań x = +/-y, gdzie x, y > 0 i x > y (tworzymy tablicę przypisań (ang. assignments table)). W tej tablicy wiersz sprzeczny oznacza się zerem, które tylko w tym przypadku się używa.

    Główna pętla

    Główna pętla jest prosta: generujemy nowe równania i staramy się wnioskować z prostych reguł.
    Korzystamy z dodatkowych struktur, np. struktura pamiętająca dla każdej zmiennej, w których trójkach się ona znajduje.

    Dwa etapy saturacji

    Okazuje się, że najlepiej wykonywać saturację w dwóch krokach:
    1. wyszukiwanie zmiennych, dla których rozdzielenie da nam sprzeczność
    2. etap wnioskowania

    Zastosowania algorytmu Stalmarcka:

    Bibliografia

    1. J. Harrison, Starmarck's Algorithm as HOL Derived Rule, Uniwersytet w Abo w Finlandii
    2. T. Cormen, Wprowadzenie do algorytmów, WNT, Warszawa 1997, rozdział 36. NP-zupełność

    O prezentacji...

    Prezentacja przygotowana została przez: 
           Elżbietę Krępską
    w ramach przedmiotu Sztuczna Inteligencja i Systemy Doradcze.
    Data: maj 2004 r.