第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 小不可满足子式可以更好地解释不可满足的根源所第 ８ 卷第 ６ 期 智 能 系 统 学 报 Ｖｏｌ．８ №．６ ２０１３ 年 １２ 月 ＣＡＡＩ Ｔｒａｎｓａｃｔｉｏｎｓ ｏｎ Ｉｎｔｅｌｌｉｇｅｎｔ Ｓｙｓｔｅｍｓ Ｄｅｃ． ２０１３ ＤＯＩ：１０．３９６９ ／ ｊ．ｉｓｓｎ．１６７３⁃４７８５．２０１２１２０５８ 网络出版地址：ｈｔｔｐ： ／ ／ ｗｗｗ．ｃｎｋｉ．ｎｅｔ ／ ｋｃｍｓ／ ｄｅｔａｉｌ ／ ２３．１５３８．ＴＰ．２０１３１０１２．１８１３．００２．ｈｔｍｌ 不可满足子式研究 殷明浩，李欣 （东北师范大学 计算机科学与信息技术学院，吉林 长春 １３０１１７） 摘 要：为了广泛有效地将不可满足子式应用于知识验证、产品规划、硬件和软件的设计与验证等领域，对不可满足 子式进行了相关研究．对当前不可满足子式的主要相关算法进行了概述评论、分类归纳，并从计算复杂性角度介绍了 其子类、参数复杂性以及 ＱＢＦ 中的极小不可满足子式．总结了近 １０ 年来不可满足子式的理论与算法，讨论了不可满 足子式的未来研究发展方向．研究有利于进一步发现不可满足的根本原因，从而进行有针对性地改进，并对相关人员 的研究提供帮助． 关键词：可满足性问题；不可满足子式；可满足模理论；局部搜索 中图分类号：ＴＰ３１１ 文献标志码：Ａ 文章编号：１６７３⁃４７８５（２０１３）０６⁃０４９７⁃０８ 中文引用格式：殷明浩，李欣． 不可满足子式研究［Ｊ］． 智能系统学报， ２０１３， ８（６）： ４９７⁃５０４． 英文引用格式：ＹＩＮ Ｍｉｎｇｈａｏ， ＬＩ Ｘｉｎ． Ｒｅｓｅａｒｃｈ ｏｎ ａｎ ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒｍｕｌａ［ Ｊ］． ＣＡＡＩ Ｔｒａｎｓａｃｔｉｏｎｓ ｏｎ Ｉｎｔｅｌｌｉｇｅｎｔ Ｓｙｓｔｅｍｓ， ２０１３， ８（６）： ４９７⁃５０４． Ｒｅｓｅａｒｃｈ ｏｎ ａｎ ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒｍｕｌａ ＹＩＮ Ｍｉｎｇｈａｏ， ＬＩ Ｘｉｎ （Ｓｃｈｏｏｌ ｏｆ Ｃｏｍｐｕｔｅｒ Ｓｃｉｅｎｃｅ ａｎｄ Ｉｎｆｏｒｍａｔｉｏｎ Ｔｅｃｈｎｏｌｏｇｙ， Ｎｏｒｔｈｅａｓｔ Ｎｏｒｍａｌ Ｕｎｉｖｅｒｓｉｔｙ， Ｃｈａｎｇｃｈｕｎ １３０１１７， Ｃｈｉｎａ） Ａｂｓｔｒａｃｔ：Ｉｎ ｒｅｃｅｎｔ ｙｅａｒｓ， ａｎ ｉｎｃｒｅａｓｉｎｇ ｎｕｍｂｅｒ ｏｆ ｒｅｓｅａｒｃｈｅｒｓ ｈａｖｅ ｓｔａｒｔｅｄ ｔｏ ｆｏｃｕｓ ｔｈｅｉｒ ａｔｔｅｎｔｉｏｎ ｏｎ ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒｍｕｌａｓ， ｅｓｐｅｃｉａｌｌｙ ｉｎ ｒｅｇａｒｄｓ ｔｏ ｔｈｅ ｅｘｔｒｅｍｅｌｙ ｓｍａｌｌ ａｎｄ ｔｈｅ ｍｉｎｉｍａｌ ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒｍｕｌａｓ． Ｔｈｅ ｕｎｓａｔｉｓｆｉ⁃ ａｂｌｅ ｓｕｂｆｏｒｍｕｌａ （ＵＳ） ｈａｓ ａ ｗｉｄｅ ｒａｎｇｅ ｏｆ ｐｒａｃｔｉｃａｌ ａｐｐｌｉｃａｔｉｏｎｓ， ｉｎｃｌｕｄｉｎｇ ｋｎｏｗｌｅｄｇｅ ｖａｌｉｄａｔｉｏｎ， ｐｒｏｄｕｃｔ ｐｒｏ⁃ ｇｒａｍｓ， ａｎｄ ｄｅｓｉｇｎ ａｎｄ ｖｅｒｉｆｉｃａｔｉｏｎ ｏｆ ｈａｒｄｗａｒｅ ａｎｄ ｓｏｆｔｗａｒｅ． Ａｎ ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒｍｕｌａ ｍａｙ ｂｅ ｖｅｒｙ ｈｅｌｐｆｕｌ ｉｎ ｄｉ⁃ ａｇｎｏｓｉｎｇ ｔｈｅ ｃａｕｓｅｓ ｏｆ ｕｎｆｅａｓｉｂｉｌｉｔｙ ｉｎ ｌａｒｇｅ ｓｙｓｔｅｍｓ． Ｉｎ ｔｈｅ ｐａｓｔ １０ ｙｅａｒｓ， ｒｅｓｅａｒｃｈ ｏｎ ａｎ ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒｍｕｌａ ｈａｓ ｂｅｅｎ ｄｅｖｅｌｏｐｅｄ ｑｕｉｃｋｌｙ． Ｉｎ ｔｈｉｓ ｐａｐｅｒ， ｔｈｅ ａｕｔｈｏｒｓ ｄｉｓｃｕｓｓ ｔｈｅ ａｌｇｏｒｉｔｈｍ ｉｎ ｒｅｌａｔｉｏｎ ｔｏ ａｎ ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒ⁃ ｍｕｌａ， ｉｎｔｒｏｄｕｃｅ ｔｈｅ ｓｕｂｃａｔｅｇｏｒｙ ｏｆ ａｎ ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒｍｕｌａ ｆｒｏｍ ｔｈｅ ｖｉｅｗｐｏｉｎｔ ｏｆ ｃａｌｃｕｌａｔｉｏｎ ｃｏｍｐｌｅｘｉｔｙ， ｐａｒａｍ⁃ ｅｔｅｒ ｃｏｍｐｌｅｘｉｔｙ ａｎｄ ｔｈｅ ｒｅｓｅａｒｃｈ ｏｎ ａｎ ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒｍｕｌａ ｉｎ ＱＢＦ． Ｆｉｎａｌｌｙ， ｔｈｅ ａｕｔｈｏｒｓ ｄｉｓｃｕｓｓ ｔｈｅ ｆｕｔｕｒｅ ｄｉ⁃ ｒｅｃｔｉｏｎ ｏｆ ｒｅｓｅａｒｃｈ ｏｎ ａｎ ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒｍｕｌａ． Ｋｅｙｗｏｒｄｓ：ｓａｔｉｓｆｉａｂｉｌｉｔｙ ｐｒｏｂｌｅｍ； ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒｍｕｌａ； ｓａｔｉｓｆｉａｂｉｌｉｔｙ ｍｏｄｕｌｅ ｔｈｅｏｒｙ； ｌｏｃａｌ ｓｅａｒｃｈ 收稿日期：２０１２⁃１２⁃２７． 网络出版日期：２０１３⁃１０⁃１２． 基金项目：国家自然科学基金资助项目（６１０７００８４，６０８０３０１２）． 通信作者：殷明浩． Ｅ⁃ｍａｉｌ： ｙｍｈ＠ ｎｅｎｕ．ｅｄｕ．ｃｎ． 可满足性问题（ｓａｔｉｓｆｉａｂｉｌｉｔｙ ｐｒｏｂｌｅｍ， ＳＡＴ）是当 前人们研究得最多的约束可满足性问题，也是当今 计算机科学和人工智能研究的核心问题．在实际应 用领域中的很多问题，例如等价性检查、大规模集成 电路的自动布线、自动测试向量生成、硬件与软件的 属性验证等都可转化为约束可满足问题，即能够归 约为一阶逻辑公式或命题逻辑．然而，仅仅判断命题 逻辑的可满足性是无法满足实际要求的．当公式不 可满足时，为了查找不可满足的原因，往往要删除无 关子句进而提取不可满足子式．目前，研究人员对不 可满足子式的算法研究和相应计算的复杂性表现出 了极大兴趣．寻找最小不可满足子式的决策问题是 ∑２ ⁃ｃｏｍｐｌｅｔｅ 问题［１］ ，寻找一个极小不可满足子式 是 Ｄ ｐ ⁃ｃｏｍｐｌｅｔｅ 问 题． 目 前 有 很 多 算 法 是 关 于 极 小［２⁃１１］和最小不可满足子式［１２⁃１４］ 的提取，这些提取 不可满足子式的算法主要应用于形式验证领域．极 小不可满足子式可以更好地解释不可满足的根源所