Efektivní implementace DP eliminace
| Thesis title in Czech: | Efektivní implementace DP eliminace |
|---|---|
| Thesis title in English: | Effective implementation of DP elimination |
| Key words: | Davisova-Putnamova rezoluce|Konjunktivní normální forma|DP eliminace |
| English key words: | Davis-Putnam resolution|Conjunctive normal form|DP elimination |
| Academic year of topic announcement: | 2023/2024 |
| Thesis type: | diploma thesis |
| Thesis language: | |
| 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: | 31.03.2024 |
| Date of assignment: | 01.04.2024 |
| Confirmed by Study dept. on: | 01.04.2024 |
| Guidelines |
| 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. |
| References |
| [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. |