极小SMT不可满足子式的提取算法

摘要

解释可满足性模理论(Satisfiability Modulo Theories,SMT)公式不可满足的原因在众多领域都具有非常重要的理论与应用价值,而极小不可满足子式能够为公式不可满足的原因提供精确的解释,帮助应用领域的自动化工具迅速定位错误,准确诊断问题失败的本质缘由.本文针对极小SMT不可满足子式的求解问题,提出了SMT公式搜索树及其三类结点的概念,并证明了不可满足子式、极小不可满足子式与三类结点之间的映射关系。基于这种映射关系,采用宽度优先的搜索策略,提出了宽度优先搜索的极小SMT不可满足子式求解算法。基于业界公认的SMT Competition 2007测试集进行了实验,结果表明:该算法能够有效地求解极小不可满足子式.