本文通过分析阐述了布尔可满足性问题中，采用了子句学习增强 DPLL 的实现方式是最高效的，并与已有的分辨规则证明体系相对照，证明了该方法在一些条件下可以提供更短的证明过程，且该算法可以通过利用问题结构，通过导向学习算法的方法取得指数性的加速。

Jun, 2011

通过嵌入特定领域的启发式方法来提高 CDCL 算法的性能并不容易，本文提出了一种通用框架来设计和实现新的启发式方法，并在两个工业领域实验中取得成功。

Nov, 2016

本文提出了一种新的问题转化方法，将 CNF 公式的决策问题转化为 Horn 公式的最大可满足性问题，并证明了在鸽笼公式的情况下 MaxSAT resolution steps 的数量存在多项式绑定。

May, 2017

通过扩展冲突驱动子句学习技术，本文使用基于整数线性规划方法处理复杂的实际问题，并讨论该方法在优化方面的潜在改进。

Feb, 2024

本文介绍了使用因果推理探究 SAT 求解器内在工作机制的方法 CausalSAT，并通过实验验证了其中四条经验法则和三个与现代 SAT 求解器实现密切相关的问题。

Jun, 2023

提出了基于冲突驱动子句学习算法的新型神经网络验证框架 DeepCDCL，通过引入异步子句学习和管理结构，与直接应用 CDCL 框架相比，减少了冗余的时间消耗。同时，在 ACAS Xu 和 MNIST 数据集上对我们的方法的性能进行了详细评估，显示在大多数情况下实现了显著加速。

Mar, 2024

本文提出了一种基于冲突驱动约束学习（CDCL）的方法，通过智能管理学习到的约束条件来有效地更新流推理算法的遗留解决方案，研究了强化学习在连续评估先前计算的约束条件的实用性，并在真实世界的重构问题上取得了显着的性能提升，为流推理场景提供了新的解决思路。

Aug, 2020

该研究提出一种新的冲突驱动程序合成技术，并介绍了冲突的等价性模块以及学习如何规避类似问题的可用引理，该技术的性能实验证明优于两个针对数据整理和函数式编程的最先进的合成工具。

Nov, 2017

研究表明，类增量学习 (CIL) 的问题可以分解为两个子问题：任务内预测 (WP) 和任务 ID 预测 (TP)，其中 TP 与分布外检测 (OOD) 相关联。该研究的关键结论是，无论是否通过 CIL 算法显式或隐式定义 WP 和 TP 或 OOD 检测，优秀的 WP 和 TP 或 OOD 检测都对于良好的 CIL 表现是必要且充分的，其中 TIL 就是 WP。基于理论结果，还设计了新的 CIL 方法，其在 CIL 和 TIL 两个设置中性能均优于强基线。

Nov, 2022

通过固定减少顺序，基于超前法逻辑来推导非冗余子句，本研究展示了 SCL (FOL) 可以模拟无相等符号的一阶逻辑。我们建立一个地面部分模型，根据固定的顺序来执行基于超前法的推理，其中假面积分的最小 false 地面实例触发非冗余超级位置推论。我们定义了 SCL 计算的相应策略，使得由 SCL 学习的子句和超前法推论的子句重合。从这个角度来看，SCL 计算可以被看作是超前法计算的一般化。

May, 2023