Proof Number Search (pn-search)

Autor: Maciej Maciak

Jest to jeden z algorytmów best - first search, które przeszukują węzły w drzewach gier wybierając zawsze ten, który uważają za najlepszy. Różnica pomiędzy nimi polega na tym, który węzeł zostanie uznany za najlepszy.

Ten algorytm operuje na drzewach AND/OR. Oto ich definicja:

Drzewo uznajemy za rozwiązane gdy jego korzeń ma wartość TRUE lub FALSE (odpowiednio udowodnione, obalone).

W algorytmie możemy stosować dwa rodzaje wyliczania wartości węzła:

Obliczenie wartości węzła J typu AND:

    Jeśli J ma przynajmniej jedno dziecko o wartości FALSE to ma wartość FALSE.

    wpp. Jeśli J ma choć jedno dziecko o wartości UNKNOWN (lub nie wyliczone)- też jest UNKNOWN.

    wpp. J ma wartość FALSE.

Obliczenie wartości węzła J typu OR:

    Jeśli J ma choć jednego potomka o wartości TRUE - ma wartość TRUE.

    wpp. Jeśli J ma choć jednego potomka o wartości UNKNOWN (lub nie wyliczonego) - ma wartość UNKNOWN.

    wpp. J ma wartość FALSE.

W algorytmie pn-search nie znamy rozkładu wartości węzłów, zakładamy o nim, że jest równe.

Definicje:

    Zbiór dowodzący dla drzewa T - taki zbiór liści granicznych, że jeśli pokażemy prawdziwość dla nich wszystkich to udowodnimy drzewo.

    Zbiór obalający dla drzewa T - taki zbiór liści granicznych, że jeśli pokażemy nieprawdziwość dla nich wszystkich to udowodnimy drzewo.

    proof number drzewa T - moc minimalnego zbioru dowodzącego drzewo T.

    disproof number drzewa T - moc minimalnego zbioru obalającego drzewo T.

węzeł J proof number disproof number
J ma wartość TRUE 0 ∞
J ma wartość FALSE ∞ 0
J ma wartość UNKNOWN, jest węzłem wewnętrznym i ma typ AND suma proof number wszystkich dzieci J minimum disproof number wszystkich dzieci J
J ma wartość UNKNOWN, jest węzłem wewnętrznym i ma typ OR minimum proof number wszystkich dzieci J suma disproof number wszystkich dzieci J
J jest liściem (nie ma wartości TRUE lub FALSE) 1 1

W algorytmie rozwiązujemy poddrzewa o najmniejszy proof number lub disproof number. W każdym kroku wybieramy liść z prawdopodobnie najkrótszego rozwiązania. Powtarzamy aż dojdziemy o końca, skończy się czas lub zasoby.

Pytaniem jest czy mamy rozważać proof number, czy disproof number.

Otóż najlepszy wybór spełnia oba te warunki.

def. most proving number J z drzewa T - J jest węzłem granicznym i jeśli J przyjmuje wartość TRUE to zmniejsza proof number o 1, jeśli FALSE - zmniejsza disproof number o 1.

Teza: Dla drzewa T AND/OR i dowolnych zbiorów A, B, takich że:

    A - minimalny niepusty zbiór obalający T

    B - minimalny niepusty zbiór dowodzący T

Przecięcie A i B jest niepuste.

Dowód:

    1. Jeśli T ma jeden węzeł J - A = {J}, B = {J}

    2. Krok indukcyjny: zakładamy, że udowodniliśmy tezę dla wszystkich potoków J1...Jn węzła J typu OR.

        Aby udowodnić J wystarczy udowodnić jednego potomka Jx.

        Niech proof(K) = minimalny zbiór dowodzący K, disp(K) = minimalny zbiór obalający K.

        Istnieje x, że proof(J) = proof(Jx), oraz wiadomo, że disp(J) = ∑disp(Ji)    i = 1..n

        Z założenia indukcyjnego wiemy, że disp(Jx) ∩ proof(Jx) ≠ Ř. Zatem disp(J) ∩ proof(J) ≠ Ř.

      Dowód dla J typu AND analogiczny (znajduje się w notatkach).

Zatem pokazaliśmy, że węzeł most proving node zawsze istnieje. Jest to węzeł szukany.

