<p>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.</p>
<p>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.</p>
<p>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 <a href="https://sites.cs.ucsb.edu/%7Enestan/pdf/VLSID14.pdf" rel="nofollow noreferrer">here</a>). The second is to apply an approach with unsatisfiable cores (discussed <a href="https://stackoverflow.com/questions/41425514/partial-assignments-in-z3/41448059#41448059">here</a>).</p>
<p>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?</p>

CC BY-SA 4.0
2020-09-27T00:38:04.480Z
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?
Neal Young
CC BY-SA 4.0
2020-09-27T01:49:27.587Z
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)?
D.W.
CC BY-SA 4.0
2020-09-27T01:54:40.007Z
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.
user1318416
<sat>
SAT solvers & SAT solving methods admitting minimal satisfying assignments
user1318416
# SAT solvers & SAT solving methods admitting minimal satisfying assignments

(Asked by: username_0 on 2020-09-26)

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](https://sites.cs.ucsb.edu/%7Enestan/pdf/VLSID14.pdf)). The second is to apply an approach with unsatisfiable cores (discussed [here](https://stackoverflow.com/questions/41425514/partial-assignments-in-z3/41448059#41448059)).

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?

**Tags:** sat
> **Comments:**
> **username_1**: 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?  
> **username_2**: 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)?  
> **username_0**: 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.  

---

## 0 answers

