知识汇编、广度与量化
Knowledge Compilation, Width and Quantification
摘要：
在量化布尔公式（QBF）的背景下，我们推广了关于SAT和#SAT在有界树宽CNF-公式上的易处理性的许多结果。为此，我们从研究OBDD的宽度概念开始，并观察到OBDD中存在或普遍投影一个变量块时大小的爆炸只影响其宽度。然后，我们将宽度的概念推广到结构化（确定性）DNNF的更一般的表示，并给出了一个类似的算法来存在或普遍投影一个变量块。使用一个众所周知的算法转换有界树宽CNF公式到确定性DNNF，我们能够将这种连接推广到量化CNF，这给了我们一个副产品，人们可以在FPT时间内计算有界树宽和有界量词交替量化CNF的模型数量。我们也给出了一个广泛的研究有界宽度d-DNNF，并证明了我们的几个结果的最优性。
英文摘要：
We generalize many results concerning the tractability of SAT and #SAT on bounded treewidth CNF-formula in the context of Quantified Boolean Formulas (QBF). To this end, we start by studying the notion of width for OBDD and observe that the blow up in size while existentially or universally projecting a block of variables in an OBDD only affects its width. We then generalize this notion of width to the more general representation of structured (deterministic) DNNF and give a similar algorithm to existentially or universally project a block of variables. Using a well-known algorithm transforming bounded treewidth CNF formula into deterministic DNNF, we are able to generalize this connection to quantified CNF which gives us as a byproduct that one can count the number of models of a bounded treewidth and bounded quantifier alternation quantified CNF in FPT time. We also give an extensive study of bounded width d-DNNF and proves the optimality of several of our results.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