Wyszukiwanie most proving node:

    jeśli jesteśmy w węźle typu AND - wybieramy potomka o najmniejszym disproof number > 0,

    jeśli jesteśmy w węźle typu OR - wybieramy potomka o najmniejszym proof number > 0.

 

procedure ProofNumberSearch(root)

    Evaluate(root);

    SetProofAndDisproofNumbers(root);

    while root.proof ≠ 0 and root.disproof ≠ 0 and ResourcesAvailable() do

        mostProvingNode := SelectMostProving(root);

        DevelopNode(mostProvingNode);

        updateAncestors(mostProvingNode);

    od;

    if root.proof = 0 then root.value = TRUE

    elseif root.disproof = 0 then root.value = FALSE

    else root.value = UNKNOWN;

end;

Różnice pomiędzy natychmiastowym wyliczaniem, a wyliczaniem opóźnionym:

wyliczanie natychmiastowe wyliczanie opóźnione
drzewo o tym samym rozmiarze ma więcej informacji zyski przy długim wyliczaniu wartości węzła, dużej liczbie potoków

My zajmiemy się algorytmem dla wyliczania natychmiastowego, z tych powodów, że jest częściej stosowany.

Evaluate(node) - wylicza wartość węzła

GenerateAllChildren(node) - ustawia node.numberOfChildren i node.children[1..node.numberOfChildren]

ResourcesAvailable() - zwraca bool, sprawdza dostępność zasobów (pamięć, czas, etc.)

function SelectMostProving(node)

    while node.expanded do

        case node.type of

            OR:

                i:=1;

                while node.children[i].proof ≠ node.proof do i:= i+1;

            AND:

                i:=1;

                while node.children[i].disproof ≠ node.disproof do i:= i+1;

        esac;

        node := node.children[i];

    od;

    return node;

end;

procedure SetProofAndDisproofNumbers(node)

    if node.expanded then

        case node.type of

        AND:

            node.proof = ∑NεChildren(node)N.proof;

            node.disproof = MinNεChildren(node)N.disproof;

        OR:

            node.disproof = ∑NεChildren(node)N.disproof;

            node.proof = MinNεChildren(node)N.proof;

        esac;

    elseif node.evaluated then

        case node.value of

        FALSE: node.proof := ∞; node.disproof := 0;

        TRUE: node.proof := 0; node.disproof := ∞;

        UNKNOWN: node.proof := 1; node.disproof := 1;

        esac;

    else node.proof := 1; node.disproof := 1;

end;

 

procedure DevelopeNode(node)

    GenerateAllChildren(node);

    for i:=1 to node.numberOfChildren do

        Evaluate(node.children[i]);

        SetProofAndDisproofNumbers(node.children[i]);

    od;

end;

procedure UpdateAncestors(node)

    while node ≠ nil do

        SetProofAndDisproofNumbers(node);

        node := node.parent;

    od;

end;

 

Rozwinięcia

Zmniejszenie kosztów pamięciowych:

1. Usuwanie rozwiązanych poddrzew.

    Węzeł wpływa na rozwiązanie na 2 sposoby:

Tw. Rozwiązane poddrzewa nie wpływają na proces.

Dowód:

    Wszystkie nierozwiązane węzły mają:

        0 < proof < ∞

        0 < disproof < ∞

    Wszystkie rozwiązane węzły mają:

        proof = ∞ i disproof = 0

        disproof = ∞ i proof = 0

    W każdym kroku wybieramy potomka o jednym z numerów identycznym jak u rodzica - więc jeżeli byliśmy w węźle rozwiązanym to nadal w takim będziemy, jeżeli byliśmy w węźle nierozwiązanym to w takim pozostaniemy. Zaczynamy od nierozwiązanego korzenia - zatem zawsze będziemy w węzłach nierozwiązanych. Z tego wynika, że węzły rozwiązane nie leża na ścieżce o wybieranego.

    Węzeł rozwiązany albo rozwiązuje rodzica albo na niego nie wpływa:

niech A - rozwiązany węzeł, R - parent(A).

Mamy następujące przypadki:

1. A.value = TRUE

    1.1. typ R to OR - R zostaje rozwiązany

    1.2. typ R to AND i A jest ostatnim wyliczonym dzieckiem - R zostaje rozwiązany

    1.3. typ R to AND i są jeszcze nierozwiązane dzieci - rozwiązanie A nie wpływa na R

