8
$\begingroup$

Trying to find the optimal solution to WEIGHTED-MAX-3SAT, the weighted version of the 3-SAT optimization problem, is NP-hard. In fact, even approximating the non-weighted version of MAX-SAT arbitrarily well is provably NP-hard by the PCP Theorem.

A canonical algorithm for approximating WEIGHTED-MAX-3SAT is MAX-WalkSAT. Looking around I found some information on other algorithms (i.e. branch-and-bound, the DPL algorithm) which are commonly used to find solutions to 3-SAT or (unweighted) MAX-3SAT, but I didn't see any discussion of how well these would work for the weighted version. Intuitively, without being adapted they would not work as well.

I'm wondering what other algorithms are commonly used to approximate WEIGHTED-MAX-SAT, if there are well-known WEIGHTED-MAX-SAT solvers, and the relative quality of these algorithms/solvers.

Improve this question
$\endgroup$
8
  • $\begingroup$ This is not really on topic as it is asking about heuristics and implementation experience rather than provable algorithms. $\endgroup$ – Warren Schudy Oct 9 '10 at 14:43
  • 5
    $\begingroup$ @Warren: I think perhaps that is taking things a little too far. The question basically amounts to "What algorithms are good for WEIGHTED-MAX-SAT?" which is a perfectly reasonable question to ask. Many SAT solvers rely on heuristics too. Even though their worst case performance is poor, they do surprisingly well. If every question related to only exactly proved complexity results, I doubt the site would be very popular. After all, we already have the zoo. $\endgroup$ – Joe Fitzsimons Oct 10 '10 at 0:43
  • 3
    $\begingroup$ The MAXSAT competition has divisions for weighted and for unweighted: maxsat.udl.cat/10/results $\endgroup$ – Radu GRIGore Oct 11 '10 at 17:35
  • 2
    $\begingroup$ Here's one readable description of one of the algorithms used: scholar.google.com/scholar?cluster=14077294269217865108 $\endgroup$ – Radu GRIGore Oct 11 '10 at 17:38
  • 11
    $\begingroup$ @Warren: In the '80s and '90s, at many universities, theoretical computer science was very unpopular and looked down upon by the rest of computer science because it was viewed as unconnected to practice. Eventually, Google and other successes convinced them that we were worth talking to. Let's please not close off the lines of communication from the other side now, after having worked so long to open them. That would be very bad for the field, not to mention the TCS job market. $\endgroup$ – Peter Shor Oct 20 '10 at 14:16
5
$\begingroup$

Well, this can be formulated as the problem of finding the ground state of an Ising-like Hamiltonian with 3-local terms. These don't occur naturally, but you would expect them to cool similarly to other systems, so simulated annealing should work just fine for the weighted version.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Joe, after thinking about this I can't see how simulated annealing is different from MAX-WalkSAT. Isn't MAX-WalkSAT just a form of simulated annealing applied to this particular problem? $\endgroup$ – Huck Bennett Nov 23 '10 at 9:19
  • $\begingroup$ @Huck: It depends on how you choose which variables to flip. $\endgroup$ – Joe Fitzsimons Nov 24 '10 at 11:21
4
$\begingroup$

I think one can do reduction by simply duplicating the formulas according to their weight and therefore upper and lower bound results for unweighted 3-SAT also apply to weighted versions, with arbitrarily small lost. And according to a classical result of Johan Håstad, it is NP-hard to approximate 3-SAT beyond 7/8, which is the performance of assigning random values.

I am not sure about the performance of algorithms used in practical.

Improve this answer
$\endgroup$
3
  • $\begingroup$ That reduction is not polynomial in the length of the weight. If you give me a weight of length O(n) then I'll have to make 2^(O(n)) copies of the clause. $\endgroup$ – Huck Bennett Oct 9 '10 at 6:39
  • $\begingroup$ Furthermore, if I restricted the problem to MAX-SAT with non-repeating clauses (still NP-hard) that would not work. $\endgroup$ – Huck Bennett Oct 9 '10 at 6:45
  • $\begingroup$ surely all lower bounds (hardness results) for unweighted 3-SAT apply also to weighted 3-SAT (which subsumes unweighted 3-SAT). $\endgroup$ – Neal Young May 2 '13 at 3:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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