Jump to content

Maximum satisfiability problem

Edit links
From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by Luc Jaulin (talk | contribs) at 11:07, 18 May 2013 (I added a link to the concept of relaxed intersection which is closely related to the MAX-SAT problem). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

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.

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.

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.[4]
  • The minimum satisfiability problem.
  • The MAX-SAT problem can be extended to the case where the variables of the constraint satisfaction problem belong the set of reals. The problem amounts
 to finding the smallest q such that the q relaxed intersection of the m constraints is not empty.[5]

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 [6]

Solvers

There are several solvers submitted to the last Max-SAT Evaluations:

  • Branch and Bound based: Clone, MaxSatz (based on Satz), IncMaxSatz, IUT_MaxSatz, WBO.
  • Satisfiability based: SAT4J, QMaxSat.
  • Unsatisfiability based: msuncore, WPM1, PM2.

See also

References

  1. ^ Mark Krentel. The Complexity of Optimization Problems. Proc. of STOC '86. 1986.
  2. ^ Christos Papadimitriou. Computational Complexity. Addison-Wesley, 1994.
  3. ^ Cohen, Cooper, Jeavons. A complete characterization of complexity for boolean constraint optimization problems. CP 2004.
  4. ^ Josep Argelich and Felip Manyà. Exact Max-SAT solvers for over-constrained problems. In Journal of Heuristics 12(4) pp. 375-392. Springer, 2006.
  5. ^ Jaulin, L.; Walter, E. (2002). "Guaranteed robust nonlinear minimax estimation" (PDF). IEEE Transaction on Automatic Control. 47.
  6. ^ R. Battiti and M. Protasi. Approximate Algorithms and Heuristics for MAX-SAT Handbook of Combinatorial Optimization, Vol 1, 1998, 77-148, Kluwer Academic Publishers.
Retrieved from "https://en.wikipedia.org/w/index.php?title=Maximum_satisfiability_problem&oldid=555634803"