Talks and Poster Presentations (with Proceedings-Entry):
S. Bova, F. Capelli, S. Mengel, F. Slivovsky:
"On Compiling CNFs into Structured Deterministic DNNFs";
Talk: International Conference on the Theory and Applications of Satisfiability Testing,
- 2015-09-27; in: "Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing",
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.
Electronic version of the publication:
Created from the Publication Database of the Vienna University of Technology.