·4 智能系统学报 第9卷 句集扩展出来，子句集中必须有子句包含于该极大 2)极大项覆盖方法。 项（子句看作文字集合）。基于该性质，孙吉贵等提 为了避开容斥原理求解的复杂性，Yin等[2]从 出了一种新的基于扩展规则的定理证明方法NER, 相对极大项角度提出了一种基于极大项覆盖的有效 该方法将SAT问题转化为一系列文字集合的包含 SAT求解方法MC(maxterm covering for satisfiabili- 问题。NER算法按照一定次序判断极大项是否可 y)。子句C关于子句集Σ覆盖的相对极大项是C 被当前待判定的子句集Σ扩展，若存在某个极大项 覆盖，但不是Σ覆盖的极大项，表示为 不能被扩展出来，那么Σ是可满足的：否则，若所有 relativeMaxterm(C,)=MC(C)IMC()。设子句 极大项都可以被扩展出来，则Σ是不可满足的。其 集={C1,C2,C,C4{,C关于Σ的相对极大项如 最优和最坏时间复杂度分别为O(m+n×k2)和 图1所示。 O(2×(m+n×k2)),m、n、k分别表示子句集中变量 的个数、子句的个数和子句的平均长度。实验结果 表明，无论是对于随机问题还是标准测试用例，NER 算法的执行效率较ER和DR算法都有很大的提 高，有些问题可以提高2个数量级。 NER算法将所有极大项按照一定顺序来一一 判定其是否能由子句集扩展出来，直到某个极大项 不能被扩展时或者所有极大项都可由子句集扩展出 来时，才能判定出子句集的可满足性。事实上，当一 个极大项可由某一子句扩展时，接下来的部分极大 relativeMaxterm 项可以不用判断其是否可由子句集扩展出来，从而 (C 减少了需要判断的极大项个数。张立明等2定义 图1C关于的相对极大项 了半扩展规则，并且提出了基于半扩展规则的定理 Fig.1 The relative maxterm of C with respect to 证明方法SRE(semi-extension rule)。SRE算法是在 给定一个变量集合，设所有极大项集合为论域， NER算法的基础上，按一定顺序判定极大项是否可 那么空子句ε覆盖的极大项集合等于该论域。根据 被子句集扩展，当一个极大项可被子句集中的某一 扩展规则方法可知，如果MC()=MC(ε)，则子句 子句扩展时，那么基于此子句半扩展出的所有极大 集∑是不可满足的：如果relativeMaxterm(e,)≠ 项都不需判断其是否可被子句集扩展，这样减少了 ☑，则Σ是可满足的。图2给出了一个可满足的问 需要判断的极大项个数，使计算复杂度由原来NER 题实例。 方法的0(2"×(m+n×k2))降为0(2×(m+n×k2)+ n),其中d为子句集中子句的度的平均值。d越 小，SRE算法的求解效率越高：当d趋近与m时， SRE算法的求解效率较NER算法提高较小。 进一步，他们提出了基于半扩展规则的并行定 理证明方法PPSER(parallel theorem proving algo- rithm based on semi-extension rule)[2a,该方法首先 给出在极大项子空间中判定子句集可满足性的算法 PSER,然后将子句集的极大项空间分解为若干个互 不相交的子空间，对每个极大项子空间，并行地调用 MC relativeMaxterm(a,) PSER方法进行判定，如果有一个极大项子空间中 返回的结果为SAT,即该子空间中存在某个极大项 图2一个可满足问题实例 不能被扩展出来，则子句集是可满足的：否则，如果 Fig.2 A satisfiable example 所有极大项子空间返回的结果都为UNSAT,即所有 MC方法利用空子句关于子句集的相对极大项 极大项都能被扩展出来，那么子句集是不可满足的。 的个数来判定子句集的可满足性。如果相对极大项 由于并行处理，该算法在求解效率上较SRE算法有 个数为0，则子句集是不可满足的：否则，子句集是 了较大的提高。 可满足的。与扩展规则方法根据扩展出的极大项个句集扩展出来，子句集中必须有子句包含于该极大 项（子句看作文字集合）。 基于该性质，孙吉贵等提 出了一种新的基于扩展规则的定理证明方法 ＮＥＲ， 该方法将 ＳＡＴ 问题转化为一系列文字集合的包含 问题。 ＮＥＲ 算法按照一定次序判断极大项是否可 被当前待判定的子句集 Σ 扩展，若存在某个极大项 不能被扩展出来， 那么 Σ 是可满足的；否则，若所有 极大项都可以被扩展出来，则 Σ 是不可满足的。 其 最优和最坏时间复杂度分别为 Ｏ （ ｍ ＋ ｎ × ｋ ２ ） 和 Ｏ（２ ｍ ×（ｍ＋ｎ×ｋ ２ ）），ｍ、ｎ、ｋ 分别表示子句集中变量 的个数、子句的个数和子句的平均长度。 实验结果 表明，无论是对于随机问题还是标准测试用例，ＮＥＲ 算法的执行效率较 ＩＥＲ 和 ＤＲ 算法都有很大的提 高，有些问题可以提高 ２ 个数量级。 ＮＥＲ 算法将所有极大项按照一定顺序来一一 判定其是否能由子句集扩展出来，直到某个极大项 不能被扩展时或者所有极大项都可由子句集扩展出 来时，才能判定出子句集的可满足性。 事实上，当一 个极大项可由某一子句扩展时，接下来的部分极大 项可以不用判断其是否可由子句集扩展出来，从而 减少了需要判断的极大项个数。 张立明等［２１］ 定义 了半扩展规则，并且提出了基于半扩展规则的定理 证明方法 ＳＲＥ（ｓｅｍｉ⁃ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ）。 ＳＲＥ 算法是在 ＮＥＲ 算法的基础上，按一定顺序判定极大项是否可 被子句集扩展，当一个极大项可被子句集中的某一 子句扩展时，那么基于此子句半扩展出的所有极大 项都不需判断其是否可被子句集扩展，这样减少了 需要判断的极大项个数，使计算复杂度由原来 ＮＥＲ 方法的 Ｏ（２ ｍ ×（ｍ＋ｎ×ｋ ２ ））降为 Ｏ（２ ｄ ×（ｍ＋ｎ×ｋ ２ ）＋ ｎ ２ ），其中 ｄ 为子句集中子句的度的平均值。 ｄ 越 小，ＳＲＥ 算法的求解效率越高；当 ｄ 趋近与 ｍ 时， ＳＲＥ 算法的求解效率较 ＮＥＲ 算法提高较小。 进一步，他们提出了基于半扩展规则的并行定 理证明方法 ＰＰＳＥＲ （ ｐａｒａｌｌｅｌ ｔｈｅｏｒｅｍ ｐｒｏｖｉｎｇ ａｌｇｏ⁃ ｒｉｔｈｍ ｂａｓｅｄ ｏｎ ｓｅｍｉ⁃ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ） ［２２］ ，该方法首先 给出在极大项子空间中判定子句集可满足性的算法 ＰＳＥＲ，然后将子句集的极大项空间分解为若干个互 不相交的子空间，对每个极大项子空间，并行地调用 ＰＳＥＲ 方法进行判定，如果有一个极大项子空间中 返回的结果为 ＳＡＴ，即该子空间中存在某个极大项 不能被扩展出来，则子句集是可满足的；否则，如果 所有极大项子空间返回的结果都为 ＵＮＳＡＴ，即所有 极大项都能被扩展出来，那么子句集是不可满足的。 由于并行处理，该算法在求解效率上较 ＳＲＥ 算法有 了较大的提高。 ２）极大项覆盖方法。 为了避开容斥原理求解的复杂性，Ｙｉｎ 等［２３］ 从 相对极大项角度提出了一种基于极大项覆盖的有效 ＳＡＴ 求解方法 ＭＣ（ ｍａｘｔｅｒｍ ｃｏｖｅｒｉｎｇ ｆｏｒ ｓａｔｉｓｆｉａｂｉｌｉ⁃ ｔｙ）。 子句 Ｃ 关于子句集 Σ 覆盖的相对极大项是 Ｃ 覆 盖， 但 不 是 Σ 覆 盖 的 极 大 项， 表 示 为 ｒｅｌａｔｉｖｅＭａｘｔｅｒｍ（Ｃ，Σ） ＝ ＭＣ（Ｃ） ＼ＭＣ（Σ） 。 设子句 集 Σ ＝ ｛Ｃ１ ， Ｃ２ ， Ｃ３ ， Ｃ４ ｝，Ｃ 关于 Σ 的相对极大项如 图 １ 所示。 图 １ Ｃ 关于 Σ 的相对极大项 Ｆｉｇ． １ Ｔｈｅ ｒｅｌａｔｉｖｅ ｍａｘｔｅｒｍ ｏｆ Ｃ ｗｉｔｈ ｒｅｓｐｅｃｔ ｔｏ Σ 给定一个变量集合，设所有极大项集合为论域， 那么空子句 ε 覆盖的极大项集合等于该论域。 根据 扩展规则方法可知，如果 ＭＣ（Σ） ＝ ＭＣ（ε） ，则子句 集 Σ 是不可满足的；如果 ｒｅｌａｔｉｖｅＭａｘｔｅｒｍ（ε，Σ） ≠ ∅， 则 Σ 是可满足的。 图 ２ 给出了一个可满足的问 题实例。 图 ２ 一个可满足问题实例 Ｆｉｇ． ２ Ａ ｓａｔｉｓｆｉａｂｌｅ ｅｘａｍｐｌｅ ＭＣ 方法利用空子句关于子句集的相对极大项 的个数来判定子句集的可满足性。 如果相对极大项 个数为 ０，则子句集是不可满足的；否则，子句集是 可满足的。 与扩展规则方法根据扩展出的极大项个 ·４· 智 能 系 统 学 报 第 ９ 卷