第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２ 不可满足子式求解算法 按照问题的解决方式，求解布尔不可满足子式的 方法可划分为基于 ＤＰＬＬ 搜索［２，４⁃６，１２⁃１４］ 与局部搜 索［７⁃１１］ ．通常来说 ，基于 ＤＰＬＬ 搜索方法能够找到问 题的精确解，但其面临的主要挑战是计算时间随问题 规模的增大呈指数级增长．而局部启发式搜索尽管有 时无法给出精确解，但其运算速度快，求解效率高． 根据不可满足子式的大小可以分为 ２ 类：１）极小 不可满足子式的提取算法［２⁃１１］ ；２）最小不可满足子式 的提取算法［１２⁃１４］ ．相对而言，最小不可满足子式的求 解难度更大，算法的复杂度也更高． ２．１ 极小不可满足子式求解 当前主流的不可满足子式提取算法关于极小不 可满足子式的提取．形式验证与人工智能规划问题 均可转为可满足性问题，一组可满足的赋值代表了 一种可行方案；反之，说明原问题存在错误，寻找不 可满足子式可以精确地对问题进行定位． ２．１．１ 基于冲突树的搜索算法 Ｈａｎ 和 Ｌｅｅ ［２４］提出了一个获得所有极小不可满 足子式的算法．该方法的思想是有序遍历集合 Ｓ 的 所有子集．它由 ２ 部分组成：１）用 ＣＳ⁃ｔｒｅｅ（冲突树） 的不同结点表示集合 Ｓ 的不同子集，并且没有哪 ２ 个结点表示相同的子集．ＣＳ⁃ｔｒｅｅ 定义了子集间的遍 历顺序，因此保证了同一子集不被重复搜索．为了实 现这个目标，一个结点由集合 Ｄ 和集合 Ｐ ２ 部分组 成，表示为 Ｄ ∪ Ｐ ．集合 Ｄ 的元素一定要出现在所 有后续子集中，而集合 Ｐ 的元素不需要．如果一个结 点有｜ Ｐ ｜ 个孩子，它由逐个消减集合 Ｐ 约束，并加 入到集合 Ｄ 中获得．函数 ａｌｌ ｓｕｂｓｅｔｓ （Ｄ，Ｐ，ϕ） 遍历 ＣＳ⁃ｔｒｅｅ 的所有结点，返回 Ｄ ∪ Ｘ（Ｘ ⊂ Ｐ） ．当迭代访 问一个根结点时，每次迭代以深度优先方式遍历 ＣＳ⁃ｔｒｅｅ，并且每次内部调用 ａｌｌ ｓｕｂｓｅｔｓ（ ）函数访问 这个孩子结点的后代．２）利用 ＣＳ⁃ｔｒｅｅ 探测所有极小 不可满足子式．算法以深度优先方式遍历树，测试每 个结点的标志 Ｄ ∪ Ｐ ，判断其可满足性．如果结点可 满足，那么就不必访问它的孩子节点．否则，继续寻 找孩子节点来寻找不可满足子式．如果遍历所有孩 子结点没有发现子集 Ａ 使得 Ａ ⊂ Ｄ ．那么集合 Ｄ 就 是极小不可满足集合．文献［２］在以上基本算法中加 入了预处理，利用约束独立性、利用始终满足的子 句、蕴涵、廉价求解器、增量式求解器、无视约束等策 略．其中，使用增量式求解器极大地改进了算法，它 减少了对算法规则的依赖性，能够快速地发现可满 足子集． ２．１．２ ＯＭＵＳ 与 ＡＳＭＵＳ 算法 文献［１４］中，É． Ｇｒéｇｏｉｒｅ 提出了基于启发式局部 搜索算法 ＯＭＵＳ．ＯＭＵＳ 算法是通过计算关键子句分 值来获得一个极小不可满足子式的启发式算法．算法 主要分为 ２ 部分：１）在局部算法中根据子句布尔值为 假的频度计算子句的分值，移除确定不可能出现在不 可满足子式中的子句．具体来说，对于一个不可满足 子式，如果在局部搜索时终未能找到它的一个赋值模 型，那么将移除子式中分值最低的子句．获得的子公 式将被记录在堆栈中．２）检查最后一个未能赋值的子 式是否可满足，如果子公式是不可满足的，那么它就 是不可满足子式的近似解．否则，重复检查栈顶子句 超集的不可满足性，直到一个集合被证明是不可满足 的．该过程将获得一个近似的极小不可满足子式．然 后，调用一个精细调节（ｆｉｎｅ ｔｕｎｅｓ）过程，ＯＭＵＳ 算法 最终获得一个不可满足子式． É． Ｇｒéｇｏｉｒｅ 在文献［８］ 中提出了 ＡＳＭＵＳ 算法． ＡＳＭＵＳ 以 ＯＭＵＳ 为基础，可以近似求解所有不可满 足子式的集合．ＭＡＸ⁃ＳＡＴ 可以提供极小的不可满足 子式数量．ＭＡＸ⁃ＳＡＴ 解中的剩余不可满足子句一定 尽可能多地属于那些不可满足子式的交集．那么对 于每个子句，记录最小的子句数．在探测到一个不可 满足子式后，把不可满足子式中分值最高的子句删 除掉．很显然，ＡＳＭＵＳ 是不完全的． ２．１．３ 基于消解反驳的局部搜索算法 局部搜索是一种求解优化问题的算法，算法从 解空间的一个点出发，每一步从当前候选解移动到 一个邻居候选解，去寻找较好的候选解，候选解的质 量是由一个评估函数来界定的．局部搜索算法在处 理规模较大的问题时，其收敛速度快，求解效率高． 上文提到的 ＯＭＵＳ 与 ＡＳＭＵＳ 实质上是启发式局部 搜索与计数的组合．消解是判定 ＳＡＴ 问题的基本方 法之一．一个公式经过一系列的消解步骤最终产生 空子句，则公式是不可满足的．文献［９⁃１１］中采用局 部搜索方法作为解空间的搜索策略．算法在搜索过 程中建立证明公式不可满足性的消解序列，并从其 中提取不可满足子式．算法描述如下：算法启发式或 随机地选择 ２ 个子句进行消解，最终得到一个消解 序列或达到最大迭代次数．搜索过程融合了一些基 于启发式的 ＳＡＴ 推理技术，包括二元子句消解、等 价约简和单元子句传播．算法首先寻找公式中是否 存在单元子句，如果存在，则在公式上进行单元子句 传播，并进一步判断能否产生空子句；如果存在二元 子句，则执行二元子句消解与等价性约简，启发式地 选择消解子句．若 ２ 类子句都不存在，则随机选取 ２ 第 ６ 期 殷明浩，等：不可满足子式研究 ·４９９·