2. A.value = FALSE

    2.1. typ R to AND - R zostaje rozwiązany

    2.2. typ R to OR i A jest ostatnim wyliczonym dzieckiem - R zostaje rozwiązany

    2.3. typ R to OR i są jeszcze nierozwiązane dzieci - rozwiązanie A nie wpływa na R

Zatem rozwiązane poddrzewa nie wpływają na rozwiązanie - możemy je bezpiecznie usunąć po zaktualizowaniu rodzica.

 

2. pn2-search

    Mamy dwie funkcje:

    pn2 - jest to funkcja pn-search z ograniczoną wielkością drzewa do N. Zwraca proof i disproof (z nich wynika czy TRUE, FALSE, UNKNOWN). Po wykonaniu jego drzewo jest niszczone.

    pn1 - jest to funkcja pn-search, która przy wyliczaniu wartości proof i disproof dla węzła J korzysta z pn2 z ograniczeniem wielkości drzewa do N = wielkość drzewa z pn1.

    Rozwinięcie: przechowywanie kilku ostatnich drzew z pn2.

    Cechy algorytmu:

Badania eksperymentalne wykazały, że pn2-search przeszukuje średnio 3x więcej węzłów dla tego samego problemu.

Jeśli pn-search może rozwiązać problem dla 106 węzłów to w tej samej pamięci pn2-search może rozwiązać problem wielkości 1012.

Redukcja koniecznego czasu

W każdym obrocie pętli zaczynamy w root, dochodzimy do most_provingNode i wracamy. Nie musi tak być.

Rozwinięcie polega na tym, że:

    - jeśli proof i disproof rodzica się nie zmieniają - to już nic się nie zmienia.

    - jeśli proof i disproof rodzica się nie zmieniają - leży on na ścieżce do kolejnego most_provingNode, więc w następnym obrocie możemy od niego zacząć.

Wiedza o problemie

 Jeśli dysponujemy wiedzą umożliwiającą wcześniejsze oszacowanie proof i disproof zanim zostaną one wyliczone (przy inicjalizacji węzła) możemy odnieść z tego korzyści. Wykorzystywane są do tego następujące techniki:

1. Oszacowanie liczby potomków.

    n - liczba potomków

    Węzeł typu AND

        proof = n

        disproof = 1

    Węzeł typu OR

        proof = n

        disproof = 1

    W ten sposób przy ograniczonej wielkości drzewa badamy najpierw te, które w najmniejszy stopniu rozbudowują drzewo.

2. Oszacowanie wynikające ze specyfikacji problemu

    Dla wielu problemów istnieją cechy pozwalające określi np. liczbę ruchów możliwych jeszcze do wykonania aby gra się zakończyła (pozytywnie lub negatywnie). Tych wartości możemy użyć do określenia proof i disproof.

3. Oszacowania ze względu na głębokość węzła

    Im węzeł jest głębiej tym będzie miał większe proof i disproof. W ten sposób otrzymuje się drzewa niższe i szersze.

    Przy wykorzystaniu standardowego pn_search zdarzało się, że przy grze w szachy znajdowane było rozwiązanie w 114 ruchach gdy możliwe było w 4. To rozszerzenie pozwala tego uniknąć.

Te metody wciąż są jeszcze eksperymentalne i nie do końca zbadane. Zaburzają one założenia pn-search:

Tak więc należy się nimi posługiwać ostrożnie.

Grafy z cyklami i powtórzeniami zamiast drzew

Grafy z powtórzeniami (jeden węzeł może mieć wielu ojców) Directed Acyclic Graph - DAG

Rozwiązanie praktyczne: traktujemy graf jak zwykłe drzewo, przy poprawianiu musimy poprawić wszystkich rodziców.

Rozwiązanie to nie jest do końca poprawne (zwraca poprawny wynik, ale może coś przeoczyć), ale używane w praktyce.

Grafy z cyklami - Direct Cycling Graphs (DCG)

Takie grafy otrzymujemy, gdy mamy ruchy, które prowadzą do pozycji wcześniejszych.

Rozwiązanie: Konwertujemy graf do drzewa dzieląc węzły o wielu rodzicach na kilka, oraz zmieniając cykle na ścieżki, gdzie drugie wystąpienie tego samego wierzchołka odpowiednio wyliczamy.