第6期 殷明浩，等：不可满足子式研究 ·503· 判断一个公式是否属于MU(k).因为其使用了“遍 其缺点，尽可能提高算法的效率.例如文献[26]中提 历全部k个子集”的策略，所以算法非常依赖参数k 出了一种在CSP中提取极小不可满足子式的混合 H.Fleischne等利用双边图匹配的某些相应赋值限 算法，这是直接算法和间接算法的混合.文献[14]求 制寻找一个可满足的真值赋值.算法的时间复杂度 解最小不可满足子式可以视为贪心算法与遗传算法 为n,精确上界0(lnk+1/2).(l为公式长度，n 的混合算法 为公式的变量数).S.Szeide[2提出了一个算法，并 3)新领域中扩展：在形式验证等实际应用中， 得到一个新的结果.算法产生于SAT问题的固定参 QBF、CSP、SMT都比SAT表达力强.尤其SMT技术 数可解问题：对于一个CNF公式F,如果其子集中 得到飞速发展，并且在验证领域获得很好的效果.研 子句个数超过变量个数最多k个，那么可以在 究SMT的极小不可满足子式将是未来主要方向. O(2n3)时间内判断公式F的可满足性.参数k就 4)参数复杂性：将固定差值的极小不可满足子 是F的最大差值，可以用图匹配算法有效计算.最 式转化为固定参数问题，并且求解其计算复杂性.但 后，基于以上结论，利用图论中的最大差值和q-ex 是，对于QBF中，MF(k)(k>1)是否可以在多项式 panding双边图0]计算出改进的结果为O(2*n). 时间内判定，依然是开放的， 3.3QBF中的极小不可满足子式 参考文献： 近年来，SAT技术已经成功应用在限界模型检验 (bounded model checking,BMC)并推广到限界的模型 [1]GUPTA A.Learning abstractions for model checking[D]. Pittsburgh:Carnegie Mellon University,2006:1-180. 检验.但是直接将基于SAT的BMC推广到非限界的 [2]De La BANDA M G,STUCKEY P J,WAZNY J.Finding 模型检验的方法不能克服软件规模增大导致的状态 all minimal unsatisfiable subsets [C]//Proceedings of the 空间爆炸问题，即模型检验过程中软件规模的增大可 5th ACM SIGPLAN International Conference on Principles 能导致命题逻辑公式的长度呈指数倍的增长.带量词 and Practice of Declaritive Programming.New York,USA, 2003:32-43. 的布尔公式QBF作为SAT公式的自然扩展具有紧凑 [3]OH Y,MNEIMNEH M N,ANDRAUS Z S.AMUSE:a 的空间结构和更强大、更直观的表达能力， minimally unsatisfiable subformula extractor[C]//Proceed- 赵希顺等2]对QBF中的极小不可满足问题 ings of the 41st Annual Design Automation Conference.New (minimal falsity,MF)进行了研究.对不可满足的子 York,USA,2004:518-523. 式研究，有可能产生新的QBF求解算法.QBF的最 [4]LIFFTTON M,SAKALLAH K.On finding all minimally un- satisfiable subformulas [C]//Theory and Applications of 小不可满足公式QCNF指的是该公式不可满足但其 Satisfiability Testing.St.Andrews,Scotland,2005:173- 任一真子公式均可满足.一个QCNF公式的差值不 186. 同于命题公式的差值，其差值是子句数和存在量词 [5]MARQUES-SILVA J,LYNCE I.On improving MUS extrac- 之间的差值.对QCNF公式固定差值为1的极小不 tion algorithms[M//Lecture Notes in Computer Science, Heidelberg:Springer,2011,6695:159-173. 可满足子式可表示为MF(1).文献[23]中得出重要 [6]Van MAAREN H,WIERINGA S.Finding guaranteed 结论：对QCNF公式固定差值为1的极小不可满足 MUSes fast[M].Heidelberg:Springer,2008:291-304. 子式可以在多项式时间有解.这个证明依赖于公式 [7]GREGOIRE E,MAZURE B,PIETTE C.Extracting MUSes MU(1)的结构.对于MF(k)(k≥2)是否存在多项 [C]//Proceedings of the 17th European Conference on Ar- 式时间可解，仍然是开放的. tificial Intelligence 2006.Riva del Garda,Italy,2006:387- 391. 4总结与展望 8]GREGOIRE E.MAZURE B.PIETTE C.Local-search ex- traction of MUSes[J].Constrain,2007,12(3):325-344. 不可满足子式的研究给研究人员带了多方面的 [9]ZHANG J,SHEN S,LI S.Finding unsatisfiable subformu- 挑战，但是也给研究人员带来多方面机会.不可满足 las with stochastic method M].Heidelberg:Springer, 2007,4881:385-394. 子式的研究出现了以下研究方面的热点， [10]ZHANG J,SHEN S,LI S.A heuristic local search algo- 1)使用符号化技术，如BDD技术能够紧凑地表 rithm for unsatisfiable cores extraction[M].Heidelberg: 示公式，是缓解内存瓶颈的关键技术.文献[31]借助 Springer,.2007,4707:649-659. 于BDD判断公式是不可满足的并且其全部子公式 [11]ZHANG J,SHEN S,LI S.Tracking unsatisfiable subfor- 是满足的，从而证明公式是极小不可满足子式， mulas from reduced refutation proof[J].Journal of Soft- ware,2009,4(1):42-49. 2)混合求解算法：每种求解策略有其自身优点 [12]LYNCE I,MARQUES-SILVA J P.On computing minimum 和缺点.混合求解有利于发挥各自算法的优势，避免 unsatisfiable cores[C]//International Symposium on Theo-判断一个公式是否属于 ＭＵ（ｋ）．因为其使用了 “遍 历全部 ｋ 个子集”的策略，所以算法非常依赖参数 ｋ． Ｈ． Ｆｌｅｉｓｃｈｎｅ 等利用双边图匹配的某些相应赋值限 制寻找一个可满足的真值赋值．算法的时间复杂度 为 ｎ Ｏ（ｋ） ，精确上界 Ｏ（ｌｎ ｋ ＋ １ ／ ２）． （ｌ 为公式长度，ｎ 为公式的变量数）．Ｓ． Ｓｚｅｉｄｅ ［２２］ 提出了一个算法，并 得到一个新的结果．算法产生于 ＳＡＴ 问题的固定参 数可解问题：对于一个 ＣＮＦ 公式 Ｆ，如果其子集中 子句个数超过变量个数最多 ｋ 个， 那么 可 以 在 Ｏ（２ ｋ ｎ ３ ） 时间内判断公式 Ｆ 的可满足性．参数 ｋ 就 是 Ｆ 的最大差值，可以用图匹配算法有效计算．最 后，基于以上结论，利用图论中的最大差值和 ｑ⁃ｅｘ⁃ ｐａｎｄｉｎｇ 双边图［３０］计算出改进的结果为 Ｏ（２ ｋ ｎ ４ ） ． ３．３ ＱＢＦ 中的极小不可满足子式 近年来，ＳＡＴ 技术已经成功应用在限界模型检验 （ｂｏｕｎｄｅｄ ｍｏｄｅｌ ｃｈｅｃｋｉｎｇ，ＢＭＣ）并推广到限界的模型 检验．但是直接将基于 ＳＡＴ 的 ＢＭＣ 推广到非限界的 模型检验的方法不能克服软件规模增大导致的状态 空间爆炸问题，即模型检验过程中软件规模的增大可 能导致命题逻辑公式的长度呈指数倍的增长．带量词 的布尔公式 ＱＢＦ 作为 ＳＡＴ 公式的自然扩展具有紧凑 的空间结构和更强大、更直观的表达能力． 赵希顺等［２３］ 对 ＱＢＦ 中的极小不可满足问题 （ｍｉｎｉｍａｌ ｆａｌｓｉｔｙ，ＭＦ） 进行了研究．对不可满足的子 式研究，有可能产生新的 ＱＢＦ 求解算法．ＱＢＦ 的最 小不可满足公式 ＱＣＮＦ 指的是该公式不可满足但其 任一真子公式均可满足．一个 ＱＣＮＦ 公式的差值不 同于命题公式的差值，其差值是子句数和存在量词 之间的差值．对 ＱＣＮＦ 公式固定差值为 １ 的极小不 可满足子式可表示为 ＭＦ（１）．文献［２３］中得出重要 结论：对 ＱＣＮＦ 公式固定差值为 １ 的极小不可满足 子式可以在多项式时间有解．这个证明依赖于公式 ＭＵ（１）的结构． 对于 ＭＦ（ ｋ） （ ｋ≥２）是否存在多项 式时间可解，仍然是开放的． ４ 总结与展望 不可满足子式的研究给研究人员带了多方面的 挑战，但是也给研究人员带来多方面机会．不可满足 子式的研究出现了以下研究方面的热点． １）使用符号化技术，如 ＢＤＤ 技术能够紧凑地表 示公式，是缓解内存瓶颈的关键技术．文献［３１］借助 于 ＢＤＤ 判断公式是不可满足的并且其全部子公式 是满足的，从而证明公式是极小不可满足子式． ２）混合求解算法：每种求解策略有其自身优点 和缺点．混合求解有利于发挥各自算法的优势，避免 其缺点，尽可能提高算法的效率．例如文献［２６］中提 出了一种在 ＣＳＰ 中提取极小不可满足子式的混合 算法，这是直接算法和间接算法的混合．文献［１４］求 解最小不可满足子式可以视为贪心算法与遗传算法 的混合算法． ３）新领域中扩展：在形式验证等实际应用中， ＱＢＦ、ＣＳＰ、ＳＭＴ 都比 ＳＡＴ 表达力强．尤其 ＳＭＴ 技术 得到飞速发展，并且在验证领域获得很好的效果．研 究 ＳＭＴ 的极小不可满足子式将是未来主要方向． ４）参数复杂性：将固定差值的极小不可满足子 式转化为固定参数问题，并且求解其计算复杂性．但 是，对于 ＱＢＦ 中，ＭＦ（ ｋ） （ ｋ＞１） 是否可以在多项式 时间内判定，依然是开放的． 参考文献： ［１］ ＧＵＰＴＡ Ａ． Ｌｅａｒｎｉｎｇ ａｂｓｔｒａｃｔｉｏｎｓ ｆｏｒ ｍｏｄｅｌ ｃｈｅｃｋｉｎｇ［Ｄ］． Ｐｉｔｔｓｂｕｒｇｈ： Ｃａｒｎｅｇｉｅ Ｍｅｌｌｏｎ Ｕｎｉｖｅｒｓｉｔｙ， ２００６： １⁃１８０． ［２］Ｄｅ Ｌａ ＢＡＮＤＡ Ｍ Ｇ， ＳＴＵＣＫＥＹ Ｐ Ｊ， ＷＡＺＮＹ Ｊ． Ｆｉｎｄｉｎｇ ａｌｌ ｍｉｎｉｍａｌ ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｓｅｔｓ ［ Ｃ］ ／ ／ Ｐｒｏｃｅｅｄｉｎｇｓ ｏｆ ｔｈｅ ５ｔｈ ＡＣＭ ＳＩＧＰＬＡＮ Ｉｎｔｅｒｎａｔｉｏｎａｌ Ｃｏｎｆｅｒｅｎｃｅ ｏｎ Ｐｒｉｎｃｉｐｌｅｓ ａｎｄ Ｐｒａｃｔｉｃｅ ｏｆ Ｄｅｃｌａｒｉｔｉｖｅ Ｐｒｏｇｒａｍｍｉｎｇ． Ｎｅｗ Ｙｏｒｋ， ＵＳＡ， ２００３： ３２⁃４３． ［３］ ＯＨ Ｙ， ＭＮＥＩＭＮＥＨ Ｍ Ｎ， ＡＮＤＲＡＵＳ Ｚ Ｓ． ＡＭＵＳＥ： ａ ｍｉｎｉｍａｌｌｙ ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒｍｕｌａ ｅｘｔｒａｃｔｏｒ［Ｃ］ ／ ／ Ｐｒｏｃｅｅｄ⁃ ｉｎｇｓ ｏｆ ｔｈｅ ４１ｓｔ Ａｎｎｕａｌ Ｄｅｓｉｇｎ Ａｕｔｏｍａｔｉｏｎ Ｃｏｎｆｅｒｅｎｃｅ． Ｎｅｗ Ｙｏｒｋ， ＵＳＡ， ２００４： ５１８⁃５２３． ［４］ＬＩＦＦＩＴＯＮ Ｍ， ＳＡＫＡＬＬＡＨ Ｋ． Ｏｎ ｆｉｎｄｉｎｇ ａｌｌ ｍｉｎｉｍａｌｌｙ ｕｎ⁃ ｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒｍｕｌａｓ ［ Ｃ ］ ／ ／ Ｔｈｅｏｒｙ ａｎｄ Ａｐｐｌｉｃａｔｉｏｎｓ ｏｆ Ｓａｔｉｓｆｉａｂｉｌｉｔｙ Ｔｅｓｔｉｎｇ． Ｓｔ． Ａｎｄｒｅｗｓ， Ｓｃｏｔｌａｎｄ， ２００５： １７３⁃ １８６． ［５］ＭＡＲＱＵＥＳ⁃ＳＩＬＶＡ Ｊ， ＬＹＮＣＥ Ｉ． Ｏｎ ｉｍｐｒｏｖｉｎｇ ＭＵＳ ｅｘｔｒａｃ⁃ ｔｉｏｎ ａｌｇｏｒｉｔｈｍｓ ［ Ｍ］ ／ ／ Ｌｅｃｔｕｒｅ Ｎｏｔｅｓ ｉｎ Ｃｏｍｐｕｔｅｒ Ｓｃｉｅｎｃｅ， Ｈｅｉｄｅｌｂｅｒｇ： Ｓｐｒｉｎｇｅｒ， ２０１１， ６６９５： １５９⁃１７３． ［ ６ ］ Ｖａｎ ＭＡＡＲＥＮ Ｈ， ＷＩＥＲＩＮＧＡ Ｓ． Ｆｉｎｄｉｎｇ ｇｕａｒａｎｔｅｅｄ ＭＵＳｅｓ ｆａｓｔ［Ｍ］． Ｈｅｉｄｅｌｂｅｒｇ： Ｓｐｒｉｎｇｅｒ， ２００８： ２９１⁃３０４． ［７］ＧＲÉＧＯＩＲＥ É， ＭＡＺＵＲＥ Ｂ， ＰＩＥＴＴＥ Ｃ． Ｅｘｔｒａｃｔｉｎｇ ＭＵＳｅｓ ［Ｃ］ ／ ／ Ｐｒｏｃｅｅｄｉｎｇｓ ｏｆ ｔｈｅ １７ｔｈ Ｅｕｒｏｐｅａｎ Ｃｏｎｆｅｒｅｎｃｅ ｏｎ Ａｒ⁃ ｔｉｆｉｃｉａｌ Ｉｎｔｅｌｌｉｇｅｎｃｅ ２００６． Ｒｉｖａ ｄｅｌ Ｇａｒｄａ， Ｉｔａｌｙ， ２００６： ３８７⁃ ３９１． ［８］ＧＲÉＧＯＩＲＥ É， ＭＡＺＵＲＥ Ｂ， ＰＩＥＴＴＥ Ｃ． Ｌｏｃａｌ⁃ｓｅａｒｃｈ ｅｘ⁃ ｔｒａｃｔｉｏｎ ｏｆ ＭＵＳｅｓ［Ｊ］． Ｃｏｎｓｔｒａｉｎ， ２００７， １２（３）： ３２５⁃３４４． ［９］ＺＨＡＮＧ Ｊ， ＳＨＥＮ Ｓ， ＬＩ Ｓ． Ｆｉｎｄｉｎｇ ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒｍｕ⁃ ｌａｓ ｗｉｔｈ ｓｔｏｃｈａｓｔｉｃ ｍｅｔｈｏｄ ［ Ｍ ］． Ｈｅｉｄｅｌｂｅｒｇ： Ｓｐｒｉｎｇｅｒ， ２００７， ４８８１： ３８５⁃３９４． ［１０］ＺＨＡＮＧ Ｊ， ＳＨＥＮ Ｓ， ＬＩ Ｓ． Ａ ｈｅｕｒｉｓｔｉｃ ｌｏｃａｌ ｓｅａｒｃｈ ａｌｇｏ⁃ ｒｉｔｈｍ ｆｏｒ ｕｎｓａｔｉｓｆｉａｂｌｅ ｃｏｒｅｓ ｅｘｔｒａｃｔｉｏｎ ［ Ｍ］． Ｈｅｉｄｅｌｂｅｒｇ： Ｓｐｒｉｎｇｅｒ， ２００７， ４７０７： ６４９⁃６５９． ［１１］ ＺＨＡＮＧ Ｊ， ＳＨＥＮ Ｓ， ＬＩ Ｓ． Ｔｒａｃｋｉｎｇ ｕｎｓａｔｉｓｆｉａｂｌｅ ｓｕｂｆｏｒ⁃ ｍｕｌａｓ ｆｒｏｍ ｒｅｄｕｃｅｄ ｒｅｆｕｔａｔｉｏｎ ｐｒｏｏｆ ［ Ｊ］． Ｊｏｕｒｎａｌ ｏｆ Ｓｏｆｔ⁃ ｗａｒｅ， ２００９， ４（１）： ４２⁃４９． ［１２］ＬＹＮＣＥ Ｉ， ＭＡＲＱＵＥＳ⁃ＳＩＬＶＡ Ｊ Ｐ． Ｏｎ ｃｏｍｐｕｔｉｎｇ ｍｉｎｉｍｕｍ ｕｎｓａｔｉｓｆｉａｂｌｅ ｃｏｒｅｓ［Ｃ］ ／ ／ Ｉｎｔｅｒｎａｔｉｏｎａｌ Ｓｙｍｐｏｓｉｕｍ ｏｎ Ｔｈｅｏ⁃ 第 ６ 期 殷明浩，等：不可满足子式研究 ·５０３·