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

作者：张建民; 沈胜宇; 李思昆

来源：计算机辅助设计与图形学学报, 2009, (07): 984-990.

• 可满足性模理论
• 极小不可满足子式
• DPLL(T)
• 搜索树
• 宽度优先搜索 satisfiability modulo theories(SMT)
• minimal unsatisfiable subformula
• DPLL(T)
• searching tree
• breadth first search

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

• 单位
  中国人民解放军国防科学技术大学