Kompilace KNF do backdoor decomposable monotone circuit

• Thesis title in Czech: Kompilace KNF do backdoor decomposable monotone circuit
• Thesis title in English: Compilation of a CNF into a backdoor decomposable monotone circuit
• Key words: kompilace znalostí|konjunktivní normální forma|backdoor decomposable monotone circuit|decomposable negation normal form
• English key words: knowledge compilation|conjunctive normal form|backdoor decomposable monotone circuit|decomposable negation normal form
• Academic year of topic announcement: 2020/2021
• Thesis type: diploma thesis
• Thesis language: čeština
• Department: Department of Theoretical Computer Science and Mathematical Logic (32-KTIML)
• Supervisor: RNDr. Petr Kučera, Ph.D.
• Author: hidden - assigned and confirmed by the Study Dept.
• Date of registration: 08.12.2020
• Date of assignment: 08.12.2020
• Confirmed by Study dept. on: 22.12.2020
• Date and time of defence: 02.09.2021 09:00
• Date of electronic submission: 22.07.2021
• Date of submission of printed version: 22.07.2021
• Date of proceeded defence: 02.09.2021
• Opponents: prof. RNDr. Ondřej Čepek, Ph.D.

Guidelines

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í.

References

[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.