.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不可满足子式，其约束的有关子 显然，对于同一个问题实例，可能存在不同的不 集是不可满足的，并且其真子集是可满足的.在，最小不可满足子式可以精确地定位错误原因，但 是其求解难度极大． 随着 ＳＭＴ （ ｓａｔｉｓｆｉａｂｉｌｉｔｙ ｍｏｄｕｌｏ ｔｈｅｏｒｉｅｓ）技术的不断发展，它开始逐渐取代 ＳＡＴ．相 对于 ＳＡＴ，ＳＭＴ 具有更好的抽象能力，更接近于高层 设计，极具发展潜力．它使用字级建模，不必像 ＳＡＴ 那样将问题转化为位级处理，从而减少了空间和时 间的开销．ＳＭＴ 可以看作是 ＳＡＴ 问题的一个扩展， 它极大地补充了 ＳＡＴ 的不足之处．求解其极小不可 满足子式算法也极具实际意义．ＳＭＴ 技术是近几年 发展起来的，目前提取 ＳＭＴ 中极小不可满足子式的 算法比较少． Ｃｉｍａｔｔｉ ［１５⁃１６］ 提出了一个新颖的方式 ｌｅｍｍａ⁃Ｌｉｆｔ 来提取 ＳＭＴ 极小不可满足子式； 张建 民［１７］提出了基于 ＤＰＬＬ（Ｔ）的深度优先搜索的极小 ＳＭＴ 不可满足子式求解算法 ＤＦＳ⁃ＭＵＳＥ 和宽度优 先搜索的极小 ＳＭＴ 不可满足子式的求解算法 ＢＦＳ⁃ ＭＵＳＥ．２０１０ 年，他又提出了基于冲突分析与否证蕴 含的 极 小 ＳＭＴ 不 可 满 足 子 式 求 解 算 法 ＣＡＲＩ⁃ ＭＵＳＥ ［１８］ ，该算法的效果明显好于 ＤＦＳ⁃ＭＵＳＥ 算法， 性能随着时间复杂度的增加更加明显． 研究不可满足子式的复杂性对不可满足子式求 解算法也极具重大意义．Ｈ．Ｋ．Ｂüｎｉｎｇ 和赵希顺［１９］ 对 不可满足的子类进行了研究，介绍了各子类的特性， 并在文献中对子 类 的 复 杂 性 进 行 了 证 明［２０］ ． Ｈ． Ｆｌｅｉｓｃｈｎｅ ［２１］ 、Ｓ． Ｓｚｅｉｄｅ ［２２］ 将固定参数的概念与极小 不可满足子式中固定差值概念相关联，证明了固定 参数的极小不可满足子式的计算复杂性．带量词的 布尔公式 ＱＢＦ 作 ＳＡＴ 公式的自然扩展具有紧凑的 空间结构以及更强大、更直观的表达能力，对 ＱＢＦ 中极小不可满足子式的研究有利于探索新的 ＱＢＦ 算法．赵希顺［２３］ 证明了 ＱＢＦ 中，对 ＱＣＮＦ 公式固定 差值为 １ 的极小不可满足子式可以在多项式时间内 有解． １ 相关定义 在计算机科学领域，不可满足子式的研究最初 源于 ＳＡＴ 问题，首先介绍本文涉及的相关概念． 定义 １ 命题可满足性问题． 给定一个 ＣＮＦ 表达式 Ｆ 和一个变量集合｛Ｖ ＝ ｘ１ ，ｘ２ ，ｘ３ ｝．如果变量集合 Ｖ 中的一组赋值使得表达 式 Ｆ 的值为真，那么称表达式 Ｆ 是可满足的；否则， 表达式 Ｆ 为不可满足． 定义 ２ 不可满足子式／ 不可满足核（ＵＳ ／ ＵＣ）． 对于一个公式 φ ， ϕ 是 φ 的一个不可满足子 式，当且仅当 φ 是不可满足的，且 ϕ ⊆ φ ． 显然，对于同一个问题实例，可能存在不同的不 可满足子式，每个不可满足子式的子句数也可能不 同．其中一些不可满足子式可能是其他不可满足子 式的子集．在最坏情况下，不可满足子式就是原始公 式本身． 定义 ３ 极小不可满足子式． 对于一个不可满足的公式 φ 的一个不可满足子 式 ϕ ，那么 φ 是极小不可满足子式，当且仅当 ∀ ϕ ∈ φ ，使得 ϕ 是可满足的． 定义 ４ 最小不可满足子式． 给出一个不可满足的公式 φ 以及 φ 的所有不可 满足子式构成的集合 ｛ϕ１ ，ϕ２ ，…，ϕｎ ｝ ，如果 ϕｋ ∈ ｛ϕ１ ，ϕ２ ，…，ϕｎ ｝ 是 最 小 不 可 满 子 式， 当 且 仅 当 ∀ϕｉ ∈｛ϕ１ ，ϕ２ ，…，ϕｎ ｝ ， １ ≤ ｉ ≤ ｎ ， 使 得 ｜ ϕｋ ｜ ≤｜ ϕｉ ｜ ． 定义 ５ 量化布尔公式⁃ＱＢＦ 问题． 一个 ＱＣＮＦ 公式 φ ＝ Ｑ１ ｘ１Ｑ２ ｘ２…Ｑｎ ｘｎϕ ，其中 Ｑｉ ∈｛∃，∀｝ ， ϕ 是一个 ＣＮＦ 公式，用矩阵形式表 达 φ ． ｘ １ ， ｘ ２ ，…， ｘｎ 分别被 Ｑ１ ，Ｑ２ ，…，Ｑｎ 量化．有 时，可以简写为 φ ＝ Ｑϕ ． 定义 ６ ＱＢＦ 极小不可满足子式（ＭＦ）． 当且仅当 φ 是不可满足的，并且从 φ 中移出任 何一个子句将导致公式变为可满足，一个 ＱＢＦ 公式 φ 被称为极小不满足，不可满足子式的子式可以表 示为 ＭＦ（ｍｉｎｉｍａｌ ｆａｌｓｅ ｆｏｒｍｕｌａｓ）． 定义 ７ 可满足性模理论（ＳＭＴ）． ＳＭＴ 是 ＳＡＴ 的一种扩展，其命题不仅包括布尔 公式，还包括其他特定理论中的一阶逻辑约束，如整 数与实数算术类型、位向量、递归及数据类型等． 定义 ８ ＳＭＴ 不可满足子式． 给出一个不可满足的无量词一阶逻辑公式 φ， 当且仅当 ϕ 是不可满足的，并且 ϕ ⊆ φ ， ϕ 是公式 φ 的一个 ＳＭＴ 不可满足子式． 定义 ９ 极小 ＳＭＴ 不可满足子式． 给出不可满足的无量词一阶逻辑公式 φ ，及其 一个不可满足子式 ϕ ，那么 ϕ 是极小 ＳＭＴ 不可满足 子式，当且仅当 ∀ ϕ ∈ φ ，使得 ϕ 是可满足的． 定义 １０ 约束可满足问题（ＣＳＰ）． 由一个变量集合和一个约束集合组成．问题的一 个状态是由对一些或全部变量的一个赋值定义的完 全赋值：每个变量都参与的赋值．问题的解是满足所 有约束的完全赋值，或更进一步，使目标函数最大化． 定义 １１ 极小 ＣＳＰ 不可满足子式． 一个极小 ＣＳＰ 不可满足子式，其约束的有关子 集是不可满足的，并且其真子集是可满足的． ·４９８· 智 能 系 统 学 报 第 ８ 卷