<p>If the function is linear, then you can reduce to MaxSAT. Then there are some related formalisms like pseudo-boolean optimizatin (PBO) or integer linear programming (ILP).</p>

CC BY-SA 3.0
2013-07-15T17:00:34.413Z
2013-07-15T17:00:34.413Z
Mikolas
<p>In general, since the instance may have no solution at all, the problem is not too meaningful (or if you want to find the minimum weight solution if one exists and fail otherwise, then the problem becomes at least as hard as SAT itself).</p>

<p>Therefore, you may want to impose restrictions to ensure that 1) a solution always exists, and 2) smaller weight solutions are harder to find than those with larger weight.</p>

<p>One such restriction would be to not allow negations in the instance. In this case, the all-ones assignment is always trivially satisfying and more generally we will have a monotone structure in the solution space (so that flipping variables from 0 to 1 will keep a satisfying assignment feasible). In this case, it is easy to see that the problem of finding minimum-weight satisfying assignment for SAT (with $n$ variables and $m$ clauses) becomes <em>equivalent</em> to the minimum set-cover problem (with universe size $m$ and $n$ sets). Namely, the $i$th element of the universe belongs to the $j$th set in the set-cover instance iff the $i$th clause in the SAT instance contains the $j$th variable. If you restrict yourself to the special case of 2-SAT, the problem becomes equivalent to minimum vertex cover, and in general for $k$-SAT the problem would be equivalent to minimum $k$-uniform hypergraph vertex cover.</p>

CC BY-SA 3.0
2013-07-15T19:00:43.973Z
2013-07-15T19:00:43.973Z
Mahdi Cheraghchi
<p>This problem is obviously as difficult as SAT itself (for instance for a function that assigns each solution weight $0$) but I suppose it can, for general function $f$ behave differently from SAT. Namely it can still be difficult even if the underlying SAT problem has sufficiently large number of solutions to make it easy to solve. </p>

<p>Do you perhaps have more information about the function that defines the cost of the solution? The question in the present form does not seem sensible.</p>

CC BY-SA 3.0
2013-07-15T14:49:28.143Z
2013-07-15T14:49:28.143Z
Rasto S.
<p>SAT can be converted to Independent Set. Weighted independent set is a well studied problem.</p>

<p><a href="http://link.springer.com/article/10.1023%2FA%3A1008765214400" rel="nofollow">A Note on the Approximation of a Minimum Weight Maximal Independent Set</a></p>

CC BY-SA 3.0
2013-07-15T17:11:31.547Z
2013-07-15T17:11:31.547Z
Russell Easterly
<p>Given an arbitrary SAT instance, I would like to find the solution with the minimum weight. The weight of a valid assignment is computed using a function.</p>

<p>Is this a known problem or are there other problems that I can reduce this one to?</p>

CC BY-SA 3.0
2013-07-15T17:24:57.543Z
What's the function?  The answer will depend upon what your objective function looks like.
D.W.
CC BY-SA 3.0
2013-07-16T12:12:52.743Z
Plus, do not use "weight" for the name  of your function, as the weight of a binary assignment is commonly used to refer to its number of ones. "score" would be more adequate.
J.y B.y
<sat>
Weighted SAT: is this a known problem?
Mike Cops
# Weighted SAT: is this a known problem?

(Asked by: username_0 on 2013-07-15)

Given an arbitrary SAT instance, I would like to find the solution with the minimum weight. The weight of a valid assignment is computed using a function.

Is this a known problem or are there other problems that I can reduce this one to?

**Tags:** sat
> **Comments:**
> **username_1**: What's the function?  The answer will depend upon what your objective function looks like.  
> **username_2**: Plus, do not use "weight" for the name  of your function, as the weight of a binary assignment is commonly used to refer to its number of ones. "score" would be more adequate.  

---

## 4 answers

### Answer by username_3 on 2013-07-15. Score: 3

If the function is linear, then you can reduce to MaxSAT. Then there are some related formalisms like pseudo-boolean optimizatin (PBO) or integer linear programming (ILP).


---

### Answer by username_4 on 2013-07-15. Score: 2

In general, since the instance may have no solution at all, the problem is not too meaningful (or if you want to find the minimum weight solution if one exists and fail otherwise, then the problem becomes at least as hard as SAT itself).

Therefore, you may want to impose restrictions to ensure that 1) a solution always exists, and 2) smaller weight solutions are harder to find than those with larger weight.

One such restriction would be to not allow negations in the instance. In this case, the all-ones assignment is always trivially satisfying and more generally we will have a monotone structure in the solution space (so that flipping variables from 0 to 1 will keep a satisfying assignment feasible). In this case, it is easy to see that the problem of finding minimum-weight satisfying assignment for SAT (with $n$ variables and $m$ clauses) becomes *equivalent* to the minimum set-cover problem (with universe size $m$ and $n$ sets). Namely, the $i$th element of the universe belongs to the $j$th set in the set-cover instance iff the $i$th clause in the SAT instance contains the $j$th variable. If you restrict yourself to the special case of 2-SAT, the problem becomes equivalent to minimum vertex cover, and in general for $k$-SAT the problem would be equivalent to minimum $k$-uniform hypergraph vertex cover.


---

### Answer by username_5 on 2013-07-15. Score: 2

This problem is obviously as difficult as SAT itself (for instance for a function that assigns each solution weight $0$) but I suppose it can, for general function $f$ behave differently from SAT. Namely it can still be difficult even if the underlying SAT problem has sufficiently large number of solutions to make it easy to solve.

Do you perhaps have more information about the function that defines the cost of the solution? The question in the present form does not seem sensible.


---

### Answer by username_6 on 2013-07-15. Score: 1

SAT can be converted to Independent Set. Weighted independent set is a well studied problem.

[A Note on the Approximation of a Minimum Weight Maximal Independent Set](http://link.springer.com/article/10.1023%2FA%3A1008765214400)


---

