基于否证蕴含的极小一阶不可满足子式求解算法  

An Algorithm for Extracting Minimal Unsatisfiable Subformulae in First-Order Logic Based on Refutation Implication

作　　者：张建民[1] 沈胜宇[1] 李思昆[1] 

机构地区：[1]国防科学技术大学计算机学院,长沙410073

出　　处：《计算机学报》2010年第3期415-426,共12页Chinese Journal of Computers

基　　金：国家自然科学基金(60603088)资助~~

摘　　要：解释公式不可满足的原因在软件分析与验证等众多领域都具有非常重要的理论与应用价值,而极小不可满足子公式能够为公式不可满足的原因提供精炼的解释,帮助应用领域的自动化工具迅速定位错误,准确地诊断问题失败的本质缘由.文中针对极小一阶不可满足子式的求解问题,引入了否证蕴含图及其正向与逆向可达结点的概念,并证明了不可满足子式与否证蕴含图之间的关系.基于二者的关系,提出了基于冲突分析与否证蕴含的极小一阶不可满足子式求解算法,并融合了蕴含图剪枝技术,以提高算法效率.通过实验与当前最优的深度优先搜索算法进行了比较,结果表明:文中的算法显著优于深度优先搜索算法,并且随着公式复杂度的增加,性能优势更加明显.Explaining the causes of infeasibility of formulae has theoretical and practical applications in various fields,such as software verification and analysis.A minimal unsatisfiable subformula can provide a succinct explanation of infeasibility,and help automatic tools to rapidly locate the errors,and determine the underlying reasons for the failure.The authors introduce the definition of refutation implication graph and its forward and backward reachable vertices,and the relationship between the minimal unsatisfiable subformulae and the refutation implication graph.Based on the relationship,the authors propose an algorithm based on conflict analysis and refutation implication,in which a technique called refutation implication graph pruning is implemented.The experimental results on practical benchmarks show that the proposed algorithm outperforms the depth-first search algorithm.While the formulae are becoming more complex,the algorithm is much faster than the depth-first search algorithm.

关 键 词：一阶逻辑公式 可满足模理论问题 极小不可满足子式 消解否证 否证蕴含图 

分 类 号：TP302[自动化与计算机技术—计算机系统结构]