本文研究了用于准确计算布尔公式的确定性决策图 (d-DNNF) 表示法，将其转换为自由二叉决策图 (FBDD) 用于提供计算上限，并证明了决策 - DNNF 的指数下限，从而提高了关联概率数据库的计算效率。

Sep, 2013

本文介绍了一种名为 sentential decision diagrams (SDDs) 的表达语言，证明了在布尔函数的表示中 SDDs 比 ordered binary decision diagrams (OBDDs) 更简洁，该结论解决了知识编译中的一个开放性问题，并且在人工智能和知识编译等领域有广泛的应用。

Jan, 2016

本文提出一种新的表示语言 CCDD，并利用其支持的多项式算法在模型计数和一致采样上显著改进于目前最先进的 Decision-DNNF，SDD 和 OBDD [AND] 编译器，以及在 CNF 上开发模型计数器和一致采样器。

Feb, 2022

结构化 d-DNNF、SDD 和 OBDD 之间存在可处理性转换和简洁性差距的问题，我们通过实验证明结构化 d-DNNF 不支持多项式时间的取反、析取和存在量词操作，并且存在一些函数，其具有等价的多项式大小的结构化 d-DNNF，但没有等价的 SDD 表示。我们还通过对算术电路（AC）的研究，将这个结果推广到 PSDD 和结构化 d-DNNF 的单调 AC 类似物之间，从而展示了简洁性差距。

Feb, 2024

本文介绍了可分解否定范式（DNNF）作为可行的命题理论形式，并提供了一些在多项式时间内可以执行的强大逻辑操作。在此基础上，本文提出了将任何合取范式（CNF）转化为 DNNF 的算法，并提供其空间和时间复杂度上的结构保证。同时它也介绍了将有序二叉决策图（OBDD）表示的命题理论转换为等价的 DNNF 的线性时间算法。接着，介绍了采用新的操作在 d-DNNF 上遍历之后实现线性时间、完整的信念修正系统。

Mar, 2000

本文旨在确定哪些布尔函数可以由小型的 SDDs 表示，同时将多项式大小的布尔函数表示集合与来自 Darwiche 和 Marquis 经典知识编译地图的表示类型进行比较。最主要的结果是通过等效的不明确的非确定性 OBDDs 对 SDDs 进行准多项式仿真，回答了 SDDs 和超过 OBDDs 的 FBDDs 相对简洁性之间的一个开放问题。

Feb, 2018

本文研究了如何将一个二进制神经网络的决策函数编译成可行的表示形式，如有序二进制决策图和命题决策图，并讨论了使用这些表示形式来验证神经网络的鲁棒性和计算期望鲁棒性的方法。此外，本文还提出了一种基于伪多项式时间算法编译单个神经元的高效方法，并在手写数字数据集中展示了两个神经网络的高准确度但鲁棒性不同的案例研究。最后，实验证明使用命题决策图可以获得神经网络的紧凑表示形式。

Apr, 2020

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

Aug, 2013

该研究讨论了 #SMT 的编译策略，提出了一种基于穷尽 DPLL (T) 搜索的自上而下的编译器。

Jun, 2023

讨论了 Pearlian 结构因果模型中用于限定部分可辨识查询（如反事实推断）边界的问题，并提出了一种迭代 EM 方案，通过对初始化参数进行抽样，得到这些边界的内部近似。该方法需要对共享相同结构方程和拓扑结构、但具有不同外生概率的模型进行多次（贝叶斯网络）查询，因此将底层模型编译成算术电路具有优势，从而实现了显著的推理加速。通过单一的符号知识编译，我们展示了如何获得具有符号参数的电路结构，以在计算不同查询时将其替换为实际值。此外，我们还讨论了进一步加速边界计算的并行化技术。与标准贝叶斯网络推断相比，实验证明了明显的计算优势，加速比可达一个数量级。

Oct, 2023