基于否证蕴含的极小一阶不可满足子式求解算法*张建民+,沈胜宇,李思昆(国防科技大学计算机学院,湖南长沙410073)AnAlgorithmforExtractingMinimalUnsatisfiableSubformulaeinFirst-orderLogicBasedonRefutationImplication*ZHANGJian-Min+,SHENSheng-Yu,LISi-Kun(SchoolofComputer,NationalUniversityofDefenseTechnology,Changsha410073,China)Abstract:Explainingthecausesofinfeasibilityofformulaehastheoreticalandpracticalapplicationsinvariousfields,suchassoftwareverificationandanalysis.Aminimalunsatisfiablesubformulacanprovideasuccinctexplanationofinfeasibility,andhelpautomatictoolstorapidlylocatetheerrors,anddeterminetheunderlyingreasonsforthefailure.Weintroducethedefinitionofrefutationimplicationgraphanditsforwardandbackwardreachablevertices,andtherelationshipbetweentheminimalunsatisfiablesubformulaeandtherefutationimplicationgraph.Basedontherelationship,weproposeanalgorithmbasedonconflictanalysisandrefutationimplication,inwhichatechniquecalledrefutationimplicationgraphpruningisimplemented.Wereportexperimentalresultsonpracticalbenchmarks,ascomparedwiththebestknowndepth-firstsearchalgorithm.Theresultsshowthatouralgorithmoutperformsthedepth-firstsearchalgorithm.Whiletheformulaearebecomingmorecomplex,ouralgorithmismuchfasterthanthedepth-firstsearchalgorithm.Keywords:First-orderformula;SatisfiabilityModuloTheories(SMT);minimalunsatisfiablesubformulae;resolutionrefutation;refutationimplicationgraph摘要:解释公式不可满足的原因在软件分析与验证等众多领域都具有非常重要的理论与应用价值，而极小不可满足子公式能够为公式不可满足的原因提供精炼的解释，帮助应用领域的自动化工具迅速定位错误，准确地诊断问题失败的本质缘由。本文针对极小一阶不可满足子式的求解问题，引入了否证蕴含图及其正向与逆向可达结点的概念，并证明了不可满足子式与否证蕴含图之间的关系。基于二者的关系，提出了基于冲突分析与否证蕴含的极小一阶不可满足子式求解算法，并融合了蕴含图剪枝技术，以提高算法效率。通过实验与当前最优的深度优先搜索算法进行了比较，结果表明：本文的算法显著优于深度优先搜索算法，并且随着公式复杂度的增加，性能优势更加明显。关键词:一阶逻辑公式;可满足模理论问题;极小不可满足子式;消解否证;否证蕴含图中图法分类号:TP302文献标识码:A近年来，命题逻辑的可满足求解技术得到了飞速地发展，涌现了众多高效的SAT求解器，目前SAT求解**本课题得到国家自然科学基金(No.60603088)资助.作者简介:张建民(1979－),男,山西平遥人,博士生,主要研究领域为计算机辅助验证方法,E-mail:jmzhang@nudt.edu.cn,联系地址:国防科技大学计算机学院博士生队,电话:13786126649;沈胜宇(1975－),男,博士,副研究员,主要研究领域为计算机辅助设计与验证方法;李思昆(1941－),男,教授,博士生导师,CCF高级会员,主要研究领域为计算机辅助设计与验证方法,虚拟现实.器已经成为软件分析与验证等领域的重要工具。但是，命题逻辑限于其相对较弱的表达能力，无法表达许多领域的问题，例如，软件的分析与验证[1]、实时系统的验证[2]等；而在另外一些应用中，如汇编代码与RTL级Verilog代码的验证问题[3]，布尔逻辑虽然也能够表达与处理，但由于其抽象层次较低，例如字变量会转换为一组无关的布尔变量，因此大大增加了问题的规模，显著提高了空间与时间的开销。而基于非量化一阶逻辑的可满足问题，即可满足性模理论(SatisfiabilityModuloTheories，SMT)问题恰好弥补了SAT技术的不足，迅速成为验证领域的研究热点。可满足性模理论问题源于实际应用需求，例如软件的形式化验证、电子设计自动化与人工智能等众多领域的问题，都能够规约为非量化一阶逻辑公式，采用SMT求解器来解决。当公式不可满足时，通常要求查找不可满足的原因，诊断与定位问题的错误，这就要求移除公式中与不可满足无关的短句，只保留一部分短...