·500· 智能系统学报 第8卷 个子句进行消解.最后采用一个递归函数从空子句 步提高效率，在MiniSat的分支选择中加入了启发式 开始回溯，逐步遍历整个消解序列，提取布尔不可满 策略.当每个变量决策时，MiniSat的分支默认选择 足子式 赋值为负值的一支.在算法的第1轮中，并不发生任 2.1.4基于最大可满足性的求解算法 何变化.第1轮之后，每个尚未删除的子句都在前1 目前，有很多研究人员利用极大可满足性和极 轮中有了一个关联赋值.除了新的关键子句移动到 小不可满足性之间的二元关系提取极小不可满足子 这个赋值的前面，随后的子句仍将保持同样的顺序. 式.Bailey和Stuckey在文献[25]中已经阐述了这种 程序因此确定了变量的分支方向，这将引导求解器 关系.基于最大可满足性的CAMUS[4,Digger!1]能 按着以前关联赋值的方向寻找新的赋值。 够提取极小不可满足子式：贪心遗传算法和蚁群算 2.2最小不可满足子式求解 法「)能够提取最小不可满足子式.文献[26]中提出 不可满足子式反应了问题的存在最小不可满足 了一种在CSP中提取极小不可满足子式的混合算 子式比极小不可满足子式更能精确地定位错误.研究 法.该算法也是基于最大可满足性求解极小不可满 最小不可满足算法，也是研究人员的最终目的.目前 足子式.求解CSP极小不可满足子式的算法一般分 关于最小不可满足子式的提取研究还相对较少， 为直接算法和间接算法.间接算法利用极小不可满 2.2.1基于辅助变量的算法 足子式和极小修正集(MCS)之间的关系.算法主要 算法AMUSE3)和文献[12]中算法通过引入一 是寻找一个完全的极小修正集，然后从中提取极小 组辅助变量求解不可满足子式.AMUSE是对一个基 不可满足子式.另一方面，直接算法通过产生子集和 于DPLL构架的SAT求解器的扩展.它不再寻找一 测试其可满足性直接地在CSPs约束的子集空间搜 个可满足的真值赋值而是寻找其中蕴含的不可满足 索不可满足子式.混合算法融合了直接和间接方法 子式.为此引入了一组辅助变量，通过自底向上的方 混合算法像间接算法那样不再计算全部的极小修正 式搜索不可满足树的空间：从一个空子句开始，逐步 集，而是寻找极小修正集中较小的子集.这就是所谓 添加子句，直到获得一个不可满足子式.为了改善搜 的“主干”集合，即极小修正子集发现的不可消减的 索效率，其中使用了冲突子句学习优化策略.但是 碰集每个主干集表示不可满足子式的一个簇.通过 AMUSE算法无法保证获得极小不可满足子式，尤其 直接方法搜索主干的超级空间，这些主干集随后逐 随着问题规模的扩大，效率会明显下降.文献[6]中 个被扩展为完全的不可满足子式.实验表明，基于最 提出了一个获得最小不可满足子式的模型：ω：= 大可满足性的混合算法比单纯直接算法或间接算法 {一s:}Uw:,其中新子句w是由子句w与选择变 效率高很多.混合算法通过在每步中搜索一个较小 量s:构成.选择变量s:决定是否选择子句w.对每个 的空间提高效率」 S中变量赋值，产生的子式可能是满足的，也可能是 2.1.5基于关联赋值的算法 不满足的对于不可满足的子式，S中有多少变量赋 文献[27]中算法提出了关联赋值的概念，将赋 值为1，就意味着有多少子句包含在不可满足子式 值与子句联系起来.关联赋值的概念来自于布劳威 里.那么最小不可满足子式就是S集合中赋值为1 尔不动点近似算法在可满足性问题方面的应用.它 的、数量最少的子公式通常可以使用高效的求解器 将子句视为实体，也就是一个有序的赋值集合，并且 来实现这个模型.公式中变量被组织成2个互斥的 从可能的赋值中选择一个赋值与其关联.这些赋值 集合：变量集合S和变量集合X首先决策变量S,然 形成一个完整的序列，在序列中优先选择所有可满 后决策变量X因此每次变量S赋值，都定义了一个 足赋值，再选择所有不可满足赋值.当达到帕累托最 潜在的子式.如果对于一个赋值，所有的子句都满 优后，有可能找到这些子句的一个子集来表示不可 足，那么回溯到最近未决策的变量S.否则，每次回 满足性.在帕累托最优中，所有子句已经选择了一个 溯要先改变X赋值，再改变S赋值，直到没有变量X 椎一的不满足自己的赋值.帕累托最优证明了子句 的赋值可以改变，则S中赋值为1最少的，就是最小 的选择权与不可满足公式之间的冲突.当子句证明 不可满足子式」 了公式的不可满足性后，利用文献[27]中的理论去 2.2.2分支限界算法 实现算法，寻找一个不可满足子式.然而这种算法的 文献中[13]中CAMUS-min和Digger都是基于 效率并不高，文献[12]中提出了一个简单有效的极 分支限界的算法.CAMUS-min算法是CAMUS的改 小不可满足子式抽取算法MiniUnsat..MiniUnsat中包 进，它比CAMUS多了分支限界过程.CAMUS利用极 含了一个高效率SAT求解器MiniSat2.0.为了进一 大可满足性和极小不可满足性之间的二元关系提取个子句进行消解．最后采用一个递归函数从空子句 开始回溯，逐步遍历整个消解序列，提取布尔不可满 足子式． ２．１．４ 基于最大可满足性的求解算法 目前，有很多研究人员利用极大可满足性和极 小不可满足性之间的二元关系提取极小不可满足子 式．Ｂａｉｌｅｙ 和 Ｓｔｕｃｋｅｙ 在文献［２５］中已经阐述了这种 关系．基于最大可满足性的 ＣＡＭＵＳ ［４］ ，Ｄｉｇｇｅｒ ［１３］ 能 够提取极小不可满足子式；贪心遗传算法和蚁群算 法［１４］能够提取最小不可满足子式．文献［２６］中提出 了一种在 ＣＳＰ 中提取极小不可满足子式的混合算 法．该算法也是基于最大可满足性求解极小不可满 足子式．求解 ＣＳＰ 极小不可满足子式的算法一般分 为直接算法和间接算法．间接算法利用极小不可满 足子式和极小修正集（ＭＣＳ）之间的关系．算法主要 是寻找一个完全的极小修正集，然后从中提取极小 不可满足子式．另一方面，直接算法通过产生子集和 测试其可满足性直接地在 ＣＳＰｓ 约束的子集空间搜 索不可满足子式．混合算法融合了直接和间接方法． 混合算法像间接算法那样不再计算全部的极小修正 集，而是寻找极小修正集中较小的子集．这就是所谓 的“主干”集合，即极小修正子集发现的不可消减的 碰集．每个主干集表示不可满足子式的一个簇．通过 直接方法搜索主干的超级空间，这些主干集随后逐 个被扩展为完全的不可满足子式．实验表明，基于最 大可满足性的混合算法比单纯直接算法或间接算法 效率高很多．混合算法通过在每步中搜索一个较小 的空间提高效率． ２．１．５ 基于关联赋值的算法 文献［２７］中算法提出了关联赋值的概念，将赋 值与子句联系起来．关联赋值的概念来自于布劳威 尔不动点近似算法在可满足性问题方面的应用．它 将子句视为实体，也就是一个有序的赋值集合，并且 从可能的赋值中选择一个赋值与其关联．这些赋值 形成一个完整的序列，在序列中优先选择所有可满 足赋值，再选择所有不可满足赋值．当达到帕累托最 优后，有可能找到这些子句的一个子集来表示不可 满足性．在帕累托最优中，所有子句已经选择了一个 惟一的不满足自己的赋值．帕累托最优证明了子句 的选择权与不可满足公式之间的冲突．当子句证明 了公式的不可满足性后，利用文献［２７］中的理论去 实现算法，寻找一个不可满足子式．然而这种算法的 效率并不高，文献［１２］中提出了一个简单有效的极 小不可满足子式抽取算法 ＭｉｎｉＵｎｓａｔ．ＭｉｎｉＵｎｓａｔ 中包 含了一个高效率 ＳＡＴ 求解器 ＭｉｎｉＳａｔ ２．０．为了进一 步提高效率，在 ＭｉｎｉＳａｔ 的分支选择中加入了启发式 策略．当每个变量决策时，ＭｉｎｉＳａｔ 的分支默认选择 赋值为负值的一支．在算法的第 １ 轮中，并不发生任 何变化．第 １ 轮之后，每个尚未删除的子句都在前 １ 轮中有了一个关联赋值．除了新的关键子句移动到 这个赋值的前面，随后的子句仍将保持同样的顺序． 程序因此确定了变量的分支方向，这将引导求解器 按着以前关联赋值的方向寻找新的赋值． ２．２ 最小不可满足子式求解 不可满足子式反应了问题的存在．最小不可满足 子式比极小不可满足子式更能精确地定位错误．研究 最小不可满足算法，也是研究人员的最终目的．目前 关于最小不可满足子式的提取研究还相对较少． ２．２．１ 基于辅助变量的算法 算法 ＡＭＵＳＥ ［３］和文献［１２］中算法通过引入一 组辅助变量求解不可满足子式．ＡＭＵＳＥ 是对一个基 于 ＤＰＬＬ 构架的 ＳＡＴ 求解器的扩展．它不再寻找一 个可满足的真值赋值而是寻找其中蕴含的不可满足 子式．为此引入了一组辅助变量，通过自底向上的方 式搜索不可满足树的空间：从一个空子句开始，逐步 添加子句，直到获得一个不可满足子式．为了改善搜 索效率，其中使用了冲突子句学习优化策略．但是 ＡＭＵＳＥ 算法无法保证获得极小不可满足子式，尤其 随着问题规模的扩大，效率会明显下降．文献［６］中 提出了一个获得最小不可满足子式的模型： ω ′ ｉ ＝ ｛¬ ｓｉ｝ ∪ ωｉ ，其中新子句 ω ′ ｉ 是由子句 ωｉ 与选择变 量 ｓｉ 构成．选择变量 ｓｉ 决定是否选择子句 ωｉ ． 对每个 Ｓ 中变量赋值，产生的子式可能是满足的，也可能是 不满足的．对于不可满足的子式，Ｓ 中有多少变量赋 值为 １，就意味着有多少子句包含在不可满足子式 里．那么最小不可满足子式就是 Ｓ 集合中赋值为 １ 的、数量最少的子公式．通常可以使用高效的求解器 来实现这个模型．公式中变量被组织成 ２ 个互斥的 集合：变量集合 Ｓ 和变量集合 Ｘ．首先决策变量 Ｓ，然 后决策变量 Ｘ．因此每次变量 Ｓ 赋值，都定义了一个 潜在的子式．如果对于一个赋值，所有的子句都满 足，那么回溯到最近未决策的变量 Ｓ．否则，每次回 溯要先改变 Ｘ 赋值，再改变 Ｓ 赋值，直到没有变量 Ｘ 的赋值可以改变，则 Ｓ 中赋值为 １ 最少的，就是最小 不可满足子式． ２．２．２ 分支限界算法 文献中［１３］中 ＣＡＭＵＳ⁃ｍｉｎ 和 Ｄｉｇｇｅｒ 都是基于 分支限界的算法．ＣＡＭＵＳ⁃ｍｉｎ 算法是 ＣＡＭＵＳ 的改 进，它比 ＣＡＭＵＳ 多了分支限界过程．ＣＡＭＵＳ 利用极 大可满足性和极小不可满足性之间的二元关系提取 ·５００· 智 能 系 统 学 报 第 ８ 卷