On Compiling CNFs into Structured Deterministic DNNFs
Lecture Notes in Computer Science(2015)
摘要
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.
更多查看译文
关键词
Leaf Node, Binary Tree, Dynamic Programming Algorithm, Computable Function, Conjunctive Normal Form
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要