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

Mar, 2000

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

Jun, 2023

论文提出了关于大规模自然问题中精确概率推断效率的新极限，尤其是给出了关于知识编译到 SDD 和 DNNF 形式的新下限，并利用 SDD 大小与最佳划分通信复杂度的关系证明了一类大型问题的 SDD 大小的指数下限。

Jun, 2015

通过使用 Davis-Putnam 算法，提出了一种算法 CDP，用于计算 CNF 或 DNF 公式的模型的准确数量，该算法的平均运行时间是 O (nm^d)，在大量的 CNF formulas 实验中的实际表现已经被估计。

Jun, 2011

决策图是一种有效表达命题公式的强大工具，本文介绍了一种通用技术将决策图应用于 SMT 级别，并可产生理论规范的 T-DD，从而解决了现有技术的一些限制。

Apr, 2024

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

Apr, 2020

本文提供了一种知识编译的角度，分析了不同的编译方法（依据目标编译语言的简洁性与语言在多项式时间内支持的查询和转换的类别），并提供了一张知识编译图使新的编译方法能在已有方法的背景下进行分析。

Jun, 2011

使用动态规划算法和代数决策图作为主要数据结构来计算布尔公式的精确文字加权模型计数，并将该方法实现在 ADDMC 中，通过在 1914 个标准模型计数基准测试中的比较，展示 ADDMC 在加权模型计数上显著优于现有最佳的求解器。

Jul, 2019

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

Sep, 2013

介绍了一种基于 SAT 求解器的算法和实现工具，用于处理大规模的 CNF 公式的近似计数问题。通过多项式调用的方式，能够高精度地估算满足条件的解数，同时针对过大的问题仍能提供高置信度的估算边界。

Jun, 2013