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?
2
-
3$\begingroup$ What's the function? The answer will depend upon what your objective function looks like. $\endgroup$– D.W.Jul 15, 2013 at 17:24
-
1$\begingroup$ 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. $\endgroup$– J..y B..yJul 16, 2013 at 12:12
Add a comment
|
4 Answers
$\begingroup$
$\endgroup$
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).
$\begingroup$
$\endgroup$
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.
$\begingroup$
$\endgroup$
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.
answered Jul 15, 2013 at 19:00
$\begingroup$
$\endgroup$
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
