Kompilace KNF do backdoor decomposable monotone circuit
| Název práce v češtině: | Kompilace KNF do backdoor decomposable monotone circuit |
|---|---|
| Název v anglickém jazyce: | Compilation of a CNF into a backdoor decomposable monotone circuit |
| Klíčová slova: | kompilace znalostí|konjunktivní normální forma|backdoor decomposable monotone circuit|decomposable negation normal form |
| Klíčová slova anglicky: | knowledge compilation|conjunctive normal form|backdoor decomposable monotone circuit|decomposable negation normal form |
| Akademický rok vypsání: | 2020/2021 |
| Typ práce: | diplomová práce |
| Jazyk práce: | čeština |
| Ústav: | Katedra teoretické informatiky a matematické logiky (32-KTIML) |
| Vedoucí / školitel: | RNDr. Petr Kučera, Ph.D. |
| Řešitel: | skrytý - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 08.12.2020 |
| Datum zadání: | 08.12.2020 |
| Datum potvrzení stud. oddělením: | 22.12.2020 |
| Datum a čas obhajoby: | 02.09.2021 09:00 |
| Datum odevzdání elektronické podoby: | 22.07.2021 |
| Datum odevzdání tištěné podoby: | 22.07.2021 |
| Datum proběhlé obhajoby: | 02.09.2021 |
| Oponenti: | prof. RNDr. Ondřej Čepek, Ph.D. |
| Zásady pro vypracování |
| NNF je speciální typ obvodu, v němž jsou použita hradla AND, OR a vstupy jsou literály. V Decomposable NNF (DNNF) hradla AND navíc splňují podmínku "decomposability". Tato struktura byla popsána v [1]. Později bylo popsáno několik postupů a několik kompilátorů, jež překládají formuli v konjunktivní normální do DNNF. Nedávno bylo popsáno v [5] zobecnění DNNF v podobě backdoor decomposable monotone circuit (BDMC), což je struktura, která se od DNNF liší tím, že v listech (tedy vstupech) jsou formule z nějaké základní třídy.
Cílem práce je upravit postupy obvyklé při kompilaci KNF do DNNF pro kompilaci KNF do BDMC, kde jako základní třídu uvažujeme některou třídu formulí, která připouští polynomiální test splnitelnosti (skrytě hornovské, 2-CNF, monotónní). Cílem je ověřit, zda tento způsob kompilace může vést ke struktuře, která bude podstatně úspornější (ve velikosti), než DNNF vytvořená některým ze známých kompilátorů do DNNF. Součástí práce bude implementace navržených postupů a jejich experimentální ověření. |
| Seznam odborné literatury |
| [1] Darwiche, A. (1999, July). Compiling knowledge into decomposable negation normal form. In IJCAI (Vol. 99, pp. 284-289).
[2] Darwiche, A. (2004, August). New advances in compiling CNF to decomposablenegation normal form. In Proc. of ECAI (pp. 328-332). [3] J.-M. Lagniez and P. Marquis. "An Improved Decision-DNNF Compiler". Proceedings of IJCAI'17, pages 667-673. [4] Muise, C., McIlraith, S., Beck, J. C., & Hsu, E. (2010, January). Fast d-DNNF Compilation with sharpSAT. In Proceedings of the 8th AAAI Conference on Abstraction, Reformulation, and Approximation (pp. 54-60). [5] Kučera, P., & Savický, P. (2018). Backdoor Decomposable Monotone Circuits and their Propagation Complete Encodings. arXiv preprint arXiv:1811.09435. |