2
$\begingroup$

I recently ran into MaxSAT competitions website and was looking into the problem formulation. I vaguely remember reading somewhere that MinCostSAT and MaxSAT are related to each other and one can be reduced to another. I read here http://repository.lib.ncsu.edu/ir/handle/1840.16/4594 that the MaxSAT to MinCostSAT reduction is to use a slack variable for each clause in the MaxSAT and giving it the value of 1 and all other boolean variables 0 reduces the problem to MinCostSAT. Can some one please tell me how does this work? How does it make the MaxSAT instance the instance of MinCostSAT?

Also, what is the reduction from MinCostSAT to MaxSAT or may be even weighted MaxSAT, especially considering the fact that I have a problem to which I know the cost of assignments and want to minimize this cost and if I have the off the shelf solvers available like the ones that have won MaxSAT competitions, how do I go about reducing my MinCostSAT problem to MaxSAT?

P.S. I hope this won't be rejected as an implementation level question since my question is really about reduction. I can think about implementing it, if I know the reduction at least.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
1
$\begingroup$

First thing to realize is that minimization can be rephrased as maximization of the negated literal (and vice a versa). So minimizing $x+y$ is the same as maximizing $\lnot x + \lnot y$. So to get a partial maxsat problem you just add the unit clauses $\lnot x$, $\lnot y$ as soft clauses and the original clauses as hard. (partial MaxSAT is crucial here, weighted partial MaxSAT is needed if you have coefficients in the minimization function)

Improve this answer
$\endgroup$
7
  • $\begingroup$ First of all thank you very much for the answer. So if I understand correctly the rationale behind partial MaxSAT is that, hard clauses must be satisfied whatsoever and soft clauses must be attempted to be satisfied as much as possible to make the entire cost minimize as much as possible, right? $\endgroup$
    – Madhusudan.C.S
    Mar 29, 2012 at 2:57
  • $\begingroup$ Secondly, if I have co-efficients for literals, how does partial weighted MaxSAT work? Say I have 40x + 50y as my cost function and I have the clause in CNF as say $\lnot x\ \ y$. So what should be the weight of the clause in the MaxSAT version? The sum of the co-efficients? Or should the clauses be set to the highest weight to ensure that they are the hard clauses? And what should be the weights of the negated unit clauses that represent the cost function? $\endgroup$
    – Madhusudan.C.S
    Mar 29, 2012 at 3:00
  • $\begingroup$ You still encode the original SAT problem as hard clauses. The unit clauses will have the weights equal to the coefficient to the corresponding term in the function. Check out e.g. springerlink.com/content/k3w23h8j6j5413j0 $\endgroup$
    – Mikolas
    Mar 29, 2012 at 8:54
  • $\begingroup$ Ah coolness! Thank you very much! Reading that paper now. $\endgroup$
    – Madhusudan.C.S
    Mar 30, 2012 at 4:18
  • $\begingroup$ @Madhusudan.C.S did you figure it out? I realized that my response might have been a little bit rushed. $\endgroup$
    – Mikolas
    Apr 8, 2012 at 20:39

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.