Abstrakt
Most modern state-of-the-art SAT solvers output a complete assignment of variables for satisfiable formulas. However, in many cases the formulas can be satisfied by partial truth assignments, assigning truth values only to a fraction of the variables.
We describe a scenario from SMT-solving where short satisfying partial assignments are desirable. We show the practical relevance of this scenario by describing its application in the code performance modeling domain.
The advantage of finding a shorter satisfying assignment is caused by a time-consuming decision procedure. The time spent by finding the shortest assignment by far outweighs the running time of the decision procedure of the described domain.
The problem of finding minimum-size satisfying partial truth assignments is well-known in the field of Boolean optimization as the shortest implicant problem. We describe and experimentally evaluate several methods of solving this problem.
These include reduction to partial maximum/minimum satisfiability — PMAXSAT/PMINSAT, pseudo-Boolean optimization and iterated SAT solving. We examine these methods experimentally on existing benchmark formulas as well as on our new benchmark set based on the performance modeling scenario.
Our experiments on the chosen benchmarks indicate that the iterated SAT solving is the fastest method.