search

niklasso / minisat

A minimalistic and high-performance SAT solver
minisat.se
Other
1.01k stars 382 forks source link

Find a solution that contains as few values assigned to be true as possible. #39

Closed wfz0755 closed 4 years ago

wfz0755 commented 4 years ago

Hello guys,

May I ask if there is a way to assign those useless variables to be false in SAT(or try to find the feasible solution that contains the least number of true variables)? For example, in an already solved instance, if a variable x can either be true or false and the solution is still feasible. Then I would rather it be false, which is beneficial in my current use case,

Lastly, thanks for sharing such an elegant SAT solver!

yxliang01 commented 4 years ago

I think you are looking for a MaxSAT solver, instead of SAT solver.

wfz0755 commented 4 years ago

I think you are looking for a MaxSAT solver, instead of SAT solver. Oh really? But in my scenario, a feasible solution is still required. But for MaxSAT, according to Wikipedia, it tries to determine the maximum number of clauses that can be satisfied. So they might be different.

yxliang01 commented 4 years ago

Yes, MaxSAT will give you a model of the formula. You can think of this, you have a SAT formula F, then you can also have a set of soft constraints on the negation of each variable (1 negation is 1 clause). By trying to find a model that most of the soft constraints are satisfied, you have your problem solved I believe.

liffiton commented 4 years ago

To expand on that a bit, consider the formula (a v b v c)(!b v c). Many MaxSAT solvers let you set some clauses as hard (must be satisfied) and others as soft (can be "relaxed" or left unsatisfied w/ some cost). Add the original two clauses as hard clauses and add three soft clauses: (!a) (!b) (!c). The MaxSAT solver will find a model that satisfies the hard [original] clauses and sets as many variables as possible to False.

If you don't need a globally optimal solution and your application needs an answer faster than a MaxSAT solver provides one, you might look into setting the variables' "user polarity" in newVar() instead. By telling the solver to try False first, you might end up with a model with more False assignments, but I think that might really depend on a lot of things about your constraints and be somewhat unpredictable.

wfz0755 commented 4 years ago

Ah, I get what you guys mean. Thank you so much for your patient explanation! @yxliang01 @liffiton Then I will try the "use polarity" way first and see if the problem can be mitigated. By the way, I may also try out MaxSAT, is there any good recommendation on MaxSAT solvers (that provides straight forward APIs and relatively efficient)?

liffiton commented 4 years ago

I'm not sure which MaxSAT solvers are made to be used via an API; most I know of are primarily (often solely) command line tools. And it also depends on your language. For example, SAT4J is made as a library, but it's in Java so will only be easily accessible from JVM-based languages. If you're okay running a separate program to solve your MaxSAT instances, you might look through the solvers in a recent MaxSAT Evaluation. That page just provides source downloads; searching for each solver's homepage might help you find documentation or other indications of whether they're suitable for integration within another program.

wfz0755 commented 4 years ago

Got it, I will look into it! Really appreciate your help @liffiton :)