On OBDDs for CNFs of Bounded Treewidth
On OBDDs for CNFs of Bounded Treewidth
复制标题
关于有界树宽 CNF 的 OBDD
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Igor Razgon
中科院分区：
文献类型：
--
作者：
Igor Razgon
在本文中，我们表明，一个CNF不能编译成一个有序的二叉决策图（OBDD）的固定参数的大小参数化的原始图树宽的CNF。因此，我们提供了一个参数化的分离OBDD和句子决策图（SDDs），这种固定参数的编译是可能的。事实上，我们证明，建议的下限也产生一个经典的（非参数化）分离OBDD和SDDs。我们还表明，最好的OBDDs现有的参数化上限，事实上持有关联图树宽参数化。
In this paper we show that a CNF cannot be compiled into an Ordered Binary Decision Diagram (OBDD) of fixed-parameter size parameterized by the primal graph treewidth of the CNF. Thus we provide a parameterized separation between OBDDs and Sentential Decision Diagrams (SDDs) for which such fixed-parameter compilation is possible. In fact, we demonstrate that the proposed lower bound also yields a classical (non-parameterized) separation of OBDDs and SDDs. We also show that the best existing parameterized upper bound for OBDDs in fact holds for incidence graph treewidth parameterization.