Solving SMT Problems with a Costly Decision Procedure by Finding Minimum Satisfying Assignments of Boolean Formulas

摘要

An SMT-solving procedure can be implemented by using a SAT solver to ?nd a satisfying assignment of the propositional skeleton of the predicate formula and then deciding the feasibility of the assignment using a particular decision procedure. The complexity of the decision procedure depends on the size of the assignment. In case that the runtime of the solving is dominated by the decision procedure it is convenient to ?nd short satisfying assignments in the SAT solving phase. Unfortunately most of the modern state-of-the-art SAT solvers always output a complete assignment of variables for satis?able formulas even if they can be satis?ed by assigning truth values to only a fraction of the variables. In this paper, we ?rst describe an application in the code performance modeling domain, which requires SMT-solving with a costly decision procedure. Then we focus on the problem of ?nding minimum-size satisfying partial truth assignments. We describe and experimentally evaluate several methods how to solve this problem. These include reduction to partial maximum satis?ability – PMAXSAT, PMINSAT, pseudo-Boolean optimization and iterated SAT solving. We examine the methods experimentally on existing benchmark formulas as well as on a new benchmark set based on the performance modeling scenario.