- 编码器 - 只有 Transformer 的形式推理的计算复杂性
研究了编码器 - 只有变压器 (EOT) 的形式化推理的挑战和可能性，发现 EOT 的满足性问题 (SAT) 是不可判定的，但限定了注意力能力的量化 EOT 可以在 NEXPTIME 内解决 SAT 问题。
- 制作一个优秀的雪人是困难的
通过使用 SAT 方法解决难题视频游戏，我们证明了直接将游戏转换为 SAT 显著超过了现有的先进规划器的性能，主要原因是 SAT 能够轻松建模可达性属性，从而获得更短的解决方案。
- 基于在线动态嵌入预测的减少陈旧性的分布式 GNN 训练
SAT 是一种新颖的可扩展分布式 GNN 训练框架，通过建立包括时序图模型以预测未来嵌入的模型，有效减轻了缓存历史嵌入的陈旧问题，从而在多个大规模图数据集上实现了更好的性能和收敛速度。
- 利用一种非常简单的属性有效地推断 NFA
本文研究了基于有限状态机和重写规则的形式语法学习，提出了一种基于 SAT 求解器的 NFA 自动机规模求解方法，并验证了该方法的高效性。
- SAT 需要耗尽搜索
本文通过构造极难的 CSP（具有大域）和 SAT（具有长子句）例子，证明这些例子无法在不进行详尽搜索的情况下求解，从而得出 P≠NP 的结论，这种建设性方法对证明不可能性结果非常不同，并且缺少计算复杂性理论中当前使用的方法。
- 逻辑程序结构硬度的表征：为什么对于树宽而言，环和可达性很难？
本文介绍了一种从 SAT 到 normal ASP 的新型减少方法，并通过建立依赖图的循环长度（SCC 大小）与树宽之间所需的功能依赖性，以一种细粒度的方式刻画了硬度。
- NSNet: 一个通用的神经概率框架用于可满足性问题
介绍了一种名为 NSNet 的神经网络模型，通过使用一种新型的图神经网络 (GNN) 在潜在空间中对 BP 进行参数化，可以灵活配置以解决 SAT 和 #SAT 问题。
- 基于树宽的 ASP 到 SAT 的归约 -- ASP 普通形式难度比 SAT 高吗？
本文提出了一种新的从 ASP 到 SAT 的规约（Reduction）方法，并证明了在考虑 Treewidth 时，一般 ASP 的难度比 SAT 稍微更高，同时还对新规约进行了实证研究。
- MM更加表意与抽象的逻辑程序的配置
本篇论文重点针对模型导向人工智能的方法及其应用中 SAT 和 ASP 这两个系统的输入形式进行分析，特别是通过将输入形式重新制定和配置，优化推理过程。经过广泛领域内数据的实验证明，使用这种方法可以获得不同的优势。
- 逻辑人工智能辅助下的量子光学实验设计
本文介绍了利用逻辑人工智能（Logic AI）来设计光量子实验的方法，使用基于逻辑的算法 Klaus 将实验准备转化为满足性 (SAT) 问题，并将其与基于连续优化的最先进算法进行比较，证明逻辑 AI 明显提高了问题的解决效率，并有望在量子 - MM模态逻辑 S5 在答案集程序中的可满足性
本文用 Answer Set Programming 实现了一种更加简洁的 S5 公式求解方法，并借助可达关系确定与每个世界相关的命题原子，以此提高效率，该方法的效果与使用 SAT 求解器的方法相当。
- 基于属性缺失图的学习
本文提出了一种基于分布匹配的图神经网络 SAT，用于解决结点属性缺失情况下的图学习问题，SAT 的性能优于其它方法。
- KDD关于显著图和对抗鲁棒性
本文提出了一种基于 Saliency map 的对抗训练方法（SAT），通过使用详细的弱显著性图（如边界框和分割掩码）来改进模型的对抗鲁棒性，同时展示了如何进一步提高性能。
- AAAI对 SAT 和 CSP 两个异构类别的后门
本文在传统的强背门集和弱背门集的基础上，扩展了其概念，允许背门变量的不同实例属于不同的基类，形成异构基类。在此基础上，探讨了在 SAT 和 CSP 领域检测强背门集和弱背门集到异构基类的问题复杂度，提出检测到异构基类的背门集远比检测到同构基 - 可配置的 SAT 求解器挑战 (CSSC)
Configurable SAT Solver Competition (CSSC) compares solvers by the performance they achieved after a fully automated con - MM使用 Answer Set Programming 生成最短同步序列
检查有限自动机同步序列是否存在和找到最短同步序列是多项式时间内可解的，但是找到最短同步序列问题被称为 NP-hard 问题。本文研究了与暴力算法和基于 SAT 的方法相比，应用 Answer Set Programming 解决该优化问题的 - 有界树宽 SAT 的强背门
本文结合分解性和后门集两种方法，研究了在与给定 CNF 公式相关联的图的树宽不超过 t 的 CNF 公式集合 W_t 中找到一个小的强后门集的算法问题。我们证明了：1. 找到大小不超过 2^k 的强 W_t 后门集，或确定 F 没有大小不超 - SATzilla: 基于投资组合的 SAT 算法选择
SATzilla 是一种使用经验难度模型来构建每个实例算法组合的自动化方法，用于选择 SAT 问题的求解器，并在实验中得到了卓越的表现。
- SAT 问题的困难样例生成
本文提出了一种使用中国剩余定理将整数因子分解问题转化为 SAT 问题的算法，能够生成与 100 位整数因子分解一样难度的约 5600 变量的 SAT 实例。