Maximum satisfiability problem

From Wikipedia, the free encyclopedia

The introduction to this article provides insufficient context for those unfamiliar with the subject.
Please help improve the article with a good introductory style.

Satisfiability 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.

The Maximum Satisfiability problem (MAX-SAT) asks for the maximum number of clauses which can be satisfied by any assignment. It is an NP-hard problem.

Even more strongly, it is APX-complete, meaning there is no polynomial-time approximation scheme (PTAS) for this problem unless P=NP. It is also complete in OptP[(O(log n)] 1, or in P^{NP[log n]} 2.

There are several extensions to MAX-SAT:

The weighted maximum satisfiability problem (Weighted MAX-SAT) asks for the maximum weight which can be satisfied by any assignment, given a set of weighted clauses.
The partial maximum satisfiability problem (PMAX-SAT) asks for the maximum number of clauses which can be satisfied by any assignment of a given subset of clauses. The rest of the clauses must be satisfied.
The soft satisfiability problem (soft-SAT), given a set of SAT problems, asks for the maximum number of sets which can be satisfied by any assignment.

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.