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

Mar, 2000

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

Feb, 2022

本文介绍了用于解决量化扩展逻辑编程中的第二级推理任务的算法框架 Second Level Algebraic Model Counting (2AMC)，探讨了使用知识编译技术降低处理效率时的需要考虑变量阶数限制问题，进一步提出并实现了一种静态生成约束的策略，并在多个任务和基准测试上评估了有效性。

May, 2022

研究随机 k-CNF 公式的规模和编译时间行为，以及使用知识编译进行的大小和运行时行为的严格实证研究和分析，类似于 SAT / CSP 社区对相变行为的早期研究，我们鉴定了不同参数方面的有趣行为：子句密度和解密度，并总结我们的经验研究。

Jul, 2020

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

Jun, 2011

本篇论文介绍了一种从 SMT 到 #SMT 近似版本的约简方法，并提出了关于整数算术和线性实数算术的模型计数算法，通过对现代 SMT 求解器的高级启发式算法进行利用，运行时间为多项式级别并提供正式边界。我们使用这些算法来解决带有非确定性的无循环概率程序模型的值问题。

Nov, 2014

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

Jun, 2015

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

Jun, 2011

本研究提出了单调理论的概念，并展示了如何为这样的理论构建有效的 SMT（SAT 模块理论）求解器，包括有效的理论传播和子句学习。我们应用这些求解器解决过程内容生成问题，与基于 SAT 或 Answer Set Programming 的最先进方法相比，显著提高了求解速度并轻松解决了以往难以解决的一些问题。

May, 2014

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

Jun, 2013