# Reduction/transformation from MinCostSat to MaxSat

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.

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)
• 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? Mar 29 '12 at 3:00