SMTBCF: Efficient Backbone Computing for SMT Formulas

摘要

SMT (Satisfiable Module Theory) formulas have been widely used in practical applications. In some of the applications, including finding program bugs, plainly solving an SMT formula is sufficient. For other applications, besides solving the SMT formula, backbone variables of the SMT formulas are also needed in order to tackle the practical problems including finding invariant of certain properties in program analysis. This paper proposed a new approach SMTBCF to compute backbone variables for SMT formulas in order to accelerate the computing of backbone variables in SMT formulas and increase the efficiency of SMT formulas in practical applications. SMTBCF is the first algorithm that uses the backbone predicates to find part of the backbone variables in the SMT formulas. SMTBCF is also the first algorithm that uses the constants in the relating predicates of a backbone variable to quickly find the Unsat-isfiable Evaluation of the backbone variable. In this way, SMTBCF is able to find backbone variables of SMT formulas, reduce the number of SMT solving in SMT backbone computing, and increase the efficiency of backbone variables in SMT formulas.