张 丽 王以松,2 谢仲涛 冯仁艳

1(贵州大学计算机科学与技术学院 贵阳 550025) 2(公共大数据国家重点实验室(贵州大学) 贵阳 550025) (gs.lizhang18@gzu.edu.cn)

命题可满足性问题(satisfiability problem, SAT)是计算机科学和人工智能研究的中心问题之一，在自动推理和人工智能等领域都具有非常重要的理论意义和实践价值，世界各国的相关研究人员在这方面做了大量的工作，提出了许多求解算法和大量的改进技术.

SAT问题的模型即为命题公式可满足时，使得命题公式可满足的一组真值指派中赋值为真的原子集合.当命题公式可满足时，极小模型的计算和验证问题就成了人们关注的重点问题.当命题公式不可满足时，人们通常对分析不可满足性感兴趣.极大可满足问题(maximum satisfiability problem, MaxSAT)[1-2]和极小不可满足子集(minimal unsatis-fiable subset, MUS)问题都属于这种分析.MaxSAT是SAT问题的优化版，其目标是找到一组真值指派使得CNF公式中满足(不满足)子句的数量极大化(极小化).随着MaxSAT技术的不断发展，MaxSAT问题在Android恶意软件检测[3]、排课[4]和诊断[5]等问题中都得到了很好的应用.MUS是SAT问题的扩展，是计算一个公式集的极小不可满足公式子集，其所有真子集均是可满足的.在现实中许多重要问题可以编码为MUS问题进行求解[6-8].

基于极小模型的推理一直是人工智能研究的重要主题[9-11].极小模型也是回答集程序设计(answer set programming, ASP)和其他非单调知识表示和推理范式的核心[12]，例如，限制逻辑[13-16]、缺省逻辑[17]、极小诊断[18-22].和稳定模型语义下的逻辑程序[23-24]等.极小模型主要涉及2个任务，对于一个给定的子句理论T，计算(任务1)：寻找极小模型即计算出T的一个极小模型；……