arXiv:2502.00434v1 类型: cross 摘要: 确定性可分解否定范式 (d-DNNF) 电路是布尔函数的表示，能够实现线性时间模型计数。本文加强了我们对哪些类别的函数可以被有效地转换或编译为 d-DNNF 的理论知识。我们的主要贡献是在 incidence treewidth 参数化的情况下，对特定约束的合取进行固定参数可处理 (FPT) 编译。这涵盖了已知的 CNF 结果。所涉及的约束是所有变量排列下都可以由恒定宽度的有序二元决策图 (OBDD) 表示的所有函数。例如，这包括模算术约束和具有恒定阈值的基数约束。FPT 编译的运行时间在 incidence treewidth 上呈单变量指数增长，但指数中的常数很大。为了平衡这一点，我们提供了一种更高效的 FPT 模型计数算法，适用于约束的子类别，并不需要编译。