本文提出四种算法用于提取 LTLf 规范中的不可满足核，并采用实验评估了各种算法和工具的可行性、有效性和互补性。

Mar, 2022

本研究基于 “最小不可满子集” 算法构建了一种寻找满足给定成本度量的最佳不满足子集的算法，并开发了加速解释序列生成的方法，实验证明，该算法在解释质量和计算时间方面比 “最小不可满子集” 方法更优。

Mar, 2023

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

Dec, 2007

研究多核计算及其对约束算法的影响，探究并行算法可行性、核心处理器利用、内存共享或分布式计算选择以及静态或动态分解，尝试找到最优解并提供指导给未来研究人员。

Mar, 2018

构建适用于 NP-Hard 的 Pseudo-Boolean 优化问题的任意时刻元求解器，明显提高了性能，并改进了在组合求解器组合中性能表现最好的单个求解器 Gurobi 的成功率。

Sep, 2023

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

Dec, 2016

通过构建一个与参数化规模相近的逻辑程序，将传统参数化的 argumentation framework 转化为 disjunctive logic 程序，从而找出适合的 stable model，可以直接关联到非单调逻辑推理。

Mar, 2008

研究了逻辑程序中稳定模型的最大数量问题，得到了所有逻辑程序及分离逻辑程序的最大值，且提出了一种可在 O (3^{n/3}) 的最坏情况下找到 n 个子句程序的所有稳定模型的算法。

Jan, 1999

该研究将过渡系统用于计算命题公式的模型，证明了其适用于逻辑规划和 PC（ID）逻辑中，通过计算答案集表示的模型，提供了一种统一的视角，为不同命题形式开发的解决程序提供联系。

May, 2011

本文介绍了使用改进的 NeuroSAT 架构，通过训练简化的神经网络来直接预测实际问题的不可满足核，以提供有效的指导高性能 SAT 求解器在解决特定问题分布时的问题上的应用。

Mar, 2019