Riešenie odovzdávajte podľa pokynov na konci tohoto zadania do štvrtka 19.5. 23:59:59.
Toto cvičenie má bonusovú časť, za ktorú môžete získať ďalšie body.
Či ste správne vytvorili pull request si môžete overiť v tomto zozname PR pre pu12.
Súbory potrebné pre toto cvičenie si môžete stiahnuť ako jeden zip
pu12.zip.
Naprogramujte výrokovologický dokazovač založený na rezolvencii. V triede
Resolver implementujte metódy resolve a isSatisfiable.
Metóda Set<Clause> resolve(Clause a, Clause b) vráti množinu všetkých
klauzúl, ktoré môžu vzniknúť rezolvenciou klauzúl a
a b.
Metóda boolean isSatisfiable(Cnf theory) zistí pomocou rezolvencie, či je
klauzálna teória (formula v CNF) theory splniteľná.
Vieme, že teória je nesplniteľná vtt existuje jej zamietnutie (teda rezolvenčné odvodenie končiace prázdnou klauzulou). To však nehovorí, kedy môžeme zamietnutie prestať hľadať. Platí však, že teória je splniteľná, ak existuje rezolvenčné odvodenie obsahujúce celú teóriu, ktoré s každou dvojicu klauzúl obsahuje aj všetky ich rezolventy, ale neobsahuje prázdnu klauzulu.
Hodnotí sa hlavne korektnosť a čiastočne efektívnosť. Riešenia s horšou zložitosťou ako nižšie popísané „priamočiare“ riešenie môžu dostať menej bodov.
„Priamočiare“ riešenie prejde všetky dvojice klauzúl (vstupných aj rezolvent) a každú dvojicu skúsi rezolvovať na každej výrokovej premennej (atóme) z týchto klauzúl.
Jedna (ale nie jediná) z možností, ako zabezpečiť, aby sa prešli naozaj naozaj všetky dvojice, je prechádzať klauzuly v poradí, ako boli pridávané, a skúšať ich rezolvovať vždy so všetkými, ktoré boli pridané / spracované pred nimi.
Treba si tiež dať pozor na „zacyklenie“ a nepridávať rezolventy, ktoré sa už
vyskytli na vstupe alebo vznikli skôr.
Napríklad (a -a) a (a) sa rezolvujú znovu na (a).
Na plný počet bodov treba nájsť rozumnejšie riešenie ako zakaždým prechádzať
zoznamom všetkých klauzúl, aby sme zistili, či ju už nemáme.
Rezolvovať klauzuly na konkrétnej premennej sa dá lineárne od ich veľkosti. Keď sú klauzuly reprezentované ako množiny literálov, tak sa v lineárnom čase dá zistiť aj to, podľa ktorých premenných sa dajú rezolvovať (aj keď pre utriedené množiny treba trošku iný prístup ako pre hashované). Množinová reprezentácia klauzúl eliminuje potrebu pravidla idempotencie. Pripravili sme vám základné triedy tejto reprezentácie v C++ a Jave (technické detaily nižšie).
Krátky popis rezolvencie na wikipédii alebo v prvej kapitole Handbook of Knowledge Representation (časť 1.3.1.).
Riešenie odovzdajte do vetvy pu12 v adresári prakticke/pu12.
Odovzdávajte (modifikujte) súbor(y)
Resolver.cpp/.h.
Program ResolverTest.cpp musí korektne
zbehnúť s vašou knižnicou.
Použite reprezentáciu literálov a množinové reprezentácie klauzúl a CNF
z modulu Cnf.h/.cpp.
Odovzdávajte (modifikujte) súbor Resolver.java.
Program ResolverTest.java musí korektne
zbehnúť s vašou knižnicou.
Použite reprezentáciu literálov a množinové reprezentácie klauzúl a CNF
z modulu Cnf.java.
Uvedené „priamočiare“ riešenie nevyhľadáva rezolvovateľné dvojice klauzúl veľmi efektívnym spôsobom, ani sa obzvlášť nezaujíma o poradie rezolvovania.
Ak implementujete nejakú efektívnejšiu (vzhľadom na čas behu) metódu výberu alebo usporiadania rezolvovaných dvojíc klauzúl, uveďte to v pull requeste s krátkym popisom vášho algoritmu (odkaz na nejaký internetový zdroj je OK, implementácia ale musí byť vaša vlastná) a môžete získať až 2 bonusové body.