Aug, 2013

关于有界树宽的 CNFs 的 OBDDs

TL;DR本文表明,CNF 无法被编译成由原始图树宽参数化的固定参数大小的有序二元决策图(OBDD)。因此,我们为 OBDD 和 SDD 提供了参数化分离,并证明了所提出的下界还可以产生 OBDD 和 SDD 的古典(非参数化)分离。此外,我们还展示了对于 OBDD 的现有的最佳参数化上界实际上适用于关联图树宽参数化。