文章发现适当的子句学习可以促进 CDCL 求解器的性能，但在某些情况下，此方法可能会大大降低求解过程，这主要来自 CDCL 求解器具有多峰运行时间分布。通过使用威布尔混合分布来描述这种多峰分布，得出遗忘子句在 CDCL 求解器中对于优化单元传播速度外还有其它应用的结论。

Feb, 2022

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

May, 2017

本研究展示了如何将命题演绎推广到受限伪命题逻辑（CPPL）中，这是将自然数与少量约束符号插入命题逻辑字母表并相应地调整底层语言所导致的扩展。虽然该限制被认为是不必要的，但本研究提供了一种建设性证明，证明了 CPPL 的广义演绎推理是正确而完整的。

Jun, 2023

本文提出了两种优化方法用于针对 PSL 的结构学习，一种是基于贪心搜索的算法，另一种是结合生成子句的数据驱动和针对性能的伪似然性段分段优化（PPLL）目标的算法， 在五个实际任务中的比较表明 PPLL 实现了数量级运行时加速和 AUC 增益高达 15％以上。

Jul, 2018

本文主要介绍了一种用于从有限集的正面和负面例子中学习复杂系统可解释性描述的算法，通过在 IEEE 标准时间逻辑 PSL (Property Specification Language) 中学习公式来解决此问题，并比较了与现有 LTL 学习算法的效果。

Feb, 2020

使用约束逻辑编程 (CL) 对 SQL 查询进行建模，通过关注语义属性来对数据无关的抽象层进行建模，以发现可能存在的错误。该方法使用不同的约束域，这些约束域映射到 SQL 类型，并提出它们协作以提高准确性，最终我们获得一个包括 SQL 和 Datalog 的演绎系统并在课堂上实现它，和其他方法相比，表现出巨大的优势和差异，并展示其性能数据。

Jul, 2019

布尔可满足性 (SAT) 是一个基础的 NP-complete 问题，具有许多应用，包括自动计划和调度。为了解决大规模的情况，SAT 求解器必须依赖启发式算法，如在 DPLL 和 CDCL 求解器中选择一个分支变量。我们建议使用机器学习模型来改进这些启发式算法，通过减少步数来降低运行时间，但是由于有用的模型相对较大和较慢，这通常会阻碍运行时间。我们建议首先使用训练好的机器学习模型进行几个初始步骤，然后将控制权交给经典启发式算法，这简化了 SAT 求解的冷启动，并可以减少步数和总运行时间，但需要单独决定何时将控制权交给求解器。此外，我们介绍了一种改进的 Graph-Q-SAT，专门针对从其他领域转换而来的 SAT 问题，例如开放式车间调度问题。我们通过随机和工业 SAT 问题验证了我们方法的可行性。

Jul, 2023

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

May, 2023

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

Jun, 2023

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

Feb, 2024