求解极小SMT不可满足子式的宽度优先搜索算法

作     者：张建民 沈胜宇 李思昆 Zhang Jianmin;Shen Shengyu;Li Sikun

作者机构：国防科学技术大学计算机学院长沙410073 

基　　金：国家自然科学基金(60603088 90707003) 

出 版 物：《计算机辅助设计与图形学学报》 (Journal of Computer-Aided Design & Computer Graphics)

年 卷 期：2009年第21卷第7期

页      码：984-990页

摘      要：极小不可满足子式能够为可满足性模理论(SMT)公式的不可满足的原因提供精确的解释,帮助自动化工具迅速定位错误.针对极小SMT不可满足子式的求解问题,提出了SMT公式搜索树及其3类结点的概念,并给出了不可满足子式、极小不可满足子式与3类结点之间的映射关系.基于这种映射关系,采用宽度优先的搜索策略提出了宽度优先搜索的极小SMT不可满足子式求解算法.基于业界公认的SMT Competition2007测试集进行实验的结果表明,该算法能够有效地求解极小不可满足子式.

主 题 词：可满足性模理论 极小不可满足子式 DPLL(T) 搜索树 宽度优先搜索 

学科分类：081203[081203] 08[工学] 0835[0835] 0812[工学-测绘类] 

核心收录：

馆 藏 号：203771955...