Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):
S. Bova, F. Capelli, S. Mengel, F. Slivovsky:
"On Compiling CNFs into Structured Deterministic DNNFs";
Vortrag: International Conference on the Theory and Applications of Satisfiability Testing,
Austin, Texas;
24.09.2015
- 27.09.2015; in: "Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing",
LNCS,
9340
(2015),
ISBN: 978-3-319-24317-7;
S. 199
- 214.
Kurzfassung englisch:
We show that the traces of recently introduced dynamic programming
algorithms for #SAT can be used to construct structured
deterministic DNNF (decomposable negation normal form) representations
of propositional formulas in CNF (conjunctive normal form). This
allows us prove new upper bounds on the complexity of compiling CNF
formulas into structured deterministic DNNFs in terms of parameters
such as the treewidth and the clique-width of the incidence graph.
Elektronische Version der Publikation:
http://publik.tuwien.ac.at/files/PubDat_247936.pdf
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.