Iti0210lab72

Resolutsioonimeetod

Sissejuhatus

ekraanitõmmis: MobyGames

Teeme resolutsioonimeetodil loogika järeldusmootori. Rakendame seda Minesweeper mängus järelduste tegemiseks - tõestame, kas mingi peidetud ruudu all on miin või ei ole.

Resolutsioonimeetod eeldab konjunktiivsel normaalkujul (KNK, i.k. CNF) sisendit. Leiame viisi, kuidas Minesweeperi mängulaua osa CNF kujul esitada ning implementeerime resolutsiooni algoritmi, mis on pisut optimeeritud võrreldes õpiku kirjeldusega. Tööpõhimõttest aru saamiseks tasub lugeda ka õpiku kirjeldust ([AIMA] Figure 7.12 ja juuresolev jutt).

Minesweeper CNF kujul

Kasutame väikeseid 3x3, 3x4 jne miinivälju. Numbritega ruudud ütlevad, kui palju miine kokku naaberruutudes on, sealhulgas erinevalt arvutimängust kasutame ka numbrit 0. Tühjad ruudud (tähistame nad loetavuse huvides .) on peidetud, ehk pole öeldud, kas seal on miin või ei ole. Osade ülesannete puhul on märgiga ? tähistatud ruudud, mille kohta tuleks leida, kas seal on miin või mitte.

  1 1 0
  . . .
  . . .

Konjunktiivsel normaalkujul miinivälja esituse leidmiseks vaatame veel väiksemat näidet:

  2 .
  . .

Tähistame peidetud ruudud kokkuleppeliselt x1, x2 ja x3. Kuna meil on kolm peidetud ruutu ja lahtise ruudu kohta teame, et selle kõrval on täpselt kaks miini, siis peab olema üks peidetud ruutudest tühi. Seda võime loogikas kirjeldada järgmiselt: (x1 & x2 & -x3) v (x1 & -x2 & x3) v (-x1 & x2 & x3).

See esitus on hästi loetav ja arusaadav, aga kahjuks on tegu disjunktiivse normaalkujuga. Üldjuhul on selle teisendamine CNF-iks natuke tülikas, aga meie saame suht lihtsalt hakkama: vaata seda kalkulaatorit, kus vaikimisi on juba ees kolme muutuja loogikafunktsioon. Märgi funktsiooni väärtus '1'-ks igal pool, kus kolmest kaks muutujat on tõesed ja '0'-ks ülejäänud ridadel. DNF veerus peab nüüd olema sama avaldis mille juba leidsime, aga kõrval näeme, et read, kus funktsiooni väärtus on '0', annavad meile CNF kuju.

Seega, iga nähtava välja kohta, kus on väärtus m ja millel on n peidetud naaberruutu, saame genereerida otse CNF kuju, kui vaatame n muutujaga loogikafunktsiooni parameetrite väärtustusi, kus on m-ist erinev arv tõeseid parameetreid.

Sisendandmete genereerimine

Loogikalause literaale võib programmis esitada numbritega 1,2,3.. ja negatiivseid literaale -1,-2,-3.. jne. Literaalid moodustavad disjunkti (clause) ja need omakorda lause, mida võime esitada listi-taoliste andmestruktuuridega. Eelmise näite CNF võiks välja näha nii: [(1,2,3), (1,2,-3), (1,-2,3), (-1,2,3), (-1,-2,-3)]. Kuidas kõige mugavam on miinivälja ruute ja numbreid vastavusse seada, otsusta ise.

Mitme ruudu kohta info kokku kombineerimine käib sarnaselt. Kuna "teadmusbaas" (KB) on meil alati erinevate teadmiste konjunktsioon ja leitud lausetes disjunktide vahel ka "ja" sümbolid, siis need laused võib lihtsalt üksteise otsa liita (assotsiatiivsuse reegel). Peale seda oleks mõtekas korduvad disjunktid ära kustutada.

Kuidas genereerida disjunktide jaoks n Boole'i muutuja väärtustusi, nii et kindel arv muutujaid oleks tõesed? Üks viis on loendada numbreid kuni 2**n - 1. Binaarkujul annavad need numbrid kõik vajalikud kombinatsioonid, millest tuleb sobivad välja valida. Teine variant on kasutada rekursiivset funktsiooni.

CNF genereerimise näide

Algoritm

Implementeeri järgnev algoritm. Põhimõte on sama mis õpikus, resolutsioonireegli rakendamine disjunktidele paarikaupa, siis paarikaupa tekkinud uute disjunktidega ning uutele disjunktidele omavahel jne. Algoritm lõpetab kahel juhul - kui vastuolu leitakse, või kui uusi disjunkte ei õnnestu genereerida.

Pseudokood

Resolution_with_subsumption(clauses, alpha) {
    Candidates:= clauses U (not alpha)  // append negation of alpha to candidates
    Processed:= Empty list

    while Candidates is not empty {
next candidate:
        Next:= Candidates.pop() // remove from list
        foreach p in Processed {
            if p subsumes Next { // literals in p are a subset of Next
                go to next candidate
            }
        }

        foreach p in Processed {
            Resolvents:= resolve(Next, p)
            foreach r in Resolvents {
                if r is the empty clause {
                    return True
                }
                Candidates.push(r)  // append resolvents to candidates
            }
        }
        Processed.push(Next) // we're done with this clause
    }
    return False   // alpha is not entailed by clauses
}

Algoritm kasutab järgnevat optimisatsiooni: kui meil on disjunktid A v B v C v D ja A v B v C siis neist esimese võib ära jätta - miks, seda saab hästi aru lühema näite pealt: a & (a v b) on ekvivalentne a-ga. Resolutsioonimeetodi kontekstis nimetatakse seda tehnikat forward subsumption, ehk neeldumine.

resolve funktsioon annab tagasi kõik võimalikud resolutsioonireegli rakendamise tulemused disjunktide C1 ja C2 puhul (neid võib olla mitu või ka mitte ühtegi).

Funktsiooni prototüüp võiks olla midagi sellist:

 def resolution(kb, alpha):
    # kb - teadmusbaas CNF kujul
    # alpha - literaal, mida tahame kontrollida.

Oletame, et meid huvitab ruut indeksiga 12. Siis päring positiivse literaaliga (x12 sümboolsel kujul, 12 kui kasutad numbrilist esitust) küsib, kas järeldub, et sellel ruudul on miin. Päring negatiivse literaaliga (-x12 või -12) küsib vastupidi, kas miini ei ole.

Ülesanded ('?' on tähistatud väljad, mille kohta võiks küsimusi küsida).

1 1 0       0 0 0 .      ? . . . 0
? 1 ?       1 2 1 1      . 4 2 1 .
1 1 0       . . ? .      . 2 0 0 .

Algoritmi kiirendamine

Resolutsioonireegli produktid, mis on tautoloogiad (esineb sama muutuja positiivse ja negatiivse literaalina), võib kohe ära visata.

Veel üks lihtsalt rakendatav nipp proovimiseks: sorteeri alguses kandidaatide list, nii et lühemad disjunktid läheksid enne kasutusse.