about ubcsat

[刘燕丽]

Hi,I am Leva.  I am doing some works about maxsat algorithm. I want to use ubcsat to change the initial value of  upper bounds. May I ask whether  the ubcsat  can be used to reduce the upper bounds for partial maxsat instances.  Partial maxsat instances include the hard clauses and soft clauses. For SAT problem, all the clauses should be soft clauses which maybe be true ,maybe be false. However, hard clauses must be true. so , if  I change the initial UB of partial maxsat instances with uncsat, is it correct?

thank you very much! I wish I get your Email for this questions.    thanks again!

Best wishes!




                                                                                                                                                                                                                                Leva

 

[Dave Tompkins]

Hi Leva.

Yes, you can do this with a *weighted* max-sat problem (instance).

if you have Y soft clauses, you can weight each hard clause with the
value of Y+1, and all soft clauses with a weight of 1.

Then, if/when the weight of all unsatisfied clauses is <= Y, you have
satisfied all of the hard clauses.

A less elegant solution to this that uses regular (unweighted) max-sat
is as follows: for each hard clause, add Y duplicates of it to the
instance. This achieves the same goal but will change the behaviour
of many algorithms (perhaps in good ways, perhaps in bad ways). One
disadvantage of this approach is that increases the memory
requirements and can slow down algorithms considerably as there is
more "bookkeeping" to keep track of.

-Dave

> --
> You received this message because you are subscribed to the Google Groups
> "ubcsat" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to ubcsat+un...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.