第1期 王金艳，等：扩展规则方法研究综述 。7 展规则的SAT求解算法#ER,该算法继承了扩展规 进一步替换对问题逐渐加强，如果任何一步中返回 则方法的优点，能快速求解互补因子较高的问题。 不可满足，则原问题不可满足：如果在某一步返回可 基于归结的算法DPLL[4]主要借助单文字规则提 满足并且解释没有被阻塞，那么原问题是可满足的。 高求解效率，在互补因子较高的情况下，单文字规则 由于PPI算法需要求出满足式映射，即模型，而ER 往往不能发挥作用，因此算法#DPLL效率较低。结 算法只能判定可满足性，不能给出模型。因此他们 合#ER和#DPLL算法的特点，赖永等提出了#CDE 又给出原子被潜在地阻塞的概念，以及2个原子被 算法，该算法根据IMod(∑，∧∑2)I=IMod(∑，)I- 阻塞和被潜在地阻塞之间的关系，并对PPI算法进 IMod(∑，∧E,)I,利用函数SelectClause(∑)从 行修改，提出了基于扩展规则的一阶定理证明方法 Σ中选择适合算法#DPLL的子句集合∑，文中使用 RPPI(revised primal partial instantiation)o 的是选出所有长度小于等于3的子句作为Σ，。当 Wu等[38]指出Lin给出的原子被潜地阻塞的定 函数返回空集时，算法#CDE等价于#ER:当返回 义对新产生子句的条件限制过严，导致RPPI算法 本身时，算法#CDE等价于#DPLL。#CDE算法综合 是不完备的，他们对潜在阻塞进行了重新定义，并且 了#ER和#DPLL的优点，当互补因子较小时，#CDE 提出了一种新的一阶扩展规则算法RFOER(revised 表现出算法#DPLL的优点，当互补因子较大时，表 first-order extension rule),该算法与RPPI算法主要 现出#ER的优点。 有以下3点不同：1)RPPI算法不完备，而RFOER 2)碰集方法。 算法完备；2)RPPI调用的是基本的ER算法，而 针对SAT问题求解算法的效率会随着子句集 RFOER调用的是更为高效的带化简规则和启发式 的规模的增大而迅速降低的问题，许有军等36提出 策略的ER算法；3)RFOER中增加了M-可满足的情 一种间接应用扩展规则求解#SAT问题的MCEHST 形，使得算法可以被更灵活地应用，更适合用于求解 model counting with extension rule and hitting set 实际的问题。 tree)算法。在文献[24]中，他们发现不能被子句集 3.2描述逻辑 扩展出的极大项可以构造出该子句集的一个碰集， 描述逻辑是一种基于对象的知识表示形式化工 即可以根据子句集是否存在不含互补文字的碰集来 具，是一阶谓词逻辑的可判定子集[3]，研究有效的 判定子句集是否为可满足的。任何不能由子句集扩 推理算法是描述逻辑的一个重要研究内容。Zou 展出的极大项都对应于该子句集的一个模型，而且 等[o]将扩展规则推广到描述逻辑ALC的推理中， 该模型正好与子句集的碰集所扩展出的极大项相对 定义了概念扩展规则CER(concept extension rule) 应。MCEHST算法首先得到子句集的所有极小碰 EPCCCL each pair of clausal concept contains 集，然后利用扩展规则计算出这些碰集扩展出的极 liks)理论，即任意2个子句概念都包含链接（概念 大项个数，即模型数。当变量数一定，随着子句数的 链接或关系链接)的规范概念合取式(conjunction 增加，子句集的极小碰集数显著减少。与已存在的 normal concept,.CNC),提出了基于概念扩展规则的 其他#SAT算法比较，当子句数较大且子句较短时， 推理方法，并且证明该方法能在多项式时间内完成 该方法的执行效率较高：但是当子句数较小时，该算 任意EPCCCL理论的可满足性推理和蕴含推理，因 法的执行效率较低。实际应用时，可以根据情况来 此EPCCCL理论可以作为描述逻辑中知识编译的 决定是否选择MCEHST算法。 目标语言。进一步他们提出了基于概念扩展规则的 描述逻辑知识编译方法，该方法首先利用CER 3 扩展规则在其他逻辑中的应用 DLKC算法将CNC公式编译成EPCCCL理论，然后 目前，扩展规则方法已被推广到一阶逻辑、描述 利用基于概念扩展规则的推理方法可以在多项式时 逻辑、模态逻辑、可能性逻辑和多值逻辑，下面分别 间内回答任意查询。 讨论扩展规则方法在这些逻辑中的应用。 3.3模态逻辑 3.1一阶逻辑 模态逻辑为知识工程和并行程序的研究提供了 利用Hooker提出的部分实例化推理方法PPI 一种形式化的途径4)。目前常用的模态推理方法 (primal partial instantiation)[3),Lin等]把扩展规 大致可分为以下2种：一种是直接推广经典的推理 则方法从命题逻辑提升到一阶逻辑。PPI算法的基 方法使之能应用于模态逻辑：另一种是利用转换方 本思想是把一阶逻辑的定理证明问题转化成一系列 法将模态逻辑转换为经典逻辑，然后利用经典逻辑 SAT问题，首先从较弱的SAT问题入手，然后通过 中的方法进行推理，其中关系转换方法、函数转换方展规则的＃ＳＡＴ 求解算法＃ＥＲ，该算法继承了扩展规 则方法的优点，能快速求解互补因子较高的问题。 基于归结的算法＃ＤＰＬＬ ［３４⁃３５］主要借助单文字规则提 高求解效率，在互补因子较高的情况下，单文字规则 往往不能发挥作用，因此算法＃ＤＰＬＬ效率较低。 结 合＃ＥＲ 和＃ＤＰＬＬ 算法的特点，赖永等提出了＃ＣＤＥ 算法，该算法根据 ｜ Ｍｏｄ（Σ１ ∧ Σ２） ｜ ＝ ｜ Ｍｏｄ（Σ１） ｜ － ｜ Ｍｏｄ（Σ１ ∧ ØΣ２ ） ｜ ，利用函数 ＳｅｌｅｃｔＣｌａｕｓｅ（Σ） 从 Σ 中选择适合算法＃ＤＰＬＬ 的子句集合 Σ１ ，文中使用 的是选出所有长度小于等于 ３ 的子句作为 Σ１ 。 当 函数返回空集时，算法＃ＣＤＥ 等价于＃ＥＲ；当返回 Σ 本身时，算法＃ＣＤＥ 等价于＃ＤＰＬＬ。 ＃ＣＤＥ 算法综合 了＃ＥＲ 和＃ＤＰＬＬ 的优点，当互补因子较小时，＃ＣＤＥ 表现出算法＃ＤＰＬＬ 的优点，当互补因子较大时，表 现出＃ＥＲ 的优点。 ２）碰集方法。 针对＃ＳＡＴ 问题求解算法的效率会随着子句集 的规模的增大而迅速降低的问题，许有军等［３６］ 提出 一种间接应用扩展规则求解＃ＳＡＴ 问题的 ＭＣＥＨＳＴ （ ｍｏｄｅｌ ｃｏｕｎｔｉｎｇ ｗｉｔｈ ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ ａｎｄ ｈｉｔｔｉｎｇ ｓｅｔ ｔｒｅｅ）算法。 在文献［２４］中，他们发现不能被子句集 扩展出的极大项可以构造出该子句集的一个碰集， 即可以根据子句集是否存在不含互补文字的碰集来 判定子句集是否为可满足的。 任何不能由子句集扩 展出的极大项都对应于该子句集的一个模型，而且 该模型正好与子句集的碰集所扩展出的极大项相对 应。 ＭＣＥＨＳＴ 算法首先得到子句集的所有极小碰 集，然后利用扩展规则计算出这些碰集扩展出的极 大项个数，即模型数。 当变量数一定，随着子句数的 增加，子句集的极小碰集数显著减少。 与已存在的 其他＃ＳＡＴ 算法比较，当子句数较大且子句较短时， 该方法的执行效率较高；但是当子句数较小时，该算 法的执行效率较低。 实际应用时，可以根据情况来 决定是否选择 ＭＣＥＨＳＴ 算法。 ３ 扩展规则在其他逻辑中的应用 目前，扩展规则方法已被推广到一阶逻辑、描述 逻辑、模态逻辑、可能性逻辑和多值逻辑，下面分别 讨论扩展规则方法在这些逻辑中的应用。 ３．１ 一阶逻辑 利用 Ｈｏｏｋｅｒ 提出的部分实例化推理方法 ＰＰＩ （ｐｒｉｍａｌ ｐａｒｔｉａｌ ｉｎｓｔａｎｔｉａｔｉｏｎ） ［３７］ ，Ｌｉｎ 等［７］ 把扩展规 则方法从命题逻辑提升到一阶逻辑。 ＰＰＩ 算法的基 本思想是把一阶逻辑的定理证明问题转化成一系列 ＳＡＴ 问题，首先从较弱的 ＳＡＴ 问题入手，然后通过 进一步替换对问题逐渐加强，如果任何一步中返回 不可满足，则原问题不可满足；如果在某一步返回可 满足并且解释没有被阻塞，那么原问题是可满足的。 由于 ＰＰＩ 算法需要求出满足式映射，即模型，而 ＥＲ 算法只能判定可满足性，不能给出模型。 因此他们 又给出原子被潜在地阻塞的概念，以及 ２ 个原子被 阻塞和被潜在地阻塞之间的关系，并对 ＰＰＩ 算法进 行修改，提出了基于扩展规则的一阶定理证明方法 ＲＰＰＩ（ｒｅｖｉｓｅｄ ｐｒｉｍａｌ ｐａｒｔｉａｌ ｉｎｓｔａｎｔｉａｔｉｏｎ）。 Ｗｕ 等［３８］指出 Ｌｉｎ 给出的原子被潜地阻塞的定 义对新产生子句的条件限制过严，导致 ＲＰＰＩ 算法 是不完备的，他们对潜在阻塞进行了重新定义，并且 提出了一种新的一阶扩展规则算法 ＲＦＯＥＲ（ｒｅｖｉｓｅｄ ｆｉｒｓｔ⁃ｏｒｄｅｒ ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ），该算法与 ＲＰＰＩ 算法主要 有以下 ３ 点不同：１） ＲＰＰＩ 算法不完备，而 ＲＦＯＥＲ 算法完备；２） ＲＰＰＩ 调用的是基本的 ＥＲ 算法，而 ＲＦＯＥＲ 调用的是更为高效的带化简规则和启发式 策略的 ＥＲ 算法；３）ＲＦＯＥＲ 中增加了 Ｍ⁃可满足的情 形，使得算法可以被更灵活地应用，更适合用于求解 实际的问题。 ３．２ 描述逻辑 描述逻辑是一种基于对象的知识表示形式化工 具，是一阶谓词逻辑的可判定子集［３９］ ，研究有效的 推理算法是描述逻辑的一个重要研究内容。 Ｚｏｕ 等［４０］将扩展规则推广到描述逻辑 ＡＬＣ 的推理中， 定义了概念扩展规则 ＣＥＲ（ ｃｏｎｃｅｐｔ ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ） 和 ＥＰＣＣＣＬ （ ｅａｃｈ ｐａｉｒ ｏｆ ｃｌａｕｓａｌ ｃｏｎｃｅｐｔ ｃｏｎｔａｉｎｓ ｌｉｎｋｓ）理论，即任意 ２ 个子句概念都包含链接（概念 链接或关系链接） 的规范概念合取式（ ｃｏｎｊｕｎｃｔｉｏｎ ｎｏｒｍａｌ ｃｏｎｃｅｐｔ， ＣＮＣ），提出了基于概念扩展规则的 推理方法，并且证明该方法能在多项式时间内完成 任意 ＥＰＣＣＣＬ 理论的可满足性推理和蕴含推理，因 此 ＥＰＣＣＣＬ 理论可以作为描述逻辑中知识编译的 目标语言。 进一步他们提出了基于概念扩展规则的 描述逻辑知识编译方法， 该方法首先利用 ＣＥＲ⁃ ＤＬＫＣ 算法将 ＣＮＣ 公式编译成 ＥＰＣＣＣＬ 理论，然后 利用基于概念扩展规则的推理方法可以在多项式时 间内回答任意查询。 ３．３ 模态逻辑 模态逻辑为知识工程和并行程序的研究提供了 一种形式化的途径［４１］ 。 目前常用的模态推理方法 大致可分为以下 ２ 种：一种是直接推广经典的推理 方法使之能应用于模态逻辑；另一种是利用转换方 法将模态逻辑转换为经典逻辑，然后利用经典逻辑 中的方法进行推理，其中关系转换方法、函数转换方 第 １ 期 王金艳，等：扩展规则方法研究综述 ·７·