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

摘要：

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

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

所属期刊栏目：21

分类号：TP391.7(计算技术、计算机技术)

资助基金：国家自然科学基金60603088, 90707003

在线出版日期：2009-08-26（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：984-990