In computational complexity theory, the Maximum Satisfiability problem (MAX-SAT) is the problem of determining the maximum number of clauses, of a given Boolean formula, that can be satisfied by some assignment. It is an FNP generalization of SAT.
The MAX-SAT problem is NP-hard, since its solution easily leads to the solution of the boolean satisfiability problem, which is NP-complete. In particular for unweighted, and for weighted.
From another point of view, it is also APX-complete, and thus does not admit a PTAS unless P = NP.[1][2][3] MAX-SAT is one of the optimization extensions of the boolean satisfiability problem, which is the problem of determining if the variables of a given Boolean formula can be assigned in such a way as to make the formula evaluate to TRUE. If the clauses are restricted to have at most 2 literals, as in 2-satisfiability, we get the MAX-2SAT problem. If they are restricted to at most 3 literals per clause, as in 3-satisfiability, we get the MAX-3SAT problem.
Contents |
There are several extensions to MAX-SAT:
Many exact solvers for MAX-SAT have been developed during recent years, and many of them were presented in the well-known conference on the boolean satisfiability problem and related problems, the SAT Conference. In 2006 the SAT Conference hosted the first MAX-SAT evaluation comparing performance of practical solvers for MAX-SAT, as it has done in the past for the pseudo-boolean satisfiability problem and the quantified boolean formula problem. Because of its NP-hardness, large-size MAX-SAT instances cannot be solved exactly, and one must resort to approximation algorithms and heuristics [5]
There are several solvers submitted to the last Max-SAT Evaluations: