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?

  • 2
    $\begingroup$ This may be a stupid question, but why is finding a minimal satisfying assignment (as you've defined it) any harder than finding a (standard) satisfying assignment? If you have a satisfying assignment, can't you just greedily consider the variables one at a time, and "remove" each variable if, after removal of that variable, the remaining subset of variables (with their induced assignment) is still satisfying? $\endgroup$
    – Neal Young
    Sep 27, 2020 at 0:38
  • 1
    $\begingroup$ Do you really want minimal in the local sense you defined (you can't remove any one variable), or do you want minimal in the global sense (there is no other partial assignment with fewer variables that makes the CNF formula true)? $\endgroup$
    – D.W.
    Sep 27, 2020 at 1:49
  • $\begingroup$ Oh wow, now I feel dumb. You both are 100% correct. I've mixed up the terminology of "minimal" and "minimum". The problem I want to solve is actually trivial. The set cover problem - and minimum unsatisfiable core problem - consider the global minimum, which is much more challenging. $\endgroup$ Sep 27, 2020 at 1:54


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.