Maximum satisfiability problem

From Wikipedia, the free encyclopedia

In Computer Science, there are sets of problems similarly complex to each other (Computational complexity theory). Finding a method to efficiently solve one problem of the set means the method can be applied for all of them. A method able to solve MAX-SAT will be able to solve problems where an optimum solution has to be found (i.e. Optimization problems).

The Maximum Satisfiability problem (MAX-SAT), an FNP generalization of Satisfiability problem (SAT), asks for the maximum number of clauses which can be satisfied by any assignment. It has efficient approximation algorithms, but is NP-hard to solve exactly. Particularly, it is complete in OptP[(O(log n)] 1, or in PNP[log n] 2.
On the other hand, it is APX-complete, meaning there is no polynomial-time approximation scheme (PTAS) for this problem unless P=NP.

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

There has been developed many exact solvers during the last years, many of them presented in the SAT Conference.

Is is expected that during 2006 will be hosted the first MAX-SAT evaluation, as it was successfully done for pseudo-boolean and QBF.

[edit] See also

[edit] External links

[edit] References

1. Mark Krentel. The Complexity of Optimization Problems. 1986. ACM.

2. C. Papadimitriou. Computational Complexity. Addison-Wesley, 1994.