<p>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 <strong>partial</strong> 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)</p>

CC BY-SA 3.0
2012-03-29T02:57:58.800Z
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?
Madhusudan.C.S
CC BY-SA 3.0
2012-03-29T03:00:36.830Z
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?
Madhusudan.C.S
CC BY-SA 3.0
2012-03-29T08:54:25.540Z
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. http://www.springerlink.com/content/k3w23h8j6j5413j0/
Mikolas
CC BY-SA 3.0
2012-03-30T04:18:46.963Z
Ah coolness! Thank you very much! Reading that paper now.
Madhusudan.C.S
CC BY-SA 3.0
2012-04-08T20:39:07.650Z
@Madhusudan.C.S did you figure it out? I realized that my response might have been a little bit rushed.
Mikolas
CC BY-SA 3.0
2012-04-22T14:36:39.170Z
Thank you very much for following it up. I am so stupid that I haven't even checked back at this thread in some time. I will sit down implementing this in the next few days and will certainly let you know (or may be bug you :P ) while working on it. Thanks again!
Madhusudan.C.S
CC BY-SA 3.0
2012-06-07T01:53:11.390Z
After procrastinating on this for months, I have finally implemented this. Thank you very much for the answer. I have done it the way you suggested. The source code is available here: https://github.com/madhusudancs/PL241-MCS-Compiler/tree/maxsat-allocator Thank you very much again!
Madhusudan.C.S
CC BY-SA 3.0
2012-03-28T20:22:01.370Z
2012-03-28T20:22:01.370Z
Mikolas
<p>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 <a href="http://repository.lib.ncsu.edu/ir/handle/1840.16/4594" rel="nofollow">http://repository.lib.ncsu.edu/ir/handle/1840.16/4594</a> 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?</p>

<p>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>

<p>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.</p>

<cc.complexity-theory><sat><reductions>
Reduction/transformation from MinCostSat to MaxSat
Madhusudan.C.S
# Reduction/transformation from MinCostSat to MaxSat

(Asked by: username_0 on 2012-03-28)

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.

**Tags:** cc.complexity-theory, sat, reductions


---

## 1 answers

### Answer by username_1 on 2012-03-28. Score: 1

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)

> **Comments:**
> **username_0**: 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?  
> **username_0**: 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?  
> **username_1**: 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. http://www.springerlink.com/content/k3w23h8j6j5413j0/  
> **username_0**: Ah coolness! Thank you very much! Reading that paper now.  
> **username_1**: @username_0 did you figure it out? I realized that my response might have been a little bit rushed.  
> **username_0**: Thank you very much for following it up. I am so stupid that I haven't even checked back at this thread in some time. I will sit down implementing this in the next few days and will certainly let you know (or may be bug you :P ) while working on it. Thanks again!  
> **username_0**: After procrastinating on this for months, I have finally implemented this. Thank you very much for the answer. I have done it the way you suggested. The source code is available here: https://github.com/madhusudancs/PL241-MCS-Compiler/tree/maxsat-allocator Thank you very much again!  

---

