FourierSAT 是一种基于布尔函数的傅里叶分析的不完全的 SAT 求解器，其提出一种用于解决具有不同类型限制的系统的代数框架，并通过实验证明在某些基准测试上，它比其他解算器更具鲁棒性。

Dec, 2019

本文提出了一种基于 WLIG 的 SAT 公式生成框架 W2SAT，并通过实验证明了 WLIG 的优越性及其与其他方法的差异，并讨论了其在实际应用中的局限性以及可能的解决方案。

Feb, 2023

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

Jun, 2023

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

May, 2017

提出了一个基于给定句子算法的自动定理证明器的新的内部指导方法，该方法使用先前证明中的正负例影响未处理子句的选择。为此，提出了一种基于幺半群结构的类型广义标签出现次数的朴素贝叶斯分类的有效方案。将这种方法在高阶逻辑证明器 Satallax 中完成，证明了该方案比不具有内部指导的 Satallax 可以解决更多问题，能够扩展现有的快速分类器。在 Flyspeck 项目的一个简单类型的高阶逻辑版本上评估了我们的方法，在没有内部指导的 Satallax 不能解决的 26% 的问题上可以解决。

May, 2016

本文提出了一种非常通用的方法来学习因果模型的结构，该方法基于从任何给定的重叠的被动观察或实验性数据集获得的 d - 分离约束。此方法允许直接循环（反馈回路）和潜在变量的存在。我们的方法基于因果路径的逻辑表示，允许将相当通用的背景知识集成，推理是使用布尔满足（SAT）求解器执行的。该过程是完整的，因为它用尽了关于是否可以确定存在或不存在任何给定边缘的可用信息，否则返回 “未知”。许多现有的基于约束的因果发现算法可以看作是特殊情况，适用于一个或多个限制性假设的情况。模拟说明了这些假设对发现的影响以及现有算法的扩展能力。

Sep, 2013

提出一种基于连续局部搜索与信念传播结合的算法 GradSAT，能在求解混合布尔约束问题方面有很好的应用表现，对称布尔约束和小系数伪布尔约束也可适用，并有望成为解决布尔满足性和优化问题的有效方法之一。

Dec, 2020

提出了 DeepSAT 框架，使用 EDA 领域的知识来解决布尔可满足性问题（Boolean satisfiability），通过逻辑合成算法将 SAT 实例预处理为优化的与非图（AIGs），并利用 DAGNN 训练条件生成模型，在各种 SAT 实例上实现了显著的准确度提高。

May, 2022

通过三分图表示的实例和异构图神经网络模型，我们提出了一种基于 GraSS 的自动 SAT 求解器选择方法，该方法使用了特定领域决策，如新的节点特征设计、图中子句的位置编码、针对三分图的 GNN 架构以及运行时间敏感的损失函数，通过广泛的实验，我们证明了这种组合对于七种最先进的求解器来说在回路设计基准测试和 2022 SAT 大赛 20 年纪念赛道的实例中都能提高运行时间。

May, 2024

该研究论文提出了一种基于冲突驱动结构学习的 ATPG 算法，该算法将现代 SAT 求解器的冲突驱动启发式方法直接应用于逻辑故障传播和激活，并在基准电路上验证了其有效性和效率。

Mar, 2023