No label defined (Q4247437)

In the maximum satisfiability (MAX-SAT) problem one is given a Boolean formula in conjunctive normal form, that is, as a conjunction of clauses, each clause being a disjunction. The task is then to find an assignment to the variables that satisfies the maximum number of clauses. If one associates a positive weight to each clause one obtains the weighted MAX-SAT (MAX W-SAT) problem; one is then to determine an assignment to the variables that maximizes the sum of the weights of the satisfied clauses. Algorithms for these problems are surveyed in this handbook chapter. Exact algorithms, approximation algorithms, and local search heuristics are considered; some theoretical results regarding these are also presented. As the title of the chapter indicates, results on approximation and local search algorithms are well covered, whereas exact algorithms are given a more cursory treatment. For the entire collection see [Zbl 0903.90001].