Efektivní implementace DP eliminace

• Název práce v češtině: Efektivní implementace DP eliminace
• Název v anglickém jazyce: Effective implementation of DP elimination
• Klíčová slova: Davisova-Putnamova rezoluce|Konjunktivní normální forma|DP eliminace
• Klíčová slova anglicky: Davis-Putnam resolution|Conjunctive normal form|DP elimination
• Akademický rok vypsání: 2023/2024
• Typ práce: diplomová práce
• Ú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í: 31.03.2024
• Datum zadání: 01.04.2024
• Datum potvrzení stud. oddělením: 01.04.2024

Zásady pro vypracování

DP (Davis-Putnam) eliminace je postup eliminace existenčně kvantifikované proměnné z formule v konjunktivní normální formě (KNF) pomocí DP rezoluce. Eliminaci jedné proměnné lze provést v polynomiálním čase, při eliminaci více proměnných může však dojít k exponenciálnímu nárůstu velikosti formule. Cílem práce je efektivní implementace tohoto postupu s ohledem na následující aplikaci. Je dána formule v KNF, která reprezentuje podmínku na vstupních proměnných, kromě nich však obsahuje i existenčně kvantifikované pomocné proměnné. Taková formule může vzniknout například použitím Tseitinova kódování na obvod reprezentující funkci na vstupních proměnných nebo zakódováním rozhodovacího diagramu do KNF pomocí některého kódování popsaného v [3]. Naším cílem je některé nebo všechny pomocné proměnné eliminovat a získat tak formuli, která reprezentuje touž podmínku na vstupních proměnných s menším počtem pomocných proměnných nebo zcela bez nich.

Při implementaci by měly být použity efektivní datové struktury (ZBDD, [4]) pro reprezentaci množiny klauzulí s ohledem na to, že jak vstupní formule, tak formule, které vzniknou eliminací mohou být velké. Podobný postup byl použit již v článku [1], který může být použit jako výchozí bod. Cílem práce je také návrh vhodných heuristik pro výběr pořadí, v němž budou pomocné proměnné eliminovány. Během eliminace, by měla být prováděna minimalizace formule odstraňováním absorbovaných klauzulí, tedy klauzulí, které nejsou potřeba pro odvozování jednotkovou propagací ve formuli (viz též [2]). Jedním z cílů práce by mělo být experimentální ověření efektivity tohoto kroku při eliminaci.

Seznam odborné literatury

[1] Chatalic, P., & Simon, L. (2000). ZRES: The old Davis–Putnam procedure meets ZBDD. In Automated Deduction-CADE-17: 17th International Conference on Automated Deduction Pittsburgh, PA, USA, June 17-20, 2000. Proceedings 17 (pp. 449-454). Springer Berlin Heidelberg.

[2] Bordeaux, L., & Marques-Silva, J. (2012, January). Knowledge compilation with empowerment. In International Conference on Current Trends in Theory and Practice of Computer Science (pp. 612-624). Berlin, Heidelberg: Springer Berlin Heidelberg.

[3] Abío, I., Gange, G., Mayer-Eichberger, V., & Stuckey, P. J. (2016). On CNF encodings of decision diagrams. In Integration of AI and OR Techniques in Constraint Programming: 13th International Conference, CPAIOR 2016, Banff, AB, Canada, May 29-June 1, 2016, Proceedings 13 (pp. 1-17). Springer International Publishing.

[4] Minato, S. I. (2001). Zero-suppressed BDDs and their applications. International Journal on Software Tools for Technology Transfer, 3(2), 156-170.