0
$\begingroup$

I am currently trying to solve the Minimum Vertex Cover problem via a Weighted MAX SAT solver, but I am stuck with the model. The transformation to a simple SAT is straightforward since every node can be a variable and every edge a clause with a disjunction between start and end node, but I have a problem introducing the minimum boundary. I thought of adding clauses with each just containing a negated variable in order to inhibit that simply all variables are set to true. But this does not work in all instances. Could you hint me on how I could construct that?

$\endgroup$
  • $\begingroup$ It doesn't work because all the covering clauses must be satisfied, while the unit clauses may be unsatisfied. Anything you can do with the weights? $\endgroup$ – Fabio Somenzi Dec 8 '18 at 15:05
  • $\begingroup$ That was exactly my problem. That's why I thought that playing with the clause weights may create an equivalent for the minimum constraint. But I am not exactly sure how. $\endgroup$ – multiplex Dec 9 '18 at 9:54
  • $\begingroup$ Make the weight of a "mandatory" clause large enough that it outweighs all "optional" clauses together. $\endgroup$ – Fabio Somenzi Dec 9 '18 at 14:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.