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 in conjunctive normal form, that can be made true by an assignment of truth values to the variables of the formula.
It is a generalization of the Boolean satisfiability problem, which asks whether there exists a truth assignment that makes all clauses true.
The conjunctive normal form formula is not satisfiable: no matter which truth values are assigned to its two variables, at least one of its four clauses will be false.
More precisely, the problem is APX-complete, and thus does not admit a polynomial-time approximation scheme unless P = NP.
[12] The state-of-the-art algorithm is due to Avidor, Berkovitch and Zwick,[13][14] and its approximation ratio is 0.7968.
Because of its NP-hardness, large-size MAX-SAT instances cannot in general be solved exactly, and one must often resort to approximation algorithms and heuristics[15] There are several solvers submitted to the last Max-SAT Evaluations: MAX-SAT is one of the optimization extensions of the boolean satisfiability problem, which is the problem of determining whether the variables of a given Boolean formula can be assigned in such a way as to make the formula evaluate to TRUE.
There are many problems related to the satisfiability of conjunctive normal form Boolean formulas.