Solving SMT Problems with a Costly Decision Procedure by Finding Minimum Satisfying Assignments of Boolean Formulas
Abstract
An SMT-solving procedure can be implemented by using a SAT solver to find 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 find 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 satisfiable formulas even if they can be satisfied by assigning truth values to only a fraction of the variables.
In this paper,we first 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 finding minimum-size satisfying partial truth assignments.
We describe and experimentally evaluate several methods how to solve this problem. These include reduction to partial maximum satisfiability - 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.