- KDDGraSS: 将图神经网络与专家知识结合，用于 SAT 求解器选择
通过三分图表示的实例和异构图神经网络模型，我们提出了一种基于 GraSS 的自动 SAT 求解器选择方法，该方法使用了特定领域决策，如新的节点特征设计、图中子句的位置编码、针对三分图的 GNN 架构以及运行时间敏感的损失函数，通过广泛的实验 - 证明的最大可满足性预处理
基于 Bool 型可满足性的进展，极大可满足性已成为解决 NP 困难优化问题的可行方法，但确保 MaxSAT 求解器的正确性仍然是一个重要问题。本文介绍如何使用伪布尔型证明记录来验证广泛的现代 MaxSAT 预处理技术的正确性，通过结合 V - EduSAT: 布尔可满足性理论和应用的教学工具
EduSAT 是一个面向教育目的的教学工具，通过实现关键算法，支持学习和理解布尔可满足性和 SMT 求解技术，并提供了五个超越 SAT 和 SMT 的 NP 完全问题的求解器抽象。
- SAT 问题的机器学习：约束启发式和新的图表示
布尔可满足性 (SAT) 是一个基础的 NP-complete 问题，具有许多应用，包括自动计划和调度。为了解决大规模的情况，SAT 求解器必须依赖启发式算法，如在 DPLL 和 CDCL 求解器中选择一个分支变量。我们建议使用机器学习模型 - DeepGate2：功能感知电路表示学习
本研究提出 DeepGate2，一种新型功能感知学习框架，其使用逐对真值表之间的差异作为训练监督，并考虑电路的特性，设计了一个高效的图神经网络模型，从而在逻辑综合和布尔可满足性求解任务中表现出了显著的改进。
- 基于冲突驱动的结构学习提高 ATPG 覆盖率
该研究论文提出了一种基于冲突驱动结构学习的 ATPG 算法，该算法将现代 SAT 求解器的冲突驱动启发式方法直接应用于逻辑故障传播和激活，并在基准电路上验证了其有效性和效率。
- W2SAT: 从加权文字关系图中学习生成 SAT 实例
本文提出了一种基于 WLIG 的 SAT 公式生成框架 W2SAT，并通过实验证明了 WLIG 的优越性及其与其他方法的差异，并讨论了其在实际应用中的局限性以及可能的解决方案。
- 多智能体路径规划中，基于反例指导的抽象精炼与未经精炼的抽象
提出了一种基于 CEGAR 和 SAT 的新型多智能体路径规划求解器，该求解器在保持一些抽象不加细化的同时，需要进行后处理来修正其与正确路径规划解决方案的轻微差异，从而实现了比以前的方法更小的 SAT 编码，加快了整个求解过程，使 SAT - 蒙特卡罗森林搜索：通过强化学习实现不可满足解求解器合成
介绍了 Monte Carlo Forest Search（MCFS），它是一种用于自动合成强树搜索求解器的离线算法，用于证明给定分布的不可满足性，MCFS-SAT 是 MCFS 的一种实现，用于学习解决布尔可满足性（SAT）问题的分支策略 - 用概率方法扩展机器学习以解决组合优化问题的隐蔽博弈
应用深度学习解决困难的组合问题具有巨大的潜力。该研究侧重于布尔可满足性（SAT）问题，并通过基本的概率方法消除了由于训练集仅限于小于实际问题规模几个数量级的随机公式导致的难题。使用我们的生成器，我们对现有的最先进模型进行训练，以预测具有 1 - 推定用于布尔电路逻辑等效性检查的 SAT 编码的难度
本文研究了如何估计逻辑等价检查问题中布尔可满足性编码的困难度，提出了构建 SAT 分割以及测度困难度准确性的方法，并通过可扩展的 LEC 测试验证了这些方法可以提供有良好准确性的困难度估计。
- SATformer: 应用于 SAT 求解的 Transformer
本文提出了 SATformer，一种基于 Transformer 的布尔满足性（SAT）求解方法，实现通过学习不可满足问题实例的最小不满足核（MUC），使用图神经网络得到 CNF 中子句的嵌入表示，采用分层 Transformer 体系结构 - DeepSAT: 一种基于 EDA 驱动的 SAT 学习框架
提出了 DeepSAT 框架，使用 EDA 领域的知识来解决布尔可满足性问题（Boolean satisfiability），通过逻辑合成算法将 SAT 实例预处理为优化的与非图（AIGs），并利用 DAGNN 训练条件生成模型，在各种 S - G2SAT：学习生成 SAT 公式
本研究提出了 G2SAT 这一深度生成式框架，可以学习从输入公式集生成满足真实世界 SAT 实例特征的 SAT 公式，旨在扩展现有的数据集，为 SAT 求解器的性能提供优化方案。
- PDP: 一个通用的神经网络框架，用于学习约束满足求解器
本论文提出了一种基于图神经网络的通用框架，可用于以完全无监督的方式通过能量最小化解决 CSP 问题，并通过在图模型中传播、减少和预测的方法学习搜索策略，从而比现有的神经网络和基线模型更有效地解决 SAT 问题。
- 验证二值化深度神经网络属性
本研究提出一种使用布尔可满足性对深度神经网络的属性进行验证的严格方法，并构建了一种创建二元化神经网络布尔公式的表示方法来验证其强健性，是深度神经网络验证方面的一项重要贡献。
- 挑战 SAT 求解中分辨率限制
本文提出了一种新的问题转化方法，将 CNF 公式的决策问题转化为 Horn 公式的最大可满足性问题，并证明了在鸽笼公式的情况下 MaxSAT resolution steps 的数量存在多项式绑定。
- MMMaxSAT 的渐增式基数约束
本文介绍了一种新的方法，利用增量式计数约束来解决最大可满足性问题 (MaxSAT)。实验结果表明，与非增量式计数约束相比，该方法在性能上有显著的提高。
- 布尔可满足性问题的抽样技术
提出使用有限独立哈希的新方法来解决 boolean satisfiability 问题，并基于此方法设计了两个实用算法：一个近似均匀生成器和一个可扩展的近似模型计数器，该方法具有强大的理论保证和可扩展性，可适用于不同的应用领域。
- Erdos 离差猜想的 SAT 攻击
该研究使用布尔可满足性和状态艺术 SAT 求解器将 Erdos 偏差猜想编码，并得出一些关于它的结果。