第8卷第6期 智能系统学报 Vol.8 No.6 2013年12月 CAAI Transactions on Intelligent Systems Dec.2013 D0:10.3969/j.issn.1673-4785.201212058 网络出版地址：http://www.cnki.net/kcms/detail/23.1538.TP.20131012.1813.002.html 不可满足子式研究 般明浩，李欣 (东北师范大学计算机科学与信息技术学院，吉林长春130117) 摘要：为了广泛有效地将不可满足子式应用于知识验证、产品规划、硬件和软件的设计与验证等领域，对不可满足 子式进行了相关研究对当前不可满足子式的主要相关算法进行了概述评论、分类归纳，并从计算复杂性角度介绍了 其子类、参数复杂性以及QBF中的极小不可满足子式.总结了近10年来不可满足子式的理论与算法，讨论了不可满 足子式的未来研究发展方向研究有利于进一步发现不可满足的根本原因，从而进行有针对性地改进，并对相关人员 的研究提供帮助. 关键词：可满足性问题；不可满足子式；可满足模理论：局部搜索 中图分类号：TP311文献标志码：A文章编号：1673-4785(2013)06-0497-08 中文引用格式：殷明浩，李欣.不可满足子式研究[J].智能系统学报，2013,8(6)：497-504. 英文引用格式：YIN Minghao,LI Xin.Research on an unsatisfiable subformula[J].CAAI Transactions on Intelligent Systems, 2013,8(6):497-504. Research on an unsatisfiable subformula YIN Minghao,LI Xin (School of Computer Science and Information Technology,Northeast Normal University,Changchun 130117,China) Abstract:In recent years,an increasing number of researchers have started to focus their attention on unsatisfiable subformulas,especially in regards to the extremely small and the minimal unsatisfiable subformulas.The unsatisfi- able subformula (US)has a wide range of practical applications,including knowledge validation,product pro- grams,and design and verification of hardware and software.An unsatisfiable subformula may be very helpful in di- agnosing the causes of unfeasibility in large systems.In the past 10 years,research on an unsatisfiable subformula has been developed quickly.In this paper,the authors discuss the algorithm in relation to an unsatisfiable subfor- mula,introduce the subcategory of an unsatisfiable subformula from the viewpoint of calculation complexity,param- eter complexity and the research on an unsatisfiable subformula in QBF.Finally,the authors discuss the future di- rection of research on an unsatisfiable subformula. Keywords:satisfiability problem;unsatisfiable subformula;satisfiability module theory;local search 可满足性问题(satisfiability problem,SAT)是当 逻辑的可满足性是无法满足实际要求的.当公式不 前人们研究得最多的约束可满足性问题，也是当今 可满足时，为了查找不可满足的原因，往往要删除无 计算机科学和人工智能研究的核心问题.在实际应 关子句进而提取不可满足子式.目前，研究人员对不 用领域中的很多问题，例如等价性检查、大规模集成 可满足子式的算法研究和相应计算的复杂性表现出 电路的自动布线、自动测试向量生成、硬件与软件的 了极大兴趣.寻找最小不可满足子式的决策问题是 属性验证等都可转化为约束可满足问题，即能够归 ∑，-complete问题，寻找一个极小不可满足子式 约为一阶逻辑公式或命题逻辑.然而，仅仅判断命题 是D-complete问题.目前有很多算法是关于极 小21和最小不可满足子式214的提取，这些提取 收稿日期：2012-12-27.网络出版日期：2013-10-12 基金项目：国家自然科学基金资助项目(61070084,60803012) 不可满足子式的算法主要应用于形式验证领域.极 通信作者：殷明浩.E-mail:ymh@nenu.cdu.cn 小不可满足子式可以更好地解释不可满足的根源所
第 ８ 卷第 ６ 期 智 能 系 统 学 报 Ｖｏｌ．８ №．６ ２０１３ 年 １２ 月 ＣＡＡＩ Ｔｒａｎｓａｃｔｉｏｎｓ ｏｎ Ｉｎｔｅｌｌｉｇｅｎｔ Ｓｙｓｔｅｍｓ Ｄｅｃ． ２０１３ ＤＯＩ：１０．３９６９ ／ ｊ．ｉｓｓｎ．１６７３⁃４７８５．２０１２１２０５８ 网络出版地址：ｈｔｔｐ： ／ ／ ｗｗｗ．ｃｎｋｉ．ｎｅｔ ／ ｋｃｍｓ／ ｄｅｔａｉｌ ／ ２３．１５３８．ＴＰ．２０１３１０１２．１８１３．００２．ｈｔｍｌ 不可满足子式研究 殷明浩，李欣 （东北师范大学 计算机科学与信息技术学院，吉林 长春 １３０１１７） 摘 要：为了广泛有效地将不可满足子式应用于知识验证、产品规划、硬件和软件的设计与验证等领域，对不可满足 子式进行了相关研究．对当前不可满足子式的主要相关算法进行了概述评论、分类归纳，并从计算复杂性角度介绍了 其子类、参数复杂性以及 ＱＢＦ 中的极小不可满足子式．总结了近 １０ 年来不可满足子式的理论与算法，讨论了不可满 足子式的未来研究发展方向．研究有利于进一步发现不可满足的根本原因，从而进行有针对性地改进，并对相关人员 的研究提供帮助． 关键词：可满足性问题；不可满足子式；可满足模理论；局部搜索 中图分类号：ＴＰ３１１ 文献标志码：Ａ 文章编号：１６７３⁃４７８５（２０１３）０６⁃０４９７⁃０８ 中文引用格式：殷明浩，李欣． 不可满足子式研究［Ｊ］． 智能系统学报， ２０１３， ８（６）： ４９７⁃５０４． 英文引用格式：ＹＩＮ Ｍｉｎｇｈａｏ， ＬＩ Ｘｉｎ． Ｒｅｓｅａｒｃｈ ｏｎ ａｎ ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒｍｕｌａ［ Ｊ］． ＣＡＡＩ Ｔｒａｎｓａｃｔｉｏｎｓ ｏｎ Ｉｎｔｅｌｌｉｇｅｎｔ Ｓｙｓｔｅｍｓ， ２０１３， ８（６）： ４９７⁃５０４． Ｒｅｓｅａｒｃｈ ｏｎ ａｎ ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒｍｕｌａ ＹＩＮ Ｍｉｎｇｈａｏ， ＬＩ Ｘｉｎ （Ｓｃｈｏｏｌ ｏｆ Ｃｏｍｐｕｔｅｒ Ｓｃｉｅｎｃｅ ａｎｄ Ｉｎｆｏｒｍａｔｉｏｎ Ｔｅｃｈｎｏｌｏｇｙ， Ｎｏｒｔｈｅａｓｔ Ｎｏｒｍａｌ Ｕｎｉｖｅｒｓｉｔｙ， Ｃｈａｎｇｃｈｕｎ １３０１１７， Ｃｈｉｎａ） Ａｂｓｔｒａｃｔ：Ｉｎ ｒｅｃｅｎｔ ｙｅａｒｓ， ａｎ ｉｎｃｒｅａｓｉｎｇ ｎｕｍｂｅｒ ｏｆ ｒｅｓｅａｒｃｈｅｒｓ ｈａｖｅ ｓｔａｒｔｅｄ ｔｏ ｆｏｃｕｓ ｔｈｅｉｒ ａｔｔｅｎｔｉｏｎ ｏｎ ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒｍｕｌａｓ， ｅｓｐｅｃｉａｌｌｙ ｉｎ ｒｅｇａｒｄｓ ｔｏ ｔｈｅ ｅｘｔｒｅｍｅｌｙ ｓｍａｌｌ ａｎｄ ｔｈｅ ｍｉｎｉｍａｌ ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒｍｕｌａｓ． Ｔｈｅ ｕｎｓａｔｉｓｆｉ⁃ ａｂｌｅ ｓｕｂｆｏｒｍｕｌａ （ＵＳ） ｈａｓ ａ ｗｉｄｅ ｒａｎｇｅ ｏｆ ｐｒａｃｔｉｃａｌ ａｐｐｌｉｃａｔｉｏｎｓ， ｉｎｃｌｕｄｉｎｇ ｋｎｏｗｌｅｄｇｅ ｖａｌｉｄａｔｉｏｎ， ｐｒｏｄｕｃｔ ｐｒｏ⁃ ｇｒａｍｓ， ａｎｄ ｄｅｓｉｇｎ ａｎｄ ｖｅｒｉｆｉｃａｔｉｏｎ ｏｆ ｈａｒｄｗａｒｅ ａｎｄ ｓｏｆｔｗａｒｅ． Ａｎ ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒｍｕｌａ ｍａｙ ｂｅ ｖｅｒｙ ｈｅｌｐｆｕｌ ｉｎ ｄｉ⁃ ａｇｎｏｓｉｎｇ ｔｈｅ ｃａｕｓｅｓ ｏｆ ｕｎｆｅａｓｉｂｉｌｉｔｙ ｉｎ ｌａｒｇｅ ｓｙｓｔｅｍｓ． Ｉｎ ｔｈｅ ｐａｓｔ １０ ｙｅａｒｓ， ｒｅｓｅａｒｃｈ ｏｎ ａｎ ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒｍｕｌａ ｈａｓ ｂｅｅｎ ｄｅｖｅｌｏｐｅｄ ｑｕｉｃｋｌｙ． Ｉｎ ｔｈｉｓ ｐａｐｅｒ， ｔｈｅ ａｕｔｈｏｒｓ ｄｉｓｃｕｓｓ ｔｈｅ ａｌｇｏｒｉｔｈｍ ｉｎ ｒｅｌａｔｉｏｎ ｔｏ ａｎ ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒ⁃ ｍｕｌａ， ｉｎｔｒｏｄｕｃｅ ｔｈｅ ｓｕｂｃａｔｅｇｏｒｙ ｏｆ ａｎ ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒｍｕｌａ ｆｒｏｍ ｔｈｅ ｖｉｅｗｐｏｉｎｔ ｏｆ ｃａｌｃｕｌａｔｉｏｎ ｃｏｍｐｌｅｘｉｔｙ， ｐａｒａｍ⁃ ｅｔｅｒ ｃｏｍｐｌｅｘｉｔｙ ａｎｄ ｔｈｅ ｒｅｓｅａｒｃｈ ｏｎ ａｎ ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒｍｕｌａ ｉｎ ＱＢＦ． Ｆｉｎａｌｌｙ， ｔｈｅ ａｕｔｈｏｒｓ ｄｉｓｃｕｓｓ ｔｈｅ ｆｕｔｕｒｅ ｄｉ⁃ ｒｅｃｔｉｏｎ ｏｆ ｒｅｓｅａｒｃｈ ｏｎ ａｎ ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒｍｕｌａ． Ｋｅｙｗｏｒｄｓ：ｓａｔｉｓｆｉａｂｉｌｉｔｙ ｐｒｏｂｌｅｍ； ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒｍｕｌａ； ｓａｔｉｓｆｉａｂｉｌｉｔｙ ｍｏｄｕｌｅ ｔｈｅｏｒｙ； ｌｏｃａｌ ｓｅａｒｃｈ 收稿日期：２０１２⁃１２⁃２７． 网络出版日期：２０１３⁃１０⁃１２． 基金项目：国家自然科学基金资助项目（６１０７００８４，６０８０３０１２）． 通信作者：殷明浩． Ｅ⁃ｍａｉｌ： ｙｍｈ＠ ｎｅｎｕ．ｅｄｕ．ｃｎ． 可满足性问题（ｓａｔｉｓｆｉａｂｉｌｉｔｙ ｐｒｏｂｌｅｍ， ＳＡＴ）是当 前人们研究得最多的约束可满足性问题，也是当今 计算机科学和人工智能研究的核心问题．在实际应 用领域中的很多问题，例如等价性检查、大规模集成 电路的自动布线、自动测试向量生成、硬件与软件的 属性验证等都可转化为约束可满足问题，即能够归 约为一阶逻辑公式或命题逻辑．然而，仅仅判断命题 逻辑的可满足性是无法满足实际要求的．当公式不 可满足时，为了查找不可满足的原因，往往要删除无 关子句进而提取不可满足子式．目前，研究人员对不 可满足子式的算法研究和相应计算的复杂性表现出 了极大兴趣．寻找最小不可满足子式的决策问题是 ∑２ ⁃ｃｏｍｐｌｅｔｅ 问题［１］ ，寻找一个极小不可满足子式 是 Ｄ ｐ ⁃ｃｏｍｐｌｅｔｅ 问 题． 目 前 有 很 多 算 法 是 关 于 极 小［２⁃１１］和最小不可满足子式［１２⁃１４］ 的提取，这些提取 不可满足子式的算法主要应用于形式验证领域．极 小不可满足子式可以更好地解释不可满足的根源所
.498. 智能系统学报 第8卷 在，最小不可满足子式可以精确地定位错误原因，但 可满足子式，每个不可满足子式的子句数也可能不 是其求解难度极大.随着SMT(satisfiability modulo 同其中一些不可满足子式可能是其他不可满足子 heories)技术的不断发展，它开始逐渐取代SAT.相 式的子集.在最坏情况下，不可满足子式就是原始公 对于SAT,SMT具有更好的抽象能力，更接近于高层 式本身 设计，极具发展潜力.它使用字级建模，不必像SAT 定义3极小不可满足子式 那样将问题转化为位级处理，从而减少了空间和时 对于一个不可满足的公式”的一个不可满足子 间的开销.SMT可以看作是SAT问题的一个扩展， 式中，那么P是极小不可满足子式，当且仅当H中∈ 它极大地补充了SAT的不足之处.求解其极小不可 P,使得中是可满足的， 满足子式算法也极具实际意义.ST技术是近几年 定义4最小不可满足子式。 发展起来的，目前提取SMT中极小不可满足子式的 给出一个不可满足的公式φ以及φ的所有不可 算法比较少.Cimatti1s-16提出了一个新颖的方式 满足子式构成的集合{中，中2，…，中n},如果中：∈ lemma-Lif来提取SMT极小不可满足子式：张建 {中1，中2，…，中}是最小不可满子式，当且仅当 民[]提出了基于DPLL(T)的深度优先搜索的极小 中：∈{中1，中2，…，中}，1≤i≤n,使得 SMT不可满足子式求解算法DFS-MUSE和宽度优 1中1≤l中：1· 先搜索的极小SMT不可满足子式的求解算法BFS 定义5量化布尔公式-QBF问题 MUSE.2010年，他又提出了基于冲突分析与否证蕴 一个QCNF公式p=Qx1Q2x2…Qx.中，其中 含的极小SMT不可满足子式求解算法CARI- MUSE18】,该算法的效果明显好于DFS-MUSE算法， Q:∈{3，V},中是一个CNF公式，用矩阵形式表 性能随着时间复杂度的增加更加明显， 达p.x1,x2,…,x。分别被Q,Q2,…,Q。量化.有 研究不可满足子式的复杂性对不可满足子式求 时，可以简写为p=Q中。 解算法也极具重大意义.H.K.Buning和赵希顺[9对 定义6QBF极小不可满足子式(MF) 不可满足的子类进行了研究，介绍了各子类的特性， 当且仅当p是不可满足的，并且从P中移出任 并在文献中对子类的复杂性进行了证明20).H. 何一个子句将导致公式变为可满足，一个QBF公式 Fleischnet2)、S.Szeide]将固定参数的概念与极小 ”被称为极小不满足，不可满足子式的子式可以表 不可满足子式中固定差值概念相关联，证明了固定 示为MF(minimal false formulas). 参数的极小不可满足子式的计算复杂性.带量词的 定义7可满足性模理论(SMT) 布尔公式QBF作SAT公式的自然扩展具有紧凑的 SMT是SAT的一种扩展，其命题不仅包括布尔 空间结构以及更强大、更直观的表达能力，对QBF 公式，还包括其他特定理论中的一阶逻辑约束，如整 中极小不可满足子式的研究有利于探索新的QBF 数与实数算术类型、位向量、递归及数据类型等. 算法.赵希顺23]证明了QBF中，对QCNF公式固定 定义8SMT不可满足子式. 差值为1的极小不可满足子式可以在多项式时间内 给出一个不可满足的无量词一阶逻辑公式P, 有解。 当且仅当中是不可满足的，并且中二P,中是公式 p的一个SMT不可满足子式 1相关定义 定义9极小ST不可满足子式 在计算机科学领域，不可满足子式的研究最初 给出不可满足的无量词一阶逻辑公式”，及其 源于SAT问题，首先介绍本文涉及的相关概念 一个不可满足子式中，那么中是极小ST不可满足 定义1命题可满足性问题 子式，当且仅当H中∈P,使得中是可满足的 给定一个CNF表达式F和一个变量集合{V= 定义10约束可满足问题(CSP) x1,x2,x3}.如果变量集合V中的一组赋值使得表达 由一个变量集合和一个约束集合组成.问题的一 式F的值为真，那么称表达式F是可满足的：否则， 个状态是由对一些或全部变量的一个赋值定义的完 表达式F为不可满足 全赋值：每个变量都参与的赋值问题的解是满足所 定义2不可满足子式/不可满足核(US/UC). 有约束的完全赋值，或更进一步，使目标函数最大化， 对于一个公式P,中是”的一个不可满足子 定义11极小CSP不可满足子式 式，当且仅当p是不可满足的，且中二p. 一个极小CSP不可满足子式，其约束的有关子 显然，对于同一个问题实例，可能存在不同的不 集是不可满足的，并且其真子集是可满足的
在，最小不可满足子式可以精确地定位错误原因，但 是其求解难度极大． 随着 ＳＭＴ （ ｓａｔｉｓｆｉａｂｉｌｉｔｙ ｍｏｄｕｌｏ ｔｈｅｏｒｉｅｓ）技术的不断发展，它开始逐渐取代 ＳＡＴ．相 对于 ＳＡＴ，ＳＭＴ 具有更好的抽象能力，更接近于高层 设计，极具发展潜力．它使用字级建模，不必像 ＳＡＴ 那样将问题转化为位级处理，从而减少了空间和时 间的开销．ＳＭＴ 可以看作是 ＳＡＴ 问题的一个扩展， 它极大地补充了 ＳＡＴ 的不足之处．求解其极小不可 满足子式算法也极具实际意义．ＳＭＴ 技术是近几年 发展起来的，目前提取 ＳＭＴ 中极小不可满足子式的 算法比较少． Ｃｉｍａｔｔｉ ［１５⁃１６］ 提出了一个新颖的方式 ｌｅｍｍａ⁃Ｌｉｆｔ 来提取 ＳＭＴ 极小不可满足子式； 张建 民［１７］提出了基于 ＤＰＬＬ（Ｔ）的深度优先搜索的极小 ＳＭＴ 不可满足子式求解算法 ＤＦＳ⁃ＭＵＳＥ 和宽度优 先搜索的极小 ＳＭＴ 不可满足子式的求解算法 ＢＦＳ⁃ ＭＵＳＥ．２０１０ 年，他又提出了基于冲突分析与否证蕴 含的 极 小 ＳＭＴ 不 可 满 足 子 式 求 解 算 法 ＣＡＲＩ⁃ ＭＵＳＥ ［１８］ ，该算法的效果明显好于 ＤＦＳ⁃ＭＵＳＥ 算法， 性能随着时间复杂度的增加更加明显． 研究不可满足子式的复杂性对不可满足子式求 解算法也极具重大意义．Ｈ．Ｋ．Ｂüｎｉｎｇ 和赵希顺［１９］ 对 不可满足的子类进行了研究，介绍了各子类的特性， 并在文献中对子 类 的 复 杂 性 进 行 了 证 明［２０］ ． Ｈ． Ｆｌｅｉｓｃｈｎｅ ［２１］ 、Ｓ． Ｓｚｅｉｄｅ ［２２］ 将固定参数的概念与极小 不可满足子式中固定差值概念相关联，证明了固定 参数的极小不可满足子式的计算复杂性．带量词的 布尔公式 ＱＢＦ 作 ＳＡＴ 公式的自然扩展具有紧凑的 空间结构以及更强大、更直观的表达能力，对 ＱＢＦ 中极小不可满足子式的研究有利于探索新的 ＱＢＦ 算法．赵希顺［２３］ 证明了 ＱＢＦ 中，对 ＱＣＮＦ 公式固定 差值为 １ 的极小不可满足子式可以在多项式时间内 有解． １ 相关定义 在计算机科学领域，不可满足子式的研究最初 源于 ＳＡＴ 问题，首先介绍本文涉及的相关概念． 定义 １ 命题可满足性问题． 给定一个 ＣＮＦ 表达式 Ｆ 和一个变量集合｛Ｖ ＝ ｘ１ ，ｘ２ ，ｘ３ ｝．如果变量集合 Ｖ 中的一组赋值使得表达 式 Ｆ 的值为真，那么称表达式 Ｆ 是可满足的；否则， 表达式 Ｆ 为不可满足． 定义 ２ 不可满足子式／ 不可满足核（ＵＳ ／ ＵＣ）． 对于一个公式 φ ， ϕ 是 φ 的一个不可满足子 式，当且仅当 φ 是不可满足的，且 ϕ ⊆ φ ． 显然，对于同一个问题实例，可能存在不同的不 可满足子式，每个不可满足子式的子句数也可能不 同．其中一些不可满足子式可能是其他不可满足子 式的子集．在最坏情况下，不可满足子式就是原始公 式本身． 定义 ３ 极小不可满足子式． 对于一个不可满足的公式 φ 的一个不可满足子 式 ϕ ，那么 φ 是极小不可满足子式，当且仅当 ∀ ϕ ∈ φ ，使得 ϕ 是可满足的． 定义 ４ 最小不可满足子式． 给出一个不可满足的公式 φ 以及 φ 的所有不可 满足子式构成的集合 ｛ϕ１ ，ϕ２ ，…，ϕｎ ｝ ，如果 ϕｋ ∈ ｛ϕ１ ，ϕ２ ，…，ϕｎ ｝ 是 最 小 不 可 满 子 式， 当 且 仅 当 ∀ϕｉ ∈｛ϕ１ ，ϕ２ ，…，ϕｎ ｝ ， １ ≤ ｉ ≤ ｎ ， 使 得 ｜ ϕｋ ｜ ≤｜ ϕｉ ｜ ． 定义 ５ 量化布尔公式⁃ＱＢＦ 问题． 一个 ＱＣＮＦ 公式 φ ＝ Ｑ１ ｘ１Ｑ２ ｘ２…Ｑｎ ｘｎϕ ，其中 Ｑｉ ∈｛∃，∀｝ ， ϕ 是一个 ＣＮＦ 公式，用矩阵形式表 达 φ ． ｘ １ ， ｘ ２ ，…， ｘｎ 分别被 Ｑ１ ，Ｑ２ ，…，Ｑｎ 量化．有 时，可以简写为 φ ＝ Ｑϕ ． 定义 ６ ＱＢＦ 极小不可满足子式（ＭＦ）． 当且仅当 φ 是不可满足的，并且从 φ 中移出任 何一个子句将导致公式变为可满足，一个 ＱＢＦ 公式 φ 被称为极小不满足，不可满足子式的子式可以表 示为 ＭＦ（ｍｉｎｉｍａｌ ｆａｌｓｅ ｆｏｒｍｕｌａｓ）． 定义 ７ 可满足性模理论（ＳＭＴ）． ＳＭＴ 是 ＳＡＴ 的一种扩展，其命题不仅包括布尔 公式，还包括其他特定理论中的一阶逻辑约束，如整 数与实数算术类型、位向量、递归及数据类型等． 定义 ８ ＳＭＴ 不可满足子式． 给出一个不可满足的无量词一阶逻辑公式 φ， 当且仅当 ϕ 是不可满足的，并且 ϕ ⊆ φ ， ϕ 是公式 φ 的一个 ＳＭＴ 不可满足子式． 定义 ９ 极小 ＳＭＴ 不可满足子式． 给出不可满足的无量词一阶逻辑公式 φ ，及其 一个不可满足子式 ϕ ，那么 ϕ 是极小 ＳＭＴ 不可满足 子式，当且仅当 ∀ ϕ ∈ φ ，使得 ϕ 是可满足的． 定义 １０ 约束可满足问题（ＣＳＰ）． 由一个变量集合和一个约束集合组成．问题的一 个状态是由对一些或全部变量的一个赋值定义的完 全赋值：每个变量都参与的赋值．问题的解是满足所 有约束的完全赋值，或更进一步，使目标函数最大化． 定义 １１ 极小 ＣＳＰ 不可满足子式． 一个极小 ＣＳＰ 不可满足子式，其约束的有关子 集是不可满足的，并且其真子集是可满足的． ·４９８· 智 能 系 统 学 报 第 ８ 卷
第6期 殷明浩，等：不可满足子式研究 ·499· 2不可满足子式求解算法 2.1.20MUS与ASMUS算法 文献[14]中，E.Gregoire提出了基于启发式局部 按照问题的解决方式，求解布尔不可满足子式的 搜索算法OMUS.OMUS算法是通过计算关键子句分 方法可划分为基于DPLL搜索2,6，]与局部搜 值来获得一个极小不可满足子式的启发式算法.算法 索[通常来说，基于DPL搜索方法能够找到问 主要分为2部分：1)在局部算法中根据子句布尔值为 题的精确解，但其面临的主要挑战是计算时间随问题 假的频度计算子句的分值，移除确定不可能出现在不 规模的增大呈指数级增长.而局部启发式搜索尽管有 可满足子式中的子句具体来说，对于一个不可满足 时无法给出精确解，但其运算速度快，求解效率高. 子式，如果在局部搜索时终未能找到它的一个赋值模 根据不可满足子式的大小可以分为2类：1)极小 型，那么将移除子式中分值最低的子句.获得的子公 不可满足子式的提取算法21川：2)最小不可满足子式 式将被记录在堆栈中.2)检查最后一个未能赋值的子 的提取算法2.相对而言，最小不可满足子式的求 式是否可满足，如果子公式是不可满足的，那么它就 解难度更大，算法的复杂度也更高 是不可满足子式的近似解.否则，重复检查栈顶子句 2.1极小不可满足子式求解 超集的不可满足性，直到一个集合被证明是不可满足 当前主流的不可满足子式提取算法关于极小不 的该过程将获得一个近似的极小不可满足子式.然 可满足子式的提取形式验证与人工智能规划问题 后，调用一个精细调节(fine tunes)过程，OMUS算法 均可转为可满足性问题，一组可满足的赋值代表了 最终获得一个不可满足子式 一种可行方案：反之，说明原问题存在错误，寻找不 E.Gregoire在文献[8]中提出了ASMUS算法， 可满足子式可以精确地对问题进行定位： ASMUS以OMUS为基础，可以近似求解所有不可满 2.1.1基于冲突树的搜索算法 足子式的集合MAX-SAT可以提供极小的不可满足 Han和Lee[2]提出了一个获得所有极小不可满 子式数量MAX-SAT解中的剩余不可满足子句一定 足子式的算法该方法的思想是有序遍历集合S的 尽可能多地属于那些不可满足子式的交集那么对 所有子集.它由2部分组成：1)用CS-tree(冲突树) 于每个子句，记录最小的子句数.在探测到一个不可 的不同结点表示集合S的不同子集，并且没有哪2 满足子式后，把不可满足子式中分值最高的子句删 个结点表示相同的子集.CS-ree定义了子集间的遍 除掉.很显然，ASMUS是不完全的. 历顺序，因此保证了同一子集不被重复搜索.为了实 2.1.3基于消解反驳的局部搜索算法 现这个目标，一个结点由集合D和集合P2部分组 局部搜索是一种求解优化问题的算法，算法从 成，表示为DUP.集合D的元素一定要出现在所 解空间的一个点出发，每一步从当前候选解移动到 有后续子集中，而集合P的元素不需要.如果一个结 一个邻居候选解，去寻找较好的候选解，候选解的质 点有1P|个孩子，它由逐个消减集合P约束，并加 量是由一个评估函数来界定的.局部搜索算法在处 入到集合D中获得.函数all subsets(D,P,中)遍历 理规模较大的问题时，其收敛速度快，求解效率高， CS-tree的所有结点，返回DUX(XCP).当迭代访 上文提到的OMUS与ASMUS实质上是启发式局部 问一个根结点时，每次迭代以深度优先方式遍历 搜索与计数的组合.消解是判定SAT问题的基本方 CS-tree,并且每次内部调用all subsets()函数访问 法之一.一个公式经过一系列的消解步骤最终产生 这个孩子结点的后代.2)利用CS-tree探测所有极小 空子句，则公式是不可满足的.文献[9-11]中采用局 不可满足子式.算法以深度优先方式遍历树，测试每 部搜索方法作为解空间的搜索策略.算法在搜索过 个结点的标志DUP,判断其可满足性如果结点可 程中建立证明公式不可满足性的消解序列，并从其 满足，那么就不必访问它的孩子节点.否则，继续寻 中提取不可满足子式.算法描述如下：算法启发式或 找孩子节点来寻找不可满足子式.如果遍历所有孩 随机地选择2个子句进行消解，最终得到一个消解 子结点没有发现子集A使得ACD.那么集合D就 序列或达到最大迭代次数搜索过程融合了一些基 是极小不可满足集合.文献[2]在以上基本算法中加 于启发式的SAT推理技术，包括二元子句消解、等 入了预处理，利用约束独立性、利用始终满足的子 价约简和单元子句传播.算法首先寻找公式中是否 句、蕴涵、廉价求解器、增量式求解器、无视约束等策 存在单元子句，如果存在，则在公式上进行单元子句 略其中，使用增量式求解器极大地改进了算法，它 传播，并进一步判断能否产生空子句：如果存在二元 减少了对算法规则的依赖性，能够快速地发现可满 子句，则执行二元子句消解与等价性约简，启发式地 足子集 选择消解子句.若2类子句都不存在，则随机选取2
２ 不可满足子式求解算法 按照问题的解决方式，求解布尔不可满足子式的 方法可划分为基于 ＤＰＬＬ 搜索［２，４⁃６，１２⁃１４］ 与局部搜 索［７⁃１１］ ．通常来说 ，基于 ＤＰＬＬ 搜索方法能够找到问 题的精确解，但其面临的主要挑战是计算时间随问题 规模的增大呈指数级增长．而局部启发式搜索尽管有 时无法给出精确解，但其运算速度快，求解效率高． 根据不可满足子式的大小可以分为 ２ 类：１）极小 不可满足子式的提取算法［２⁃１１］ ；２）最小不可满足子式 的提取算法［１２⁃１４］ ．相对而言，最小不可满足子式的求 解难度更大，算法的复杂度也更高． ２．１ 极小不可满足子式求解 当前主流的不可满足子式提取算法关于极小不 可满足子式的提取．形式验证与人工智能规划问题 均可转为可满足性问题，一组可满足的赋值代表了 一种可行方案；反之，说明原问题存在错误，寻找不 可满足子式可以精确地对问题进行定位． ２．１．１ 基于冲突树的搜索算法 Ｈａｎ 和 Ｌｅｅ ［２４］提出了一个获得所有极小不可满 足子式的算法．该方法的思想是有序遍历集合 Ｓ 的 所有子集．它由 ２ 部分组成：１）用 ＣＳ⁃ｔｒｅｅ（冲突树） 的不同结点表示集合 Ｓ 的不同子集，并且没有哪 ２ 个结点表示相同的子集．ＣＳ⁃ｔｒｅｅ 定义了子集间的遍 历顺序，因此保证了同一子集不被重复搜索．为了实 现这个目标，一个结点由集合 Ｄ 和集合 Ｐ ２ 部分组 成，表示为 Ｄ ∪ Ｐ ．集合 Ｄ 的元素一定要出现在所 有后续子集中，而集合 Ｐ 的元素不需要．如果一个结 点有｜ Ｐ ｜ 个孩子，它由逐个消减集合 Ｐ 约束，并加 入到集合 Ｄ 中获得．函数 ａｌｌ ｓｕｂｓｅｔｓ （Ｄ，Ｐ，ϕ） 遍历 ＣＳ⁃ｔｒｅｅ 的所有结点，返回 Ｄ ∪ Ｘ（Ｘ ⊂ Ｐ） ．当迭代访 问一个根结点时，每次迭代以深度优先方式遍历 ＣＳ⁃ｔｒｅｅ，并且每次内部调用 ａｌｌ ｓｕｂｓｅｔｓ（ ）函数访问 这个孩子结点的后代．２）利用 ＣＳ⁃ｔｒｅｅ 探测所有极小 不可满足子式．算法以深度优先方式遍历树，测试每 个结点的标志 Ｄ ∪ Ｐ ，判断其可满足性．如果结点可 满足，那么就不必访问它的孩子节点．否则，继续寻 找孩子节点来寻找不可满足子式．如果遍历所有孩 子结点没有发现子集 Ａ 使得 Ａ ⊂ Ｄ ．那么集合 Ｄ 就 是极小不可满足集合．文献［２］在以上基本算法中加 入了预处理，利用约束独立性、利用始终满足的子 句、蕴涵、廉价求解器、增量式求解器、无视约束等策 略．其中，使用增量式求解器极大地改进了算法，它 减少了对算法规则的依赖性，能够快速地发现可满 足子集． ２．１．２ ＯＭＵＳ 与 ＡＳＭＵＳ 算法 文献［１４］中，É． Ｇｒéｇｏｉｒｅ 提出了基于启发式局部 搜索算法 ＯＭＵＳ．ＯＭＵＳ 算法是通过计算关键子句分 值来获得一个极小不可满足子式的启发式算法．算法 主要分为 ２ 部分：１）在局部算法中根据子句布尔值为 假的频度计算子句的分值，移除确定不可能出现在不 可满足子式中的子句．具体来说，对于一个不可满足 子式，如果在局部搜索时终未能找到它的一个赋值模 型，那么将移除子式中分值最低的子句．获得的子公 式将被记录在堆栈中．２）检查最后一个未能赋值的子 式是否可满足，如果子公式是不可满足的，那么它就 是不可满足子式的近似解．否则，重复检查栈顶子句 超集的不可满足性，直到一个集合被证明是不可满足 的．该过程将获得一个近似的极小不可满足子式．然 后，调用一个精细调节（ｆｉｎｅ ｔｕｎｅｓ）过程，ＯＭＵＳ 算法 最终获得一个不可满足子式． É． Ｇｒéｇｏｉｒｅ 在文献［８］ 中提出了 ＡＳＭＵＳ 算法． ＡＳＭＵＳ 以 ＯＭＵＳ 为基础，可以近似求解所有不可满 足子式的集合．ＭＡＸ⁃ＳＡＴ 可以提供极小的不可满足 子式数量．ＭＡＸ⁃ＳＡＴ 解中的剩余不可满足子句一定 尽可能多地属于那些不可满足子式的交集．那么对 于每个子句，记录最小的子句数．在探测到一个不可 满足子式后，把不可满足子式中分值最高的子句删 除掉．很显然，ＡＳＭＵＳ 是不完全的． ２．１．３ 基于消解反驳的局部搜索算法 局部搜索是一种求解优化问题的算法，算法从 解空间的一个点出发，每一步从当前候选解移动到 一个邻居候选解，去寻找较好的候选解，候选解的质 量是由一个评估函数来界定的．局部搜索算法在处 理规模较大的问题时，其收敛速度快，求解效率高． 上文提到的 ＯＭＵＳ 与 ＡＳＭＵＳ 实质上是启发式局部 搜索与计数的组合．消解是判定 ＳＡＴ 问题的基本方 法之一．一个公式经过一系列的消解步骤最终产生 空子句，则公式是不可满足的．文献［９⁃１１］中采用局 部搜索方法作为解空间的搜索策略．算法在搜索过 程中建立证明公式不可满足性的消解序列，并从其 中提取不可满足子式．算法描述如下：算法启发式或 随机地选择 ２ 个子句进行消解，最终得到一个消解 序列或达到最大迭代次数．搜索过程融合了一些基 于启发式的 ＳＡＴ 推理技术，包括二元子句消解、等 价约简和单元子句传播．算法首先寻找公式中是否 存在单元子句，如果存在，则在公式上进行单元子句 传播，并进一步判断能否产生空子句；如果存在二元 子句，则执行二元子句消解与等价性约简，启发式地 选择消解子句．若 ２ 类子句都不存在，则随机选取 ２ 第 ６ 期 殷明浩，等：不可满足子式研究 ·４９９·
·500· 智能系统学报 第8卷 个子句进行消解.最后采用一个递归函数从空子句 步提高效率，在MiniSat的分支选择中加入了启发式 开始回溯，逐步遍历整个消解序列，提取布尔不可满 策略.当每个变量决策时，MiniSat的分支默认选择 足子式 赋值为负值的一支.在算法的第1轮中，并不发生任 2.1.4基于最大可满足性的求解算法 何变化.第1轮之后，每个尚未删除的子句都在前1 目前，有很多研究人员利用极大可满足性和极 轮中有了一个关联赋值.除了新的关键子句移动到 小不可满足性之间的二元关系提取极小不可满足子 这个赋值的前面，随后的子句仍将保持同样的顺序. 式.Bailey和Stuckey在文献[25]中已经阐述了这种 程序因此确定了变量的分支方向，这将引导求解器 关系.基于最大可满足性的CAMUS[4,Digger!1]能 按着以前关联赋值的方向寻找新的赋值。 够提取极小不可满足子式：贪心遗传算法和蚁群算 2.2最小不可满足子式求解 法「)能够提取最小不可满足子式.文献[26]中提出 不可满足子式反应了问题的存在最小不可满足 了一种在CSP中提取极小不可满足子式的混合算 子式比极小不可满足子式更能精确地定位错误.研究 法.该算法也是基于最大可满足性求解极小不可满 最小不可满足算法，也是研究人员的最终目的.目前 足子式.求解CSP极小不可满足子式的算法一般分 关于最小不可满足子式的提取研究还相对较少， 为直接算法和间接算法.间接算法利用极小不可满 2.2.1基于辅助变量的算法 足子式和极小修正集(MCS)之间的关系.算法主要 算法AMUSE3)和文献[12]中算法通过引入一 是寻找一个完全的极小修正集，然后从中提取极小 组辅助变量求解不可满足子式.AMUSE是对一个基 不可满足子式.另一方面，直接算法通过产生子集和 于DPLL构架的SAT求解器的扩展.它不再寻找一 测试其可满足性直接地在CSPs约束的子集空间搜 个可满足的真值赋值而是寻找其中蕴含的不可满足 索不可满足子式.混合算法融合了直接和间接方法 子式.为此引入了一组辅助变量，通过自底向上的方 混合算法像间接算法那样不再计算全部的极小修正 式搜索不可满足树的空间：从一个空子句开始，逐步 集，而是寻找极小修正集中较小的子集.这就是所谓 添加子句，直到获得一个不可满足子式.为了改善搜 的“主干”集合，即极小修正子集发现的不可消减的 索效率，其中使用了冲突子句学习优化策略.但是 碰集每个主干集表示不可满足子式的一个簇.通过 AMUSE算法无法保证获得极小不可满足子式，尤其 直接方法搜索主干的超级空间，这些主干集随后逐 随着问题规模的扩大，效率会明显下降.文献[6]中 个被扩展为完全的不可满足子式.实验表明，基于最 提出了一个获得最小不可满足子式的模型：ω：= 大可满足性的混合算法比单纯直接算法或间接算法 {一s:}Uw:,其中新子句w是由子句w与选择变 效率高很多.混合算法通过在每步中搜索一个较小 量s:构成.选择变量s:决定是否选择子句w.对每个 的空间提高效率」 S中变量赋值，产生的子式可能是满足的，也可能是 2.1.5基于关联赋值的算法 不满足的对于不可满足的子式，S中有多少变量赋 文献[27]中算法提出了关联赋值的概念，将赋 值为1，就意味着有多少子句包含在不可满足子式 值与子句联系起来.关联赋值的概念来自于布劳威 里.那么最小不可满足子式就是S集合中赋值为1 尔不动点近似算法在可满足性问题方面的应用.它 的、数量最少的子公式通常可以使用高效的求解器 将子句视为实体，也就是一个有序的赋值集合，并且 来实现这个模型.公式中变量被组织成2个互斥的 从可能的赋值中选择一个赋值与其关联.这些赋值 集合：变量集合S和变量集合X首先决策变量S,然 形成一个完整的序列，在序列中优先选择所有可满 后决策变量X因此每次变量S赋值，都定义了一个 足赋值，再选择所有不可满足赋值.当达到帕累托最 潜在的子式.如果对于一个赋值，所有的子句都满 优后，有可能找到这些子句的一个子集来表示不可 足，那么回溯到最近未决策的变量S.否则，每次回 满足性.在帕累托最优中，所有子句已经选择了一个 溯要先改变X赋值，再改变S赋值，直到没有变量X 椎一的不满足自己的赋值.帕累托最优证明了子句 的赋值可以改变，则S中赋值为1最少的，就是最小 的选择权与不可满足公式之间的冲突.当子句证明 不可满足子式」 了公式的不可满足性后，利用文献[27]中的理论去 2.2.2分支限界算法 实现算法，寻找一个不可满足子式.然而这种算法的 文献中[13]中CAMUS-min和Digger都是基于 效率并不高，文献[12]中提出了一个简单有效的极 分支限界的算法.CAMUS-min算法是CAMUS的改 小不可满足子式抽取算法MiniUnsat..MiniUnsat中包 进，它比CAMUS多了分支限界过程.CAMUS利用极 含了一个高效率SAT求解器MiniSat2.0.为了进一 大可满足性和极小不可满足性之间的二元关系提取
个子句进行消解．最后采用一个递归函数从空子句 开始回溯，逐步遍历整个消解序列，提取布尔不可满 足子式． ２．１．４ 基于最大可满足性的求解算法 目前，有很多研究人员利用极大可满足性和极 小不可满足性之间的二元关系提取极小不可满足子 式．Ｂａｉｌｅｙ 和 Ｓｔｕｃｋｅｙ 在文献［２５］中已经阐述了这种 关系．基于最大可满足性的 ＣＡＭＵＳ ［４］ ，Ｄｉｇｇｅｒ ［１３］ 能 够提取极小不可满足子式；贪心遗传算法和蚁群算 法［１４］能够提取最小不可满足子式．文献［２６］中提出 了一种在 ＣＳＰ 中提取极小不可满足子式的混合算 法．该算法也是基于最大可满足性求解极小不可满 足子式．求解 ＣＳＰ 极小不可满足子式的算法一般分 为直接算法和间接算法．间接算法利用极小不可满 足子式和极小修正集（ＭＣＳ）之间的关系．算法主要 是寻找一个完全的极小修正集，然后从中提取极小 不可满足子式．另一方面，直接算法通过产生子集和 测试其可满足性直接地在 ＣＳＰｓ 约束的子集空间搜 索不可满足子式．混合算法融合了直接和间接方法． 混合算法像间接算法那样不再计算全部的极小修正 集，而是寻找极小修正集中较小的子集．这就是所谓 的“主干”集合，即极小修正子集发现的不可消减的 碰集．每个主干集表示不可满足子式的一个簇．通过 直接方法搜索主干的超级空间，这些主干集随后逐 个被扩展为完全的不可满足子式．实验表明，基于最 大可满足性的混合算法比单纯直接算法或间接算法 效率高很多．混合算法通过在每步中搜索一个较小 的空间提高效率． ２．１．５ 基于关联赋值的算法 文献［２７］中算法提出了关联赋值的概念，将赋 值与子句联系起来．关联赋值的概念来自于布劳威 尔不动点近似算法在可满足性问题方面的应用．它 将子句视为实体，也就是一个有序的赋值集合，并且 从可能的赋值中选择一个赋值与其关联．这些赋值 形成一个完整的序列，在序列中优先选择所有可满 足赋值，再选择所有不可满足赋值．当达到帕累托最 优后，有可能找到这些子句的一个子集来表示不可 满足性．在帕累托最优中，所有子句已经选择了一个 惟一的不满足自己的赋值．帕累托最优证明了子句 的选择权与不可满足公式之间的冲突．当子句证明 了公式的不可满足性后，利用文献［２７］中的理论去 实现算法，寻找一个不可满足子式．然而这种算法的 效率并不高，文献［１２］中提出了一个简单有效的极 小不可满足子式抽取算法 ＭｉｎｉＵｎｓａｔ．ＭｉｎｉＵｎｓａｔ 中包 含了一个高效率 ＳＡＴ 求解器 ＭｉｎｉＳａｔ ２．０．为了进一 步提高效率，在 ＭｉｎｉＳａｔ 的分支选择中加入了启发式 策略．当每个变量决策时，ＭｉｎｉＳａｔ 的分支默认选择 赋值为负值的一支．在算法的第 １ 轮中，并不发生任 何变化．第 １ 轮之后，每个尚未删除的子句都在前 １ 轮中有了一个关联赋值．除了新的关键子句移动到 这个赋值的前面，随后的子句仍将保持同样的顺序． 程序因此确定了变量的分支方向，这将引导求解器 按着以前关联赋值的方向寻找新的赋值． ２．２ 最小不可满足子式求解 不可满足子式反应了问题的存在．最小不可满足 子式比极小不可满足子式更能精确地定位错误．研究 最小不可满足算法，也是研究人员的最终目的．目前 关于最小不可满足子式的提取研究还相对较少． ２．２．１ 基于辅助变量的算法 算法 ＡＭＵＳＥ ［３］和文献［１２］中算法通过引入一 组辅助变量求解不可满足子式．ＡＭＵＳＥ 是对一个基 于 ＤＰＬＬ 构架的 ＳＡＴ 求解器的扩展．它不再寻找一 个可满足的真值赋值而是寻找其中蕴含的不可满足 子式．为此引入了一组辅助变量，通过自底向上的方 式搜索不可满足树的空间：从一个空子句开始，逐步 添加子句，直到获得一个不可满足子式．为了改善搜 索效率，其中使用了冲突子句学习优化策略．但是 ＡＭＵＳＥ 算法无法保证获得极小不可满足子式，尤其 随着问题规模的扩大，效率会明显下降．文献［６］中 提出了一个获得最小不可满足子式的模型： ω ′ ｉ ＝ ｛¬ ｓｉ｝ ∪ ωｉ ，其中新子句 ω ′ ｉ 是由子句 ωｉ 与选择变 量 ｓｉ 构成．选择变量 ｓｉ 决定是否选择子句 ωｉ ． 对每个 Ｓ 中变量赋值，产生的子式可能是满足的，也可能是 不满足的．对于不可满足的子式，Ｓ 中有多少变量赋 值为 １，就意味着有多少子句包含在不可满足子式 里．那么最小不可满足子式就是 Ｓ 集合中赋值为 １ 的、数量最少的子公式．通常可以使用高效的求解器 来实现这个模型．公式中变量被组织成 ２ 个互斥的 集合：变量集合 Ｓ 和变量集合 Ｘ．首先决策变量 Ｓ，然 后决策变量 Ｘ．因此每次变量 Ｓ 赋值，都定义了一个 潜在的子式．如果对于一个赋值，所有的子句都满 足，那么回溯到最近未决策的变量 Ｓ．否则，每次回 溯要先改变 Ｘ 赋值，再改变 Ｓ 赋值，直到没有变量 Ｘ 的赋值可以改变，则 Ｓ 中赋值为 １ 最少的，就是最小 不可满足子式． ２．２．２ 分支限界算法 文献中［１３］中 ＣＡＭＵＳ⁃ｍｉｎ 和 Ｄｉｇｇｅｒ 都是基于 分支限界的算法．ＣＡＭＵＳ⁃ｍｉｎ 算法是 ＣＡＭＵＳ 的改 进，它比 ＣＡＭＵＳ 多了分支限界过程．ＣＡＭＵＳ 利用极 大可满足性和极小不可满足性之间的二元关系提取 ·５００· 智 能 系 统 学 报 第 ８ 卷
第6期 殷明浩，等：不可满足子式研究 ·501· 极小不可满足子式，一般分为2步：1)获得公式中 限界算法，而贪心遗传算法无论在运行时间还是不 有所极大可满足子式的补集：2)通过在递归树中寻 可满足子式的大小上都优于蚁群算法， 找补集的极小碰集来提取极小不可满足子式.CA- 2.3SMT中不可满足子式求解算法 MUS-min与CAMUS不同之处在第2步，不直接寻 随着SMT技术的不断发展，它开始逐渐取代 找极小碰集，而在递归中增加了分支限界功能来减 SAT.SMT具有更好的抽象能力，更接近于高层设 小树的搜空间，产生最小的碰集.CAMUS-min中，一 计，极其具有发展潜力.它使用字级建模，不必像 个贪婪的启发式策略MIS-quick为算法提供下界， SAT中将问题转化为位级处理，从而减少了空间和 如果递归树所包含的不可满足子式没有当前不可满 时间的开销.ST可以看做是SAT问题的一个扩 足子式小，CAMUS-min删除递归树中的这些分支， 展，它极大地补充了SAT的不足之处.求解其极小不 因此运行时间大幅减少，并且最后的不可满足子式 可满足子式算法也是非常具有实际意义的.SMT技 一定是最小不可满足子式.Digger使用一个递归的 术是近几年发展起来的，目前提取ST中极小不可 分支限界树来获得最小不可满足子式.树中的每个 满足子式的算法比较少， 结点都是原始公式的一个子集，并且上下界由子集 2.3.1 Lemma--lifting方式 中的最小不可满足子式限定.因此算法在根结点处 Cimatt等[1s.16o提出了求解SMT不可满足子式 启动递归调用.Digger不同于标准的分支限界树，不 的算法一Lemma-lifting方式.Lemma--lifting方式将 光遍历叶子结点，也遍历包括根结点的所有结点.对 SMT求解器与外部命题核提取器结合起来，通过一 于每个结点，算法利用不相交的极小修正集，启发式 种直接的方式求解SMT.SMT求解器保存并返回在 选择子句的一个样本集，这不同于CAMUS-min中寻 证明公式不可满足性的过程中获得的特定理论引 找全部极小修正集.实质上，Digger利用不相交的极 理.外部命题核提取器随后调用原始SMT问题和特 小修正集关系将一个问题分解为更容易处理的子公 定理论引理的布尔抽象.算法是基于以下2个重要 式，同时在搜索最小不可满足子式过程中提供了一 的观察：1)在搜索过程中，SMT求解器发现的特定 个非常有效的下界. 理论引理是在T理论中考虑的有效子句，因此它们 2.2.3贪心遗传算法 不影响T中一个公式的可满足性：2)原始SMT公式 贪心遗传算法[4]可以视为贪心算法与遗传算 与特定理论引理的合取是命题不可满足的.因此，当 法的混合算法.贪心算法是指在对问题求解时，总是 外部命题核提取器找到原始ST公式与特定理论 做出在当前看来是最好的选择也就是说，不从整体 引理的合取的一个核时，应当删除其中的特定理论 最优上加以考虑，它所做出的仅是在某种意义上的 引理，获得一个精简的原始公式的子集.虽然在原理 局部最优解.遗传算法(genetic algorithm)是一类借 上很简单，但是该方式的概念很有趣，本质上讲， 鉴生物界的进化规律演化而来的随机化搜索方法 ST求解器动态地将理论信息适当地转化为布尔 它由美国的J.Holland教授于1975年首先提出，其 标准.而且，该方式还有以下优点：1)易于实现与升 主要特点是直接对结构对象进行操作，不存在求导 级.由于ST求解器与布尔不可满足子式提取算法 和函数连续性的限定：具有内在的隐并行性和更好 是相互独立的，因此能够将最新的求解器或算法进 的全局寻优能力：采用概率化的寻优方法，能自动获 行组合，从而提高SMT不可满足子式的求解效率； 取和指导优化的搜索空间，自适应地调整搜索方向， 2)寻找较小的不可满足子式非常有效：3)内核提取 不需要确定规则遗传算法是全局进化方法，可以避 不需要复杂的SMT推理.但是，该算法有如下缺点： 免进入局部最优，但是在初期缺乏充分有效启发信 1)需要额外的存储空间用来保存SMT求解器产生 息的情况下局部收敛速度较慢，并且对初始种群十 的引理：2)无法保证最终求得的不可满足子式是极 分依赖所以将贪心算法与遗传算法有效地结合起 小不可满子式 来，保留了2种算法的优点，极大地避免了2种算法 2.3.2基于DPLL构架求解算法 的不足.贪心遗传算法的基本策略是：首先采用贪心 DPLL是一种基于回溯的算法，在成熟运用于 算法快速计算不可满足子式的近似最优解，为遗传 SAT求解器后，基于DPLL(T)的SMT求解技术也 算法构造一个较优的初始种群，缩减其搜索空间，而 得到飞速发展.DPLL(T)由布尔引擎DPLL(X)与特 后利用遗传算法的全局性反复精化近似解，从而得 定的理论求解器T-slover组成.文献[16-17]就是基 到更小的不可满足子式实验结果表明，在运算效率 于DPLL(T)构架求解不可满足子式.文献[17]提出 以及单位时间内删除的短句数方面，显著高于分支 了深度优先方式的极小不可满足子式算法(DFS
极小不可满足子式，一般分为 ２ 步：１） 获得公式中 有所极大可满足子式的补集；２）通过在递归树中寻 找补集的极小碰集来提取极小不可满足子式．ＣＡ⁃ ＭＵＳ⁃ｍｉｎ 与 ＣＡＭＵＳ 不同之处在第 ２ 步，不直接寻 找极小碰集，而在递归中增加了分支限界功能来减 小树的搜空间，产生最小的碰集．ＣＡＭＵＳ⁃ｍｉｎ 中，一 个贪婪的启发式策略 ＭＩＳ⁃ｑｕｉｃｋ 为算法提供下界， 如果递归树所包含的不可满足子式没有当前不可满 足子式小，ＣＡＭＵＳ⁃ｍｉｎ 删除递归树中的这些分支， 因此运行时间大幅减少，并且最后的不可满足子式 一定是最小不可满足子式．Ｄｉｇｇｅｒ 使用一个递归的 分支限界树来获得最小不可满足子式．树中的每个 结点都是原始公式的一个子集，并且上下界由子集 中的最小不可满足子式限定．因此算法在根结点处 启动递归调用．Ｄｉｇｇｅｒ 不同于标准的分支限界树，不 光遍历叶子结点，也遍历包括根结点的所有结点．对 于每个结点，算法利用不相交的极小修正集，启发式 选择子句的一个样本集，这不同于 ＣＡＭＵＳ⁃ｍｉｎ 中寻 找全部极小修正集．实质上，Ｄｉｇｇｅｒ 利用不相交的极 小修正集关系将一个问题分解为更容易处理的子公 式，同时在搜索最小不可满足子式过程中提供了一 个非常有效的下界． ２．２．３ 贪心遗传算法 贪心遗传算法［１４］ 可以视为贪心算法与遗传算 法的混合算法．贪心算法是指在对问题求解时，总是 做出在当前看来是最好的选择．也就是说，不从整体 最优上加以考虑，它所做出的仅是在某种意义上的 局部最优解．遗传算法（ ｇｅｎｅｔｉｃ ａｌｇｏｒｉｔｈｍ） 是一类借 鉴生物界的进化规律演化而来的随机化搜索方法． 它由美国的 Ｊ．Ｈｏｌｌａｎｄ 教授于 １９７５ 年首先提出，其 主要特点是直接对结构对象进行操作，不存在求导 和函数连续性的限定；具有内在的隐并行性和更好 的全局寻优能力；采用概率化的寻优方法，能自动获 取和指导优化的搜索空间，自适应地调整搜索方向， 不需要确定规则．遗传算法是全局进化方法，可以避 免进入局部最优，但是在初期缺乏充分有效启发信 息的情况下局部收敛速度较慢，并且对初始种群十 分依赖．所以将贪心算法与遗传算法有效地结合起 来，保留了 ２ 种算法的优点，极大地避免了 ２ 种算法 的不足．贪心遗传算法的基本策略是：首先采用贪心 算法快速计算不可满足子式的近似最优解，为遗传 算法构造一个较优的初始种群，缩减其搜索空间，而 后利用遗传算法的全局性反复精化近似解，从而得 到更小的不可满足子式．实验结果表明，在运算效率 以及单位时间内删除的短句数方面，显著高于分支 限界算法，而贪心遗传算法无论在运行时间还是不 可满足子式的大小上都优于蚁群算法． ２．３ ＳＭＴ 中不可满足子式求解算法 随着 ＳＭＴ 技术的不断发展，它开始逐渐取代 ＳＡＴ．ＳＭＴ 具有更好的抽象能力，更接近于高层设 计，极其具有发展潜力． 它使用字级建模，不必像 ＳＡＴ 中将问题转化为位级处理，从而减少了空间和 时间的开销． ＳＭＴ 可以看做是 ＳＡＴ 问题的一个扩 展，它极大地补充了 ＳＡＴ 的不足之处．求解其极小不 可满足子式算法也是非常具有实际意义的．ＳＭＴ 技 术是近几年发展起来的，目前提取 ＳＭＴ 中极小不可 满足子式的算法比较少． ２．３．１ Ｌｅｍｍａ⁃ｌｉｆｔｉｎｇ 方式 Ｃｉｍａｔｔｉ 等［１５⁃１６］ 提出了求解 ＳＭＴ 不可满足子式 的算 法—Ｌｅｍｍａ⁃ｌｉｆｔｉｎｇ 方 式． Ｌｅｍｍａ⁃ｌｉｆｔｉｎｇ 方 式 将 ＳＭＴ 求解器与外部命题核提取器结合起来，通过一 种直接的方式求解 ＳＭＴ．ＳＭＴ 求解器保存并返回在 证明公式不可满足性的过程中获得的特定理论引 理．外部命题核提取器随后调用原始 ＳＭＴ 问题和特 定理论引理的布尔抽象．算法是基于以下 ２ 个重要 的观察：１）在搜索过程中，ＳＭＴ 求解器发现的特定 理论引理是在 Ｔ 理论中考虑的有效子句，因此它们 不影响 Ｔ 中一个公式的可满足性；２）原始 ＳＭＴ 公式 与特定理论引理的合取是命题不可满足的．因此，当 外部命题核提取器找到原始 ＳＭＴ 公式与特定理论 引理的合取的一个核时，应当删除其中的特定理论 引理，获得一个精简的原始公式的子集．虽然在原理 上很简单，但是该方式的概念很有趣，本质上讲， ＳＭＴ 求解器动态地将理论信息适当地转化为布尔 标准．而且，该方式还有以下优点：１）易于实现与升 级．由于 ＳＭＴ 求解器与布尔不可满足子式提取算法 是相互独立的，因此能够将最新的求解器或算法进 行组合，从而提高 ＳＭＴ 不可满足子式的求解效率； ２）寻找较小的不可满足子式非常有效；３）内核提取 不需要复杂的 ＳＭＴ 推理．但是，该算法有如下缺点： １）需要额外的存储空间用来保存 ＳＭＴ 求解器产生 的引理；２）无法保证最终求得的不可满足子式是极 小不可满子式． ２．３．２ 基于 ＤＰＬＬ 构架求解算法 ＤＰＬＬ 是一种基于回溯的算法，在成熟运用于 ＳＡＴ 求解器后，基于 ＤＰＬＬ（ Ｔ） 的 ＳＭＴ 求解技术也 得到飞速发展．ＤＰＬＬ（Ｔ）由布尔引擎 ＤＰＬＬ（Ｘ）与特 定的理论求解器 Ｔ⁃ｓｌｏｖｅｒ 组成．文献［１６⁃１７］就是基 于 ＤＰＬＬ（Ｔ）构架求解不可满足子式．文献［１７］提出 了深度优先方式的极小不可满足子式算法（ＤＦＳ⁃ 第 ６ 期 殷明浩，等：不可满足子式研究 ·５０１·
502 智能系统学报 第8卷 MUSE)和深度优先方式的极小不可满足子式算法 不可满足子式的复杂性 (BS-MUSE).这2个算法从不可满足子式中删除任 意一个子句，然后测试其余子句构成公式的可满足 研究不可满足子式的复杂性，对不可满足子式 性，从而判断是否为极小不可满足子式：而不必测试 算法的提出和改进有重大意义。 不可满足子式所有的真子式，将复杂度从指数降为 3.1不可满足子式的子类 线性.算法中也融合了剪枝技术、冲突子句学习技术 研究人员对不可满足子式的子类感兴趣有以下 用于别除不必要的冗余不可满足性测试，从而缩小 原因：1)有利于发展新的可满足性算法，例如，对极 了搜索空间，提高了搜索效率.算法中也融合了动态 小不可满足子式结构的深入了解，可能会改进DP 排序技术，降低了刚测试过子句的优先级，避免重复 算法：2)可能有助于求解难度大的公式.例如利用差 测试.DFS-MUSE的一个重要特点是：当选择搜索树 值特性产生新的多项式时间可解的公式类[2]：3)不 中不同的分支，会得到不同的极小SMT不可满足子 可满足子式的决策问题是DP-complete,但是不可满 式.BFS-MUSE与DFS-MUSE的区别在于搜索策略 足子式的一些子类的复杂性可能相对容易.BU 不同.BFS-MUSE是以宽度优先的方式对搜索树进 NING H K和赵希顺[190]将不可满足子式进行分类 行遍历，首先考虑同样大小的子式的可满足性，然后 研究，并讨论了这些子类的复杂性.MARG-MU类是 再考虑较小的子式.DFS-MUSE是以深度优先的方 指，如果一个极小不可满足子式是临界类，那么移除 式对搜索树进行遍历，先对当前子树内子式的可满 任意一个文字事件，将导致公式成为非极小不可满 足性测试，找出最小的子式，然后再测试其他子树的 足子式.也就是说MARG-MU类中没有多余文字 可满足性。 MAX-MU类由最大的极小不可满足子式构成，即公 式中再加入一个文字将不再是极小不可满足子式 2.3.3基于否正蕴涵图的求解算法 Unique-SAT指公式在移除任意一个子句后，只有一 文献[18]中提出了基于否正蕴涵与冲突分析 个可满足的真值分配.带有这种性质的极小不可满 提取SMT中极小不可满足子式的算法CARI-MUSE. 足子式，就是Unique-MU类.Almost-Unique-MU类， 否证蕴含图是指对一个不可满足的SMT子式及其 是Unique-MU较小的改进，即至多有一个子句f∈ 子句蕴含图，从该蕴含图的每个子句出发，至少存在 F,使得F-{f升有多于一个可满足的真值分配.Dis 一条路径可以达到空子句.否证蕴含图与不可满足 -MU类指一个极小不可满足子式F可以分裂为2 子式存在以下密切关系：对于不可满足公式F的一 个独立的公式G与H,且公式G与H中不再包含互 个消解反驳R和R对应的否证蕴含图G,那么G中 补文字.目前一些证据[9表明Unique-SAT不是D 逆向可达结点集合与公式F的交集就是F的一个 complete的，那么Unique-MU也不太可能是D- 不可满足子式.CARI-MUSE算法以上述结论为依 complete.Almost-Unique-MU要比Unique-MU复杂， 据，利用ST求解器记录在证明公式不可满足性的 因为文中证明了它是DP-complete..但是未能找到 过程中产生的消解反驳序列，并将其转化为否证蕴 Dis-MU归约到Unique-SAT方法.文献[20]中证明 含图，提取出不可满足子式为了进一步获得极小不 了以下层次结构： 可满足子式，依次删除蕴含图中原始子句及其相关 Unique-SAT≈，Unique-MU≤，Dis-MU 的冲突短句，调用SMT求解器来判断否证蕴涵图的 MU≈，MARG-MU≤，MAX-MU≈，Almost-U- 剩余子公式（结点）的可满足性，以确定该子句是否 nique-MU 为不可满足的原因：如果剩余子公式是可满足的，说 式中：≤。表示多项式时间可约.A≈B是 明公式已经是极小不可满足子式：否则，从否证蕴含 A≤B,B≤A的缩写 图中删除该子句及其冲突短句，形成更小的否证蕴 3.2不可满足子式参数复杂性 含图：算法迭代的遍历否证蕴含图中所有原始子句， Downey和Fellows提出了一种解决NP难问题 最后得到极小ST不可满足子式.为了提高搜索效 的新的研究方法，即很多难解和无法判定的问题通 率，算法中集成了蕴含图剪枝技术，减小了算法的搜 过引入参数可以得到时间复杂度为O(f(k)·n“)的 索空间.实验结果表明，CARI-MUSE算法的效率明 固定参数可解(TP)方法.极小不可满足子式也可 显高于求解极小不可满足子式的深度优先搜索算法 以参数化，通常用MU(k)(k≥1)表示固定差值为 DFS-MUSE:并且随着公式复杂度的增加，性能优势 k的极小不可满足子式参数k是子句数减去变量数 更加明显 的差值.文献[21]中提出了一个多项式时间算法来
ＭＵＳＥ）和深度优先方式的极小不可满足子式算法 （ＢＦＳ⁃ＭＵＳＥ）．这 ２ 个算法从不可满足子式中删除任 意一个子句，然后测试其余子句构成公式的可满足 性，从而判断是否为极小不可满足子式；而不必测试 不可满足子式所有的真子式，将复杂度从指数降为 线性．算法中也融合了剪枝技术、冲突子句学习技术 用于剔除不必要的冗余不可满足性测试，从而缩小 了搜索空间，提高了搜索效率．算法中也融合了动态 排序技术，降低了刚测试过子句的优先级，避免重复 测试．ＤＦＳ⁃ＭＵＳＥ 的一个重要特点是：当选择搜索树 中不同的分支，会得到不同的极小 ＳＭＴ 不可满足子 式．ＢＦＳ⁃ＭＵＳＥ 与 ＤＦＳ⁃ＭＵＳＥ 的区别在于搜索策略 不同．ＢＦＳ⁃ＭＵＳＥ 是以宽度优先的方式对搜索树进 行遍历，首先考虑同样大小的子式的可满足性，然后 再考虑较小的子式．ＤＦＳ⁃ＭＵＳＥ 是以深度优先的方 式对搜索树进行遍历，先对当前子树内子式的可满 足性测试，找出最小的子式，然后再测试其他子树的 可满足性． ２．３．３ 基于否正蕴涵图的求解算法 文献［１８］中提出了基于否正蕴涵与冲突分析 提取 ＳＭＴ 中极小不可满足子式的算法 ＣＡＲＩ⁃ＭＵＳＥ． 否证蕴含图是指对一个不可满足的 ＳＭＴ 子式及其 子句蕴含图，从该蕴含图的每个子句出发，至少存在 一条路径可以达到空子句．否证蕴含图与不可满足 子式存在以下密切关系：对于不可满足公式 Ｆ 的一 个消解反驳 Ｒ 和 Ｒ 对应的否证蕴含图 Ｇ，那么 Ｇ 中 逆向可达结点集合与公式 Ｆ 的交集就是 Ｆ 的一个 不可满足子式． ＣＡＲＩ⁃ＭＵＳＥ 算法以上述结论为依 据，利用 ＳＭＴ 求解器记录在证明公式不可满足性的 过程中产生的消解反驳序列，并将其转化为否证蕴 含图，提取出不可满足子式．为了进一步获得极小不 可满足子式，依次删除蕴含图中原始子句及其相关 的冲突短句，调用 ＳＭＴ 求解器来判断否证蕴涵图的 剩余子公式（结点）的可满足性，以确定该子句是否 为不可满足的原因；如果剩余子公式是可满足的，说 明公式已经是极小不可满足子式；否则，从否证蕴含 图中删除该子句及其冲突短句，形成更小的否证蕴 含图；算法迭代的遍历否证蕴含图中所有原始子句， 最后得到极小 ＳＭＴ 不可满足子式．为了提高搜索效 率，算法中集成了蕴含图剪枝技术，减小了算法的搜 索空间．实验结果表明，ＣＡＲＩ⁃ＭＵＳＥ 算法的效率明 显高于求解极小不可满足子式的深度优先搜索算法 ＤＦＳ⁃ＭＵＳＥ；并且随着公式复杂度的增加，性能优势 更加明显． ３ 不可满足子式的复杂性 研究不可满足子式的复杂性，对不可满足子式 算法的提出和改进有重大意义． ３．１ 不可满足子式的子类 研究人员对不可满足子式的子类感兴趣有以下 原因：１）有利于发展新的可满足性算法，例如，对极 小不可满足子式结构的深入了解，可能会改进 ＤＰ 算法；２）可能有助于求解难度大的公式．例如利用差 值特性产生新的多项式时间可解的公式类［２８］ ；３）不 可满足子式的决策问题是 Ｄ ｐ ⁃ｃｏｍｐｌｅｔｅ，但是不可满 足子式的一些子类的复杂 性 可 能 相 对 容 易． ＢÜ ＮＩＮＧ Ｈ Ｋ 和赵希顺［１９⁃２０］将不可满足子式进行分类 研究，并讨论了这些子类的复杂性．ＭＡＲＧ⁃ＭＵ 类是 指，如果一个极小不可满足子式是临界类，那么移除 任意一个文字事件，将导致公式成为非极小不可满 足子式．也就是说 ＭＡＲＧ⁃ＭＵ 类中没有多余文字． ＭＡＸ⁃ＭＵ 类由最大的极小不可满足子式构成，即公 式中再加入一个文字将不再是极小不可满足子式． Ｕｎｉｑｕｅ⁃ＳＡＴ 指公式在移除任意一个子句后，只有一 个可满足的真值分配．带有这种性质的极小不可满 足子式，就是 Ｕｎｉｑｕｅ⁃ＭＵ 类．Ａｌｍｏｓｔ⁃Ｕｎｉｑｕｅ⁃ＭＵ 类， 是 Ｕｎｉｑｕｅ⁃ＭＵ 较小的改进，即至多有一个子句 ｆ ∈ Ｆ， 使得 Ｆ － ｛ｆ｝ 有多于一个可满足的真值分配．Ｄｉｓ －ＭＵ 类指一个极小不可满足子式 Ｆ 可以分裂为 ２ 个独立的公式 Ｇ 与 Ｈ，且公式 Ｇ 与 Ｈ 中不再包含互 补文字．目前一些证据［２９］表明 Ｕｎｉｑｕｅ⁃ＳＡＴ 不是 Ｄ ｐ ⁃ ｃｏｍｐｌｅｔｅ 的， 那 么 Ｕｎｉｑｕｅ⁃ＭＵ 也 不 太 可 能 是 Ｄ ｐ ⁃ ｃｏｍｐｌｅｔｅ．Ａｌｍｏｓｔ⁃Ｕｎｉｑｕｅ⁃ＭＵ 要比 Ｕｎｉｑｕｅ⁃ＭＵ 复杂， 因为文中证明了它是 Ｄ ｐ ⁃ｃｏｍｐｌｅｔｅ． 但是未能找到 Ｄｉｓ⁃ＭＵ 归约到 Ｕｎｉｑｕｅ⁃ＳＡＴ 方法．文献［２０］ 中证明 了以下层次结构： Ｕｎｉｑｕｅ⁃ＳＡＴ≈ｐＵｎｉｑｕｅ⁃ＭＵ≤ｐＤｉｓ⁃ＭＵ ＭＵ ≈ｐＭＡＲＧ⁃ＭＵ ≤ｐＭＡＸ － ＭＵ ≈ｐＡｌｍｏｓｔ － Ｕ⁃ ｎｉｑｕｅ－ＭＵ 式中： ≤ｐ 表示多项 式 时 间 可 约． Ａ ≈ｐＢ 是 Ａ ≤ｐＢ ， Ｂ ≤ｐＡ 的缩写． ３．２ 不可满足子式参数复杂性 Ｄｏｗｎｅｙ 和 Ｆｅｌｌｏｗｓ 提出了一种解决 ＮＰ 难问题 的新的研究方法，即很多难解和无法判定的问题通 过引入参数可以得到时间复杂度为 Ｏ（ｆ（ｋ）·ｎ α ） 的 固定参数可解（ＦＴＰ）方法．极小不可满足子式也可 以参数化，通常用 ＭＵ （ｋ）（ｋ ≥ １） 表示固定差值为 ｋ 的极小不可满足子式．参数 ｋ 是子句数减去变量数 的差值．文献［２１］中提出了一个多项式时间算法来 ·５０２· 智 能 系 统 学 报 第 ８ 卷
第6期 殷明浩，等：不可满足子式研究 ·503· 判断一个公式是否属于MU(k).因为其使用了“遍 其缺点，尽可能提高算法的效率.例如文献[26]中提 历全部k个子集”的策略，所以算法非常依赖参数k 出了一种在CSP中提取极小不可满足子式的混合 H.Fleischne等利用双边图匹配的某些相应赋值限 算法，这是直接算法和间接算法的混合.文献[14]求 制寻找一个可满足的真值赋值.算法的时间复杂度 解最小不可满足子式可以视为贪心算法与遗传算法 为n,精确上界0(lnk+1/2).(l为公式长度，n 的混合算法 为公式的变量数).S.Szeide[2提出了一个算法，并 3)新领域中扩展：在形式验证等实际应用中， 得到一个新的结果.算法产生于SAT问题的固定参 QBF、CSP、SMT都比SAT表达力强.尤其SMT技术 数可解问题：对于一个CNF公式F,如果其子集中 得到飞速发展，并且在验证领域获得很好的效果.研 子句个数超过变量个数最多k个，那么可以在 究SMT的极小不可满足子式将是未来主要方向. O(2n3)时间内判断公式F的可满足性.参数k就 4)参数复杂性：将固定差值的极小不可满足子 是F的最大差值，可以用图匹配算法有效计算.最 式转化为固定参数问题，并且求解其计算复杂性.但 后，基于以上结论，利用图论中的最大差值和q-ex 是，对于QBF中，MF(k)(k>1)是否可以在多项式 panding双边图0]计算出改进的结果为O(2*n). 时间内判定，依然是开放的， 3.3QBF中的极小不可满足子式 参考文献： 近年来，SAT技术已经成功应用在限界模型检验 (bounded model checking,BMC)并推广到限界的模型 [1]GUPTA A.Learning abstractions for model checking[D]. Pittsburgh:Carnegie Mellon University,2006:1-180. 检验.但是直接将基于SAT的BMC推广到非限界的 [2]De La BANDA M G,STUCKEY P J,WAZNY J.Finding 模型检验的方法不能克服软件规模增大导致的状态 all minimal unsatisfiable subsets [C]//Proceedings of the 空间爆炸问题，即模型检验过程中软件规模的增大可 5th ACM SIGPLAN International Conference on Principles 能导致命题逻辑公式的长度呈指数倍的增长.带量词 and Practice of Declaritive Programming.New York,USA, 2003:32-43. 的布尔公式QBF作为SAT公式的自然扩展具有紧凑 [3]OH Y,MNEIMNEH M N,ANDRAUS Z S.AMUSE:a 的空间结构和更强大、更直观的表达能力， minimally unsatisfiable subformula extractor[C]//Proceed- 赵希顺等2]对QBF中的极小不可满足问题 ings of the 41st Annual Design Automation Conference.New (minimal falsity,MF)进行了研究.对不可满足的子 York,USA,2004:518-523. 式研究，有可能产生新的QBF求解算法.QBF的最 [4]LIFFTTON M,SAKALLAH K.On finding all minimally un- satisfiable subformulas [C]//Theory and Applications of 小不可满足公式QCNF指的是该公式不可满足但其 Satisfiability Testing.St.Andrews,Scotland,2005:173- 任一真子公式均可满足.一个QCNF公式的差值不 186. 同于命题公式的差值，其差值是子句数和存在量词 [5]MARQUES-SILVA J,LYNCE I.On improving MUS extrac- 之间的差值.对QCNF公式固定差值为1的极小不 tion algorithms[M//Lecture Notes in Computer Science, Heidelberg:Springer,2011,6695:159-173. 可满足子式可表示为MF(1).文献[23]中得出重要 [6]Van MAAREN H,WIERINGA S.Finding guaranteed 结论：对QCNF公式固定差值为1的极小不可满足 MUSes fast[M].Heidelberg:Springer,2008:291-304. 子式可以在多项式时间有解.这个证明依赖于公式 [7]GREGOIRE E,MAZURE B,PIETTE C.Extracting MUSes MU(1)的结构.对于MF(k)(k≥2)是否存在多项 [C]//Proceedings of the 17th European Conference on Ar- 式时间可解，仍然是开放的. tificial Intelligence 2006.Riva del Garda,Italy,2006:387- 391. 4总结与展望 8]GREGOIRE E.MAZURE B.PIETTE C.Local-search ex- traction of MUSes[J].Constrain,2007,12(3):325-344. 不可满足子式的研究给研究人员带了多方面的 [9]ZHANG J,SHEN S,LI S.Finding unsatisfiable subformu- 挑战，但是也给研究人员带来多方面机会.不可满足 las with stochastic method M].Heidelberg:Springer, 2007,4881:385-394. 子式的研究出现了以下研究方面的热点， [10]ZHANG J,SHEN S,LI S.A heuristic local search algo- 1)使用符号化技术，如BDD技术能够紧凑地表 rithm for unsatisfiable cores extraction[M].Heidelberg: 示公式，是缓解内存瓶颈的关键技术.文献[31]借助 Springer,.2007,4707:649-659. 于BDD判断公式是不可满足的并且其全部子公式 [11]ZHANG J,SHEN S,LI S.Tracking unsatisfiable subfor- 是满足的，从而证明公式是极小不可满足子式， mulas from reduced refutation proof[J].Journal of Soft- ware,2009,4(1):42-49. 2)混合求解算法：每种求解策略有其自身优点 [12]LYNCE I,MARQUES-SILVA J P.On computing minimum 和缺点.混合求解有利于发挥各自算法的优势，避免 unsatisfiable cores[C]//International Symposium on Theo-
判断一个公式是否属于 ＭＵ（ｋ）．因为其使用了 “遍 历全部 ｋ 个子集”的策略，所以算法非常依赖参数 ｋ． Ｈ． Ｆｌｅｉｓｃｈｎｅ 等利用双边图匹配的某些相应赋值限 制寻找一个可满足的真值赋值．算法的时间复杂度 为 ｎ Ｏ（ｋ） ，精确上界 Ｏ（ｌｎ ｋ ＋ １ ／ ２）． （ｌ 为公式长度，ｎ 为公式的变量数）．Ｓ． Ｓｚｅｉｄｅ ［２２］ 提出了一个算法，并 得到一个新的结果．算法产生于 ＳＡＴ 问题的固定参 数可解问题：对于一个 ＣＮＦ 公式 Ｆ，如果其子集中 子句个数超过变量个数最多 ｋ 个， 那么 可 以 在 Ｏ（２ ｋ ｎ ３ ） 时间内判断公式 Ｆ 的可满足性．参数 ｋ 就 是 Ｆ 的最大差值，可以用图匹配算法有效计算．最 后，基于以上结论，利用图论中的最大差值和 ｑ⁃ｅｘ⁃ ｐａｎｄｉｎｇ 双边图［３０］计算出改进的结果为 Ｏ（２ ｋ ｎ ４ ） ． ３．３ ＱＢＦ 中的极小不可满足子式 近年来，ＳＡＴ 技术已经成功应用在限界模型检验 （ｂｏｕｎｄｅｄ ｍｏｄｅｌ ｃｈｅｃｋｉｎｇ，ＢＭＣ）并推广到限界的模型 检验．但是直接将基于 ＳＡＴ 的 ＢＭＣ 推广到非限界的 模型检验的方法不能克服软件规模增大导致的状态 空间爆炸问题，即模型检验过程中软件规模的增大可 能导致命题逻辑公式的长度呈指数倍的增长．带量词 的布尔公式 ＱＢＦ 作为 ＳＡＴ 公式的自然扩展具有紧凑 的空间结构和更强大、更直观的表达能力． 赵希顺等［２３］ 对 ＱＢＦ 中的极小不可满足问题 （ｍｉｎｉｍａｌ ｆａｌｓｉｔｙ，ＭＦ） 进行了研究．对不可满足的子 式研究，有可能产生新的 ＱＢＦ 求解算法．ＱＢＦ 的最 小不可满足公式 ＱＣＮＦ 指的是该公式不可满足但其 任一真子公式均可满足．一个 ＱＣＮＦ 公式的差值不 同于命题公式的差值，其差值是子句数和存在量词 之间的差值．对 ＱＣＮＦ 公式固定差值为 １ 的极小不 可满足子式可表示为 ＭＦ（１）．文献［２３］中得出重要 结论：对 ＱＣＮＦ 公式固定差值为 １ 的极小不可满足 子式可以在多项式时间有解．这个证明依赖于公式 ＭＵ（１）的结构． 对于 ＭＦ（ ｋ） （ ｋ≥２）是否存在多项 式时间可解，仍然是开放的． ４ 总结与展望 不可满足子式的研究给研究人员带了多方面的 挑战，但是也给研究人员带来多方面机会．不可满足 子式的研究出现了以下研究方面的热点． １）使用符号化技术，如 ＢＤＤ 技术能够紧凑地表 示公式，是缓解内存瓶颈的关键技术．文献［３１］借助 于 ＢＤＤ 判断公式是不可满足的并且其全部子公式 是满足的，从而证明公式是极小不可满足子式． ２）混合求解算法：每种求解策略有其自身优点 和缺点．混合求解有利于发挥各自算法的优势，避免 其缺点，尽可能提高算法的效率．例如文献［２６］中提 出了一种在 ＣＳＰ 中提取极小不可满足子式的混合 算法，这是直接算法和间接算法的混合．文献［１４］求 解最小不可满足子式可以视为贪心算法与遗传算法 的混合算法． ３）新领域中扩展：在形式验证等实际应用中， ＱＢＦ、ＣＳＰ、ＳＭＴ 都比 ＳＡＴ 表达力强．尤其 ＳＭＴ 技术 得到飞速发展，并且在验证领域获得很好的效果．研 究 ＳＭＴ 的极小不可满足子式将是未来主要方向． ４）参数复杂性：将固定差值的极小不可满足子 式转化为固定参数问题，并且求解其计算复杂性．但 是，对于 ＱＢＦ 中，ＭＦ（ ｋ） （ ｋ＞１） 是否可以在多项式 时间内判定，依然是开放的． 参考文献： ［１］ ＧＵＰＴＡ Ａ． Ｌｅａｒｎｉｎｇ ａｂｓｔｒａｃｔｉｏｎｓ ｆｏｒ ｍｏｄｅｌ ｃｈｅｃｋｉｎｇ［Ｄ］． Ｐｉｔｔｓｂｕｒｇｈ： Ｃａｒｎｅｇｉｅ Ｍｅｌｌｏｎ Ｕｎｉｖｅｒｓｉｔｙ， ２００６： １⁃１８０． ［２］Ｄｅ Ｌａ ＢＡＮＤＡ Ｍ Ｇ， ＳＴＵＣＫＥＹ Ｐ Ｊ， ＷＡＺＮＹ Ｊ． Ｆｉｎｄｉｎｇ ａｌｌ ｍｉｎｉｍａｌ ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｓｅｔｓ ［ Ｃ］ ／ ／ Ｐｒｏｃｅｅｄｉｎｇｓ ｏｆ ｔｈｅ ５ｔｈ ＡＣＭ ＳＩＧＰＬＡＮ Ｉｎｔｅｒｎａｔｉｏｎａｌ Ｃｏｎｆｅｒｅｎｃｅ ｏｎ Ｐｒｉｎｃｉｐｌｅｓ ａｎｄ Ｐｒａｃｔｉｃｅ ｏｆ Ｄｅｃｌａｒｉｔｉｖｅ Ｐｒｏｇｒａｍｍｉｎｇ． Ｎｅｗ Ｙｏｒｋ， ＵＳＡ， ２００３： ３２⁃４３． ［３］ ＯＨ Ｙ， ＭＮＥＩＭＮＥＨ Ｍ Ｎ， ＡＮＤＲＡＵＳ Ｚ Ｓ． ＡＭＵＳＥ： ａ ｍｉｎｉｍａｌｌｙ ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒｍｕｌａ ｅｘｔｒａｃｔｏｒ［Ｃ］ ／ ／ Ｐｒｏｃｅｅｄ⁃ ｉｎｇｓ ｏｆ ｔｈｅ ４１ｓｔ Ａｎｎｕａｌ Ｄｅｓｉｇｎ Ａｕｔｏｍａｔｉｏｎ Ｃｏｎｆｅｒｅｎｃｅ． Ｎｅｗ Ｙｏｒｋ， ＵＳＡ， ２００４： ５１８⁃５２３． ［４］ＬＩＦＦＩＴＯＮ Ｍ， ＳＡＫＡＬＬＡＨ Ｋ． Ｏｎ ｆｉｎｄｉｎｇ ａｌｌ ｍｉｎｉｍａｌｌｙ ｕｎ⁃ ｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒｍｕｌａｓ ［ Ｃ ］ ／ ／ Ｔｈｅｏｒｙ ａｎｄ Ａｐｐｌｉｃａｔｉｏｎｓ ｏｆ Ｓａｔｉｓｆｉａｂｉｌｉｔｙ Ｔｅｓｔｉｎｇ． Ｓｔ． Ａｎｄｒｅｗｓ， Ｓｃｏｔｌａｎｄ， ２００５： １７３⁃ １８６． ［５］ＭＡＲＱＵＥＳ⁃ＳＩＬＶＡ Ｊ， ＬＹＮＣＥ Ｉ． Ｏｎ ｉｍｐｒｏｖｉｎｇ ＭＵＳ ｅｘｔｒａｃ⁃ ｔｉｏｎ ａｌｇｏｒｉｔｈｍｓ ［ Ｍ］ ／ ／ Ｌｅｃｔｕｒｅ Ｎｏｔｅｓ ｉｎ Ｃｏｍｐｕｔｅｒ Ｓｃｉｅｎｃｅ， Ｈｅｉｄｅｌｂｅｒｇ： Ｓｐｒｉｎｇｅｒ， ２０１１， ６６９５： １５９⁃１７３． ［ ６ ］ Ｖａｎ ＭＡＡＲＥＮ Ｈ， ＷＩＥＲＩＮＧＡ Ｓ． Ｆｉｎｄｉｎｇ ｇｕａｒａｎｔｅｅｄ ＭＵＳｅｓ ｆａｓｔ［Ｍ］． Ｈｅｉｄｅｌｂｅｒｇ： Ｓｐｒｉｎｇｅｒ， ２００８： ２９１⁃３０４． ［７］ＧＲÉＧＯＩＲＥ É， ＭＡＺＵＲＥ Ｂ， ＰＩＥＴＴＥ Ｃ． Ｅｘｔｒａｃｔｉｎｇ ＭＵＳｅｓ ［Ｃ］ ／ ／ Ｐｒｏｃｅｅｄｉｎｇｓ ｏｆ ｔｈｅ １７ｔｈ Ｅｕｒｏｐｅａｎ Ｃｏｎｆｅｒｅｎｃｅ ｏｎ Ａｒ⁃ ｔｉｆｉｃｉａｌ Ｉｎｔｅｌｌｉｇｅｎｃｅ ２００６． Ｒｉｖａ ｄｅｌ Ｇａｒｄａ， Ｉｔａｌｙ， ２００６： ３８７⁃ ３９１． ［８］ＧＲÉＧＯＩＲＥ É， ＭＡＺＵＲＥ Ｂ， ＰＩＥＴＴＥ Ｃ． Ｌｏｃａｌ⁃ｓｅａｒｃｈ ｅｘ⁃ ｔｒａｃｔｉｏｎ ｏｆ ＭＵＳｅｓ［Ｊ］． Ｃｏｎｓｔｒａｉｎ， ２００７， １２（３）： ３２５⁃３４４． ［９］ＺＨＡＮＧ Ｊ， ＳＨＥＮ Ｓ， ＬＩ Ｓ． Ｆｉｎｄｉｎｇ ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒｍｕ⁃ ｌａｓ ｗｉｔｈ ｓｔｏｃｈａｓｔｉｃ ｍｅｔｈｏｄ ［ Ｍ ］． Ｈｅｉｄｅｌｂｅｒｇ： Ｓｐｒｉｎｇｅｒ， ２００７， ４８８１： ３８５⁃３９４． ［１０］ＺＨＡＮＧ Ｊ， ＳＨＥＮ Ｓ， ＬＩ Ｓ． Ａ ｈｅｕｒｉｓｔｉｃ ｌｏｃａｌ ｓｅａｒｃｈ ａｌｇｏ⁃ ｒｉｔｈｍ ｆｏｒ ｕｎｓａｔｉｓｆｉａｂｌｅ ｃｏｒｅｓ ｅｘｔｒａｃｔｉｏｎ ［ Ｍ］． Ｈｅｉｄｅｌｂｅｒｇ： Ｓｐｒｉｎｇｅｒ， ２００７， ４７０７： ６４９⁃６５９． ［１１］ ＺＨＡＮＧ Ｊ， ＳＨＥＮ Ｓ， ＬＩ Ｓ． Ｔｒａｃｋｉｎｇ ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒ⁃ ｍｕｌａｓ ｆｒｏｍ ｒｅｄｕｃｅｄ ｒｅｆｕｔａｔｉｏｎ ｐｒｏｏｆ ［ Ｊ］． Ｊｏｕｒｎａｌ ｏｆ Ｓｏｆｔ⁃ ｗａｒｅ， ２００９， ４（１）： ４２⁃４９． ［１２］ＬＹＮＣＥ Ｉ， ＭＡＲＱＵＥＳ⁃ＳＩＬＶＡ Ｊ Ｐ． Ｏｎ ｃｏｍｐｕｔｉｎｇ ｍｉｎｉｍｕｍ ｕｎｓａｔｉｓｆｉａｂｌｅ ｃｏｒｅｓ［Ｃ］ ／ ／ Ｉｎｔｅｒｎａｔｉｏｎａｌ Ｓｙｍｐｏｓｉｕｍ ｏｎ Ｔｈｅｏ⁃ 第 ６ 期 殷明浩，等：不可满足子式研究 ·５０３·
·504. 智能系统学报 第8卷 ry and Applications of Satisfiability Testing.Vancouver, [24]HAN B,LEE S J.Deriving minimal conflict sets by CS- Canada,2004:305-310. trees with mark set in diagnosis from first principles[J]. [13]LIFFITON M,MNEIMNEH M,LYNCE I,et al.A branch IEEE Transactions on Systems,Man,and Cybernetics, and bound algorithm for extracting smallest minimal unsati- 1999.29(2)：281-286. sfiable subformulas[J].Constraints,2009,14(4):415- [25]BAILEY J,STUCKEY P J.Discovery of minimal unsatisfi- 442. able subsets of constraints using hitting set dualization [14]ZHANG Jianmin,SHEN Shengyu,LI Sikun.Algorithms for [M].Heidelberg:Springer,2005:174-186. deriving minimum unsatisfiable Boolean subformulae[J]. [26]SHAH I.A hybrid algorithm for finding minimal unsatisfi- Acta Electronica Sinica,2009,37(5):993-999. able subsets in over-constrained CSPs[J].International [15]CIMATTI A,GRIGGIO A,SEBASTIANI R.A simple and Journal of Intelligent Systems,2011,26(11):1023-1048. flexible way of computing small unsatisfiable cores in SAT [27]Van MAAREN H.Pivoting algorithms based on Boolean modulo theories[M].Heidelberg:Springer,2007,4501: vector labeling[J].Acta Mathematica Vietnamica,1997, 334-339. 22(1):183-198. [16]CIMATTI A,GRIGGIO A,SEBASTIANI R.Computing [28]DAVYDOV G,DAVYDOVA I,BONING H K.An effi- small unsatisfiable cores in satisfiability modulo theories cient algorithm for the minimal unsatisfiability problem for [J].Journal of Artificial Intelligence Research,2011, a subclass of CNF[J].Annals of Mathematics and Artifi- 40:701-728. cial Intelligence,1998,23:229-245. [17]ZHANG Jianmin,SHEN Shengyu,ZHANG Jun,et al.Ex- [29]TORAN J.Complexity classes defined by counting quantifi- tracting minimal unsatisfiable subformulas in satisfiability ers[J].Journal of the ACM,1991,38(3)753-774. modulo theoriesJ.Computer Science and Information [30]LOVASZ L,PLUMMER M D.Matching theory[M].Am- Systems,2011,8:693-710. sterdam:North-Holland Publishing,1986:29. [18]ZHANG Jianmin,SHEN Shengyu,LI Sikun.An algorithm [31]HUANG J P.MUP:a minimally unsatisfiability prover for extracting minimal unsatisfiable subformulae in first-or- [C]//Proceedings of the 10th Asia and South Pacific De- der logic based on refutation implication[J].Chinese Jour- sign Automation Conference.Shanghai,China,2005: nal of Conputers,2010,33(3):415-426. 432-437. [19]BU NING H K,ZHAO X.On the structure of some classes 作者简介： of minimal unsatisfiable formulas[J].Discrete Applied 殷明浩，男，1979年生，主要研究方 Mathematics,2003,130(2):185-207. 向为自动推理和智能规划.主持过多项 [20]BU NING H K,ZHAO X.The complexity of some subclas- 国家自然科学基金等项目，发表学术论 ses of minimal unsatisable formulas[J].Journal on Satisfi- 文多篇，其中被SCI检索20余篇。 ability Boolean Modeling and Computation,2007,3:1-17. [21]FLEISCHNER H,KULLMANN O,SZEIDER S.Polyno- mial-time recognition of minimal unsatisable formulas with fxed clause-variable difference[J].Theoretical Computer Science,2002,289(1):503-516. 李欣，男，1982年生，硕士研究生， [22 SZEIDER S.Minimal unsatisable formulas with bounded 主要研究领域为自动推理和智能规划。 clause-variable difference are fixed-parameter tractable 发表学术论文多篇. [M].Heidelberg:Springer,2003:548-558. [23 B0 NING H,ZHAO X.Minimal false quantified Boolean formulas[M].Heidelberg:Springer,2006:339-352
ｒｙ ａｎｄ Ａｐｐｌｉｃａｔｉｏｎｓ ｏｆ Ｓａｔｉｓｆｉａｂｉｌｉｔｙ Ｔｅｓｔｉｎｇ． Ｖａｎｃｏｕｖｅｒ， Ｃａｎａｄａ， ２００４： ３０５⁃３１０． ［１３］ＬＩＦＦＩＴＯＮ Ｍ， ＭＮＥＩＭＮＥＨ Ｍ， ＬＹＮＣＥ Ｉ， ｅｔ ａｌ． Ａ ｂｒａｎｃｈ ａｎｄ ｂｏｕｎｄ ａｌｇｏｒｉｔｈｍ ｆｏｒ ｅｘｔｒａｃｔｉｎｇ ｓｍａｌｌｅｓｔ ｍｉｎｉｍａｌ ｕｎｓａｔｉ⁃ ｓｆｉａｂｌｅ ｓｕｂｆｏｒｍｕｌａｓ［ Ｊ］． Ｃｏｎｓｔｒａｉｎｔｓ， ２００９， １４（４）： ４１５⁃ ４４２． ［１４］ＺＨＡＮＧ Ｊｉａｎｍｉｎ，ＳＨＥＮ Ｓｈｅｎｇｙｕ， ＬＩ Ｓｉｋｕｎ． Ａｌｇｏｒｉｔｈｍｓ ｆｏｒ ｄｅｒｉｖｉｎｇ ｍｉｎｉｍｕｍ ｕｎｓａｔｉｓｆｉａｂｌｅ Ｂｏｏｌｅａｎ ｓｕｂｆｏｒｍｕｌａｅ ［ Ｊ］． Ａｃｔａ Ｅｌｅｃｔｒｏｎｉｃａ Ｓｉｎｉｃａ， ２００９， ３７（５）： ９９３⁃９９９． ［１５］ＣＩＭＡＴＴＩ Ａ， ＧＲＩＧＧＩＯ Ａ， ＳＥＢＡＳＴＩＡＮＩ Ｒ． Ａ ｓｉｍｐｌｅ ａｎｄ ｆｌｅｘｉｂｌｅ ｗａｙ ｏｆ ｃｏｍｐｕｔｉｎｇ ｓｍａｌｌ ｕｎｓａｔｉｓｆｉａｂｌｅ ｃｏｒｅｓ ｉｎ ＳＡＴ ｍｏｄｕｌｏ ｔｈｅｏｒｉｅｓ［Ｍ］． Ｈｅｉｄｅｌｂｅｒｇ： Ｓｐｒｉｎｇｅｒ， ２００７， ４５０１： ３３４⁃３３９． ［１６］ ＣＩＭＡＴＴＩ Ａ， ＧＲＩＧＧＩＯ Ａ， ＳＥＢＡＳＴＩＡＮＩ Ｒ． Ｃｏｍｐｕｔｉｎｇ ｓｍａｌｌ ｕｎｓａｔｉｓｆｉａｂｌｅ ｃｏｒｅｓ ｉｎ ｓａｔｉｓｆｉａｂｉｌｉｔｙ ｍｏｄｕｌｏ ｔｈｅｏｒｉｅｓ ［Ｊ］． Ｊｏｕｒｎａｌ ｏｆ Ａｒｔｉｆｉｃｉａｌ Ｉｎｔｅｌｌｉｇｅｎｃｅ Ｒｅｓｅａｒｃｈ， ２０１１， ４０： ７０１⁃７２８． ［１７］ＺＨＡＮＧ Ｊｉａｎｍｉｎ， ＳＨＥＮ Ｓｈｅｎｇｙｕ， ＺＨＡＮＧ Ｊｕｎ， ｅｔ ａｌ． Ｅｘ⁃ ｔｒａｃｔｉｎｇ ｍｉｎｉｍａｌ ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒｍｕｌａｓ ｉｎ ｓａｔｉｓｆｉａｂｉｌｉｔｙ ｍｏｄｕｌｏ ｔｈｅｏｒｉｅｓ ［ Ｊ ］． Ｃｏｍｐｕｔｅｒ Ｓｃｉｅｎｃｅ ａｎｄ Ｉｎｆｏｒｍａｔｉｏｎ Ｓｙｓｔｅｍｓ， ２０１１， ８： ６９３⁃７１０． ［１８］ＺＨＡＮＧ Ｊｉａｎｍｉｎ， ＳＨＥＮ Ｓｈｅｎｇｙｕ， ＬＩ Ｓｉｋｕｎ． Ａｎ ａｌｇｏｒｉｔｈｍ ｆｏｒ ｅｘｔｒａｃｔｉｎｇ ｍｉｎｉｍａｌ ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒｍｕｌａｅ ｉｎ ｆｉｒｓｔ⁃ｏｒ⁃ ｄｅｒ ｌｏｇｉｃ ｂａｓｅｄ ｏｎ ｒｅｆｕｔａｔｉｏｎ ｉｍｐｌｉｃａｔｉｏｎ［Ｊ］． Ｃｈｉｎｅｓｅ Ｊｏｕｒ⁃ ｎａｌ ｏｆ Ｃｏｎｐｕｔｅｒｓ， ２０１０， ３３（３）： ４１５⁃４２６． ［１９］ＢÜ ＮＩＮＧ Ｈ Ｋ， ＺＨＡＯ Ｘ． Ｏｎ ｔｈｅ ｓｔｒｕｃｔｕｒｅ ｏｆ ｓｏｍｅ ｃｌａｓｓｅｓ ｏｆ ｍｉｎｉｍａｌ ｕｎｓａｔｉｓｆｉａｂｌｅ ｆｏｒｍｕｌａｓ ［ Ｊ ］． Ｄｉｓｃｒｅｔｅ Ａｐｐｌｉｅｄ Ｍａｔｈｅｍａｔｉｃｓ， ２００３， １３０（２）： １８５⁃２０７． ［２０］ＢÜ ＮＩＮＧ Ｈ Ｋ， ＺＨＡＯ Ｘ． Ｔｈｅ ｃｏｍｐｌｅｘｉｔｙ ｏｆ ｓｏｍｅ ｓｕｂｃｌａｓ⁃ ｓｅｓ ｏｆ ｍｉｎｉｍａｌ ｕｎｓａｔｉｓａｂｌｅ ｆｏｒｍｕｌａｓ［Ｊ］． Ｊｏｕｒｎａｌ ｏｎ Ｓａｔｉｓｆｉ⁃ ａｂｉｌｉｔｙ Ｂｏｏｌｅａｎ Ｍｏｄｅｌｉｎｇ ａｎｄ Ｃｏｍｐｕｔａｔｉｏｎ， ２００７， ３： １⁃１７． ［２１］ ＦＬＥＩＳＣＨＮＥＲ Ｈ， ＫＵＬＬＭＡＮＮ Ｏ， ＳＺＥＩＤＥＲ Ｓ． Ｐｏｌｙｎｏ⁃ ｍｉａｌ⁃ｔｉｍｅ ｒｅｃｏｇｎｉｔｉｏｎ ｏｆ ｍｉｎｉｍａｌ ｕｎｓａｔｉｓａｂｌｅ ｆｏｒｍｕｌａｓ ｗｉｔｈ ｆｘｅｄ ｃｌａｕｓｅ⁃ｖａｒｉａｂｌｅ ｄｉｆｆｅｒｅｎｃｅ ［ Ｊ］． Ｔｈｅｏｒｅｔｉｃａｌ Ｃｏｍｐｕｔｅｒ Ｓｃｉｅｎｃｅ， ２００２， ２８９（１）： ５０３⁃５１６． ［２２］ ＳＺＥＩＤＥＲ Ｓ． Ｍｉｎｉｍａｌ ｕｎｓａｔｉｓａｂｌｅ ｆｏｒｍｕｌａｓ ｗｉｔｈ ｂｏｕｎｄｅｄ ｃｌａｕｓｅ⁃ｖａｒｉａｂｌｅ ｄｉｆｆｅｒｅｎｃｅ ａｒｅ ｆｉｘｅｄ⁃ｐａｒａｍｅｔｅｒ ｔｒａｃｔａｂｌｅ ［Ｍ］． Ｈｅｉｄｅｌｂｅｒｇ： Ｓｐｒｉｎｇｅｒ， ２００３： ５４８⁃５５８． ［２３］ＢÜ ＮＩＮＧ Ｈ， ＺＨＡＯ Ｘ． Ｍｉｎｉｍａｌ ｆａｌｓｅ ｑｕａｎｔｉｆｉｅｄ Ｂｏｏｌｅａｎ ｆｏｒｍｕｌａｓ［Ｍ］． Ｈｅｉｄｅｌｂｅｒｇ： Ｓｐｒｉｎｇｅｒ， ２００６： ３３９⁃３５２． ［２４］ ＨＡＮ Ｂ， ＬＥＥ Ｓ Ｊ． Ｄｅｒｉｖｉｎｇ ｍｉｎｉｍａｌ ｃｏｎｆｌｉｃｔ ｓｅｔｓ ｂｙ ＣＳ⁃ ｔｒｅｅｓ ｗｉｔｈ ｍａｒｋ ｓｅｔ ｉｎ ｄｉａｇｎｏｓｉｓ ｆｒｏｍ ｆｉｒｓｔ ｐｒｉｎｃｉｐｌｅｓ［ Ｊ］． ＩＥＥＥ Ｔｒａｎｓａｃｔｉｏｎｓ ｏｎ Ｓｙｓｔｅｍｓ， Ｍａｎ， ａｎｄ Ｃｙｂｅｒｎｅｔｉｃｓ， １９９９， ２９（２）： ２８１⁃２８６． ［２５］ＢＡＩＬＥＹ Ｊ， ＳＴＵＣＫＥＹ Ｐ Ｊ． Ｄｉｓｃｏｖｅｒｙ ｏｆ ｍｉｎｉｍａｌ ｕｎｓａｔｉｓｆｉ⁃ ａｂｌｅ ｓｕｂｓｅｔｓ ｏｆ ｃｏｎｓｔｒａｉｎｔｓ ｕｓｉｎｇ ｈｉｔｔｉｎｇ ｓｅｔ ｄｕａｌｉｚａｔｉｏｎ ［Ｍ］． Ｈｅｉｄｅｌｂｅｒｇ： Ｓｐｒｉｎｇｅｒ， ２００５： １７４⁃１８６． ［２６］ＳＨＡＨ Ｉ． Ａ ｈｙｂｒｉｄ ａｌｇｏｒｉｔｈｍ ｆｏｒ ｆｉｎｄｉｎｇ ｍｉｎｉｍａｌ ｕｎｓａｔｉｓｆｉ⁃ ａｂｌｅ ｓｕｂｓｅｔｓ ｉｎ ｏｖｅｒ⁃ｃｏｎｓｔｒａｉｎｅｄ ＣＳＰｓ ［ Ｊ］． Ｉｎｔｅｒｎａｔｉｏｎａｌ Ｊｏｕｒｎａｌ ｏｆ Ｉｎｔｅｌｌｉｇｅｎｔ Ｓｙｓｔｅｍｓ， ２０１１， ２６（１１）： １０２３⁃１０４８． ［２７］ Ｖａｎ ＭＡＡＲＥＮ Ｈ． Ｐｉｖｏｔｉｎｇ ａｌｇｏｒｉｔｈｍｓ ｂａｓｅｄ ｏｎ Ｂｏｏｌｅａｎ ｖｅｃｔｏｒ ｌａｂｅｌｉｎｇ［ Ｊ］． Ａｃｔａ Ｍａｔｈｅｍａｔｉｃａ Ｖｉｅｔｎａｍｉｃａ， １９９７， ２２（１）： １８３⁃１９８． ［２８］ ＤＡＶＹＤＯＶ Ｇ， ＤＡＶＹＤＯＶＡ Ｉ， ＢÜＮＩＮＧ Ｈ Ｋ． Ａｎ ｅｆｆｉ⁃ ｃｉｅｎｔ ａｌｇｏｒｉｔｈｍ ｆｏｒ ｔｈｅ ｍｉｎｉｍａｌ ｕｎｓａｔｉｓｆｉａｂｉｌｉｔｙ ｐｒｏｂｌｅｍ ｆｏｒ ａ ｓｕｂｃｌａｓｓ ｏｆ ＣＮＦ［ Ｊ］． Ａｎｎａｌｓ ｏｆ Ｍａｔｈｅｍａｔｉｃｓ ａｎｄ Ａｒｔｉｆｉ⁃ ｃｉａｌ Ｉｎｔｅｌｌｉｇｅｎｃｅ， １９９８， ２３： ２２９⁃２４５． ［２９］ＴＯＲＡＮ Ｊ． Ｃｏｍｐｌｅｘｉｔｙ ｃｌａｓｓｅｓ ｄｅｆｉｎｅｄ ｂｙ ｃｏｕｎｔｉｎｇ ｑｕａｎｔｉｆｉ⁃ ｅｒｓ［Ｊ］． Ｊｏｕｒｎａｌ ｏｆ ｔｈｅ ＡＣＭ， １９９１， ３８（３）： ７５３⁃７７４． ［３０］ＬＯＶＡＳＺ Ｌ， ＰＬＵＭＭＥＲ Ｍ Ｄ． Ｍａｔｃｈｉｎｇ ｔｈｅｏｒｙ［Ｍ］． Ａｍ⁃ ｓｔｅｒｄａｍ： Ｎｏｒｔｈ⁃Ｈｏｌｌａｎｄ Ｐｕｂｌｉｓｈｉｎｇ， １９８６： ２９． ［３１］ ＨＵＡＮＧ Ｊ Ｐ． ＭＵＰ： ａ ｍｉｎｉｍａｌｌｙ ｕｎｓａｔｉｓｆｉａｂｉｌｉｔｙ ｐｒｏｖｅｒ ［Ｃ］ ／ ／ Ｐｒｏｃｅｅｄｉｎｇｓ ｏｆ ｔｈｅ １０ｔｈ Ａｓｉａ ａｎｄ Ｓｏｕｔｈ Ｐａｃｉｆｉｃ Ｄｅ⁃ ｓｉｇｎ Ａｕｔｏｍａｔｉｏｎ Ｃｏｎｆｅｒｅｎｃｅ． Ｓｈａｎｇｈａｉ， Ｃｈｉｎａ， ２００５： ４３２⁃４３７． 作者简介： 殷明浩，男，１９７９ 年生，主要研究方 向为自动推理和智能规划． 主持过多项 国家自然科学基金等项目，发表学术论 文多篇，其中被 ＳＣＩ 检索 ２０ 余篇． 李欣，男，１９８２ 年生，硕士研究生， 主要研究领域为自动推理和智能规划． 发表学术论文多篇． ·５０４· 智 能 系 统 学 报 第 ８ 卷