Iti0210lab73

Resolutsioonimeetod

Sissejuhatus

Teeme resolutsioonimeetodit ja lausearvutust kasutades järeldusi kollimaailma kohta. Kollimaailm on kirjeldatud õpikus [AIMA] 7.2.

Vaatame mingit kindlat ajahetke nagu näiteks joonisel:

Kirjeldame, mida teame sellel ajahetkel:

• reeglid, mis kirjeldavad, kuidas kollimaailm töötab
• faktid, mis kirjeldavad, mida me teame seni nähtud ruutude kohta.

Lisaks tuleb programmeerida loogikamootor, mis selle põhjal järeldab, kas mingis ruudus on või ei ole midagi ohtlikku, näiteks sügav auk.

Lihtne resolutsioonil põhinev tõestaja

Teadaolevate faktide (KB) pealt mingi lause alpha tõestamiseks piisab, kui näidata et KB & -alpha on vastuolu, ehk siis ei ole võimalik korraga väita, et KB kehtib ja alpha ei kehti. Lihtne algoritmi prototüüp selleks:

def simple_resolution_solver(KB, neg_alpha):
    # KB: list of known clauses
    #           clause example: a v b v -c v d
    #           choose your own representation, e.g. ("a", "b", "-c", "d")
    # neg_alpha: query clause, already negated
    # returns True if proof found, False otherwise

    # initialize
    todo = [neg_alpha]
    done = KB.copy()

    # process the todo list one by one
    while todo:
        current = todo.pop()

        # combine current clause with all clauses we've already seen
        for clause in done:
            # apply resolution rule
            resolvents = resolve(current, clause)
            # handle new clauses generated by the resolution rule
            for resolvent in resolvents:
                # some important things that can happen here:
                # 1. resolvent is empty: proof found that KB->alpha!
                # 2. resolvent is always true: throw it away, useless clause
                # ONLY if neither of these things happen:
                    todo.append(resolvent)

        # we're done with this clause
        done.append(current)

    # loop ended without proof
    return False

Funktsioon resolve(current, clause) peab tagastama listi võimalikest tulemustest, mida saadakse kahele disjunktile current ja clause resolutsioonireegli rakendamisel. See funktsioon kirjuta ise.

Katsetame seda algoritmi väikese ülesande peal:

  P -> Q
  L & M -> P
  B & L -> M
  A & P -> L
  A & B -> L
  A
  B

Tõesta, et nende reeglite ja faktide pealt järeldub Q. Selleks pead reeglid kõigepealt CNF kujule viima, näiteks L & M -> P teisendub -L v -M v P. Funktsioonile pead tõestatava asja ette andma eitusena (-Q).

Teooria: ANL loop, set of support

Toodud algoritm on küll lihtne, aga sisaldab juba õpiku kirjeldusega võrreldes olulisi optimisatsioone:

1. "ANL loop" on algoritm, kus disjunktid jaotatakse "tegemata" ja "tehtud" listideks. Disjunkte võetakse ükshaaval tegemata listist ning proovitakse resolutsioonireeglit selle ja kõigi tehtud listi disjunktide vahel. Tekkinud uued disjunktid lisatakse tegemata listi. See garanteerib, et sama paari ei vaadata mitu korda.
2. Set of support strateegia: kuna meil on eesmärgiks mingi fakti järeldumist kontrollida, siis see strateegia paneb "tegemata" listi ainult kontrollitava fakti ja "tehtud" listi kogu ülejäänud teadmise. Tegemata listi hakkavad siis tekkima ainult asjad, mis on kuidagi seotud meie kontrollitava faktiga. Näiteks, testülesande puhul on tegemata listis -Q ja kõik faktid tehtud listis, esimeses tsüklis tekiks kohe -P mis tähendab, et Q tõestamiseks peame esmalt tõestama P. Järgmisena leitakse P eeldused jne - see on väga sarnane backward chaining algoritmiga.

Optimeeritud variant

Esialgne variant järeldusmootorist küll töötab, aga kui ta kohe järeldust ei leia, hakkab resolutsioonireegel piiramatult uusi disjunkte genereerima - proovi näiteks eemaldada testülesandest Q tõestamiseks vajalik fakt A ja vaata mis juhtub.

Lisame neeldumise kontrolli. Lihtsustatult öeldes kontrollitakse iga resolutsioonireegli poolt genereeritud disjunkti juures, kas oli juba enne olemas mingi disjunkt, mis sisaldab sama infot.

def resolution_solver(KB, neg_alpha):
    # KB: list of known clauses
    #           clause example: a v b v -c v d
    #           choose your own representation, e.g. ("a", "b", "-c", "d")
    # neg_alpha: query clause, already negated
    # returns True if proof found, False otherwise

    # initialize
    todo = [neg_alpha]
    done = KB.copy()

    # process the todo list one by one
    while todo:
        current = todo.pop()

        # check if current is redundant
        for clause in done + todo:
            # if clause is a subset of current, then go back to the start of the loop
            # to pick new current

        # combine current clause with all clauses we've already seen
        for clause in done:
            # apply resolution rule
            resolvents = resolve(current, clause)
            # handle new clauses generated by the resolution rule
            for resolvent in resolvents:
                # some important things that can happen here:
                # 1. resolvent is empty: proof found that KB->alpha!
                # 2. resolvent is always true: throw it away, useless clause
                # ONLY if neither of these things happen:
                    todo.append(resolvent)

        # we're done with this clause
        done.append(current)

    # loop ended without proof
    return False

Nüüd peaks algoritm kiiresti tulemusi andma, kui tõestust ei leita. Proovi jälle testülesannet, eemaldades fakti A või vajaliku reegli A & B -> L.

Teooria: neeldumine

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 subsumption, ehk neeldumine. Kui kontrollime neeldumist nii, et leiame kas üks disjunkt on teise alamhulk, siis sellega leitakse ka korduvad disjunktid.

Teadmusbaasi sisu

Resolutsioonimeetod eeldab konjunktiivsel normaalkujul (KNK, i.k. CNF) sisendit.

Reeglid

Kollimaailma reeglid ütlevad, et kui ruudus on tuuletõmbus, siis vähemalt ühes naaberruudus on sügav auk. Kolli hais tähendab aga, et vähemalt ühes naaberruudus on koll. Tegelikult peaks kollimaailmas olema täpselt üks koll, aga lihtsuse mõttes lubame siin, et kolle võib olla ka mitu või mitte ühtegi.

Tuuletõmbuse/augu reegli näide ruudu (2,2) kohta:

B₂₂ <=> (P₁₂ v P₂₁ v P₂₃ v P₃₂)

Kolli reeglid on analoogsed. Mõistlik on teadmusbaas genereerida juba disjunktide kujul - vaata, millisteks disjunktideks selline reegel teisendub. Tee funktsioon, mis genereerib vajalikud disjunktid iga ruudu kohta (1,1) - (4,4).

Faktid

Fakte teame me kollimaailma läbi käidud osa kohta. Näiteks, kui meil on ruudus (1,1) tuuletõmbus, siis seda esitab fakt B₁₁. Oletame, et kolli haisu pole, seda esitab fakt -S₁₁. Ära unusta, et vaikimisi ei kehti lausearvutusloogikas mitte midagi. Kui me oleme näinud tühja ruutu, siis tuleb ka loogikamootorile öelda, et seal ei ole tuuletõmbust, kolli haisu, auku ega kolli.

Ülesanne lahendamiseks

Paksu joonega ümbritsetud ala on juba läbi käidud. B tähistab tuuletõmbust, S haisu. Tee vajalike reeglite ja faktidega teadmusbaas. Proovi resolution_solver() meetodiga tuvastada, kas ?-ga tähistatud ruudud on turvalised - selleks peaks tõestama, et seal on (või ei ole) koll või sügav auk.

Lisaülesanne

Mõtle, mis reegleid oleks lisaks vaja, kui:

1. Ruudustikus on maksimaalselt üks koll
2. Ruudustikus on täpselt üks koll

Võid seda ka algoritmiga järgi proovida. Reegel, et ruudustikus on täpselt üks koll peaks võimaldama ülesandes ruudu (3,4) turvalisust kontrollida.