这篇论文提出了一种在人工智能领域中常见的、寻找子集最优解的方法，该方法利用基数最优解和子集最优解之间的关系，结合最大可满足性 (MaxSAT) 或答案集编程 (ASP) 等语言特定的限制构造来迭代计算。作者还以抽象论证框架的优先扩展计算为例来演示该方法的应用。

Dec, 2016

本研究分析了现有的基于不可满足子公式识别的最大可满足性问题（MaxSAT）算法，并提出了几个关键性优化和新的替代算法，这些优化和新算法在实际应用中的 MaxSAT 实例上提供了显着的性能提升。

Dec, 2007

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

May, 2017

本文提出了一种新的框架 UpMax，将分割过程与 MaxSAT 解决算法分离，使用户能够根据问题来提出分割方案，证明分割对于基于不可满足性的 MaxSAT 算法的性能有很大的影响。

May, 2023

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

Dec, 2019

本文提出了一种将搜索方法与半定规划方法相结合的算法，其用于解决 MAX2SAT 问题。文中称，使用这种方法能够显著提高问题的解决速度，并在一些问题上取得了 order of magnitude 级别的速度提升。

Dec, 2018

本研究使用 MaxSAT 问题中的 SPB 约束和子句权重技术，提出了一种新的局部搜索算法 SPB-MaxSAT，为 MaxSAT 局部搜索求解器的子句权重方法提供了新的视角和优秀的性能。

Jan, 2024

在具有一致性约束的动态环境中，我们研究了在基数约束下最大化单调次模函数，其在数据挖掘和机器学习中有多个应用。我们提供了在此场景中具有一致性和逼近质量之间不同权衡的算法。实验证明我们算法在真实世界实例中的有效性。

May, 2024

该研究提出了一种基于 MAX-SAT 的错误定位算法，通过符号执行，将程序的追踪记录编码为布尔可满足公式，构造出不可满足公式，并使用 MAX-SAT 找到可能的错误原因集合，其算法实现在名为 bug-assist 的工具中，并可以自动为普遍的错误类型建议修复。

Nov, 2010

该研究提出了一种基于整数规划和强化学习算法的统一框架 DCSAT，用于解决不同类型的布尔可满足性问题，包括 MaxSAT、Weighted MaxSAT、PMS 和 WPMS 等。通过调整目标函数系数，构建了统一的整数规划表示方法，并基于 0-1 整数规划构建了适当的强化学习模型。基于二叉树搜索结构，在 SAT 问题上应用了蒙特卡罗树搜索（MCTS）方法，证明了该方法能够基于维纳 - 欣钦大数定律找到所有最优的布尔赋值。实验证明，该方法能够剪枝不必要的搜索空间，找到问题的最优布尔赋值，同时为 SAT 问题的监督学习方法提供多样的标签。

Dec, 2023