Generating diverse solutions in SAT

Abstract

This paper considers the Diverse k Set problem in SAT, that is, the problem of efficiently generating a number of diverse solutions (satisfying assignments) given a propositional formula. We provide an extensive analysis of existing algorithms for this problem in a newly developed framework and propose new algorithms. While existing algorithms adapt modern SAT solvers to solve Diverse k Set by changing their polarity selection heuristic, our new algorithms adapt the variable ordering strategy as well. Our experimental results demonstrate that the proposed algorithms improve the diversification quality of the solutions on large industrial instances of Diverse k Set arising in SAT-based semiformal verification of hardware. © 2011 Springer-Verlag.