All-SAT Using Minimal Blocking Clauses

The All-SAT problem deals with determining all the satisfying assignments that exist for a given propositional logic formula. This problem occurs in verification applications including predicate abstraction and unbounded model checking. A typical All-SAT solver is based on iteratively computing satisfying assignments using a traditional Boolean satisfiability (SAT) solver and adding blocking clauses which are the complement of the total/partial assignments. We argue that such an algorithm is doing more work than needed and introduce new algorithms that are more efficient. Experiments show that these algorithms generate solutions with up to 14X fewer partial assignments and are up to three orders of magnitude faster.