提出可高效编译为d-DNNF的约束类，突破CNF限制。
Compilation and Fast Model Counting beyond CNF
- 基于输入约束的关联树宽参数化，实现固定参数可追踪编译
- 对常数宽度有序二叉决策图表示的约束，可在单指数时间内编译
- 适用于逻辑约束模型计数，尤其适合处理奇偶与基数约束
确定性分解否定正则形式（d-DNNF）电路能实现线性时间模型计数。本文深化了对哪些布尔函数可被高效编译为d-DNNF的理论理解。主要贡献是：针对以关联树宽为参数的特定约束合取，实现了固定参数可追踪（FPT）编译，该结果推广了已知的CNF情形。这些约束均为对所有变量排序下可用常数宽度有序二叉决策图（OBDD）表示的函数，例如奇偶约束和常数阈值的基数约束。该编译算法的运行时间为关联树宽的单指数级，但指数中隐藏较大常数。为平衡效率，本文还提出了一个更高效的FPT模型计数算法，适用于上述约束的一个子类，且无需预先编译。
原文摘要 · Abstract (English)
Circuits in deterministic decomposable negation normal form (d-DNNF) are representations of Boolean functions that enable linear-time model counting. This paper strengthens our theoretical knowledge of what classes of functions can be efficiently transformed, or compiled, into d-DNNF. Our main contribution is the fixed-parameter tractable (FPT) compilation of conjunctions of specific constraints parameterized by incidence treewidth. This subsumes the known result for CNF. The constraints in question are all functions representable by constant-width ordered binary decision diagrams (OBDDs) for all variable orderings. For instance, this includes parity constraints and cardinality constraints with constant threshold. The running time of the FPT compilation is singly exponential in the incidence treewidth but hides large constants in the exponent. To balance that, we give a more efficient FPT algorithm for model counting that applies to a sub-family of the constraints and does not require compilation.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。