CAJ | 학술논문

极小不可满足子式能够为可满足性模理论(SMT)公式的不可满足的原因提供精确的解释,帮助自动化工具迅速定位错误.针对极小SMT不可满足子式的求解问题,提出了SMT公式搜索树及其3类结点的概念,并给出了不可满足子式、极小不可满足子式与3类结点之间的映射关系.基于这种映射关系,采用宽度优先的搜索策略提出了宽度优先搜索的极小SMT不可满足子式求解算法.基于业界公认的SMT Competition 2007测试集进行实验的结果表明,该算法能够有效地求解极小不可满足子式.
겁소불가만족자식능구위가만족성모이론(SMT)공식적불가만족적원인제공정학적해석,방조자동화공구신속정위착오.침대겁소SMT불가만족자식적구해문제,제출료SMT공식수색수급기3류결점적개념,병급출료불가만족자식、겁소불가만족자식여3류결점지간적영사관계.기우저충영사관계,채용관도우선적수색책략제출료관도우선수색적겁소SMT불가만족자식구해산법.기우업계공인적SMT Competition 2007측시집진행실험적결과표명,해산법능구유효지구해겁소불가만족자식.
A minimal unsatisfiable subformula can provide a succinct explanation of infeasibility of formulae in satisfiability modulo theories (SMT), and could be used in automatic tools to rapidly locate the errors. We present the definitions of searching tree for a formula in SMT and three kinds of nodes, and discuss the relationship between minimal unsatisfiable subformula and the nodes. Based on the relationship, we propose a breadth-first-search algorithm to derive minimal unsatisfiable subformulae in SMT. We have evaluated the effectiveness of the algorithm on SMT Competition 2007 industrial benchmarks. Experimental results show that the breadth-first-search algorithm can effectively compute minimal unsatisfiable subformula.