I'm in need of a SAT solver that outputs minimal assignments - that is, a set of assignments to a subset of all propositional variables such that substitution into the CNF formula makes each clause true, and such that the satisfiaction fails when any of the variables in the solution set is removed.
One possible application area is All-SAT, where one can take a standard incremental SAT solver and continually add minimal blocking clauses by negating the solutions, essentially converting the problem to a reduced form of DNF.
I've found two general methods for deriving minimal assignments. The first is to apply a minimal hitting set/set cover algorithm (or a heuristic) to the substituted CNF clauses (discussed here). The second is to apply an approach with unsatisfiable cores (discussed here).
Do any SAT solvers have strategies for minimal assignment extraction built-in? Are there any modifications to the CDCL procedure that take into account variable ordering/subsumption to make it all in one process?
