Search code examples
optimizationsatisfiabilityconjunctive-normal-form

SAT Solving for Optimization

Suppose you have a CNF formula with some variables marked special.
Is there a way to make a SAT Solver (say, minisat) find a solution maximizing the number of special variables assigned to true?

Solution

  • What you (I) want is called Partial Max Sat. There is a solver called qmaxsat, which seems to work well enough.