SAT Solving for Optimization

Question

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?

Answer 1

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

Answer 2

You can use a PBC solver such as minisat+ http://minisat.se/MiniSat+.html They solve regular CNF files with additional constraints called pseudo Boolean constraints Minisat+ also supports optimization of such constraints and from my understanding it solves your problem

Let x1, .... xn be the variables you want to maximize the number o truth assignments Then you can define the constraints maximize +1 x1 ..... +1 xn minisat+ solves such optimization problems

Answer 3

Not sure if all of these can handle the indication of special variables, but at least wikipedia gives some direction for the search:

There are several solvers submitted to the last Max-SAT Evaluations:

• Branch and Bound based: Clone, MaxSatz (based on Satz), IncMaxSatz, IUT_MaxSatz, WBO.
• Satisfiability based: SAT4J, QMaxSat.
• Unsatisfiability based: msuncore, WPM1, PM2.

Checking the description for all of them should be managable.