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.
Example The conjunctive normal form formula
( x 0 ∨ x 1 ) ∧ ( x 0 ∨ ¬ x 1 ) ∧ ( ¬ x 0 ∨ x 1 ) ∧ ( ¬ x 0 ∨ ¬ x 1 ) {\displaystyle (x_{0}\lor x_{1})\land (x_{0}\lor \lnot x_{1})\land (\lnot x_{0}\lor x_{1})\land (\lnot x_{0}\lor \lnot x_{1})}
is not satisfiable: no matter which truth values are assigned to its two variables, at least one of its four clauses will be false. However, it is possible to assign truth values in such a way as to make three out of four clauses true; indeed, every truth assignment will do this. Therefore, if this formula is given as an instance of the MAX-SAT problem, the solution to the problem is the number three.
Hardness The MAX-SAT problem is OptP-complete, and thus NP-hard (as a decision problem), since its solution easily leads to the solution of the boolean satisfiability problem, which is NP-complete. It is also difficult to find an approximate solution of the problem, that satisfies a number of clauses within a guaranteed approximation ratio of the optimal solution. More precisely, the problem is APX-complete, and thus does not admit a polynomial-time approximation scheme unless P = NP.
Weighted MAX-SAT More generally, one can define a weighted version of MAX-SAT as follows: given a conjunctive normal form formula with non-negative weights assigned to each clause, find truth values for its variables that maximize the combined weight of the satisfied clauses. The MAX-SAT problem is an instance of Weighted MAX-SAT where all weights are 1.
Approximation algorithms
1/2-approximation Randomly assigning each variable to be true with probability 1/2 gives an expected 2-approximation. More precisely, if each clause has at least k variables, then this yields a (1 − 2−k)-approximation. This algorithm can be derandomized using the method of conditional probabilities.
(1-1/e)-approximation MAX-SAT can also be expressed using an integer linear program (ILP). Fix a conjunctive normal form formula F with variables x1, x2, ..., xn, and let C denote the clauses of F. For each clause c in C, let S+c and S−c denote the sets of variables which are not negated in c, and those that are negated in c, respectively. The variables yx of the ILP will correspond to the variables of the formula F, whereas the variables zc will correspond to the clauses. The ILP is as follows:
The above program can be relaxed to the following linear program L:
The following algorithm using that relaxation is an expected (1-1/e)-approximation:
Solve the linear program L and obtain a solution O Set variable x to be true with probability yx where yx is the value given in O. This algorithm can also be derandomized using the method of conditional probabilities.
3/4-approximation The 1/2-approximation algorithm does better when clauses are large whereas the (1-1/e)-approximation does better when clauses are small. They can be combined as follows:
Run the (derandomized) 1/2-approximation algorithm to get a truth assignment X. Run the (derandomized) (1-1/e)-approximation to get a truth assignment Y. Output whichever of X or Y maximizes the weight of the satisfied clauses. This is a deterministic factor (3/4)-approximation.
Example On the formula
F = ( x ∨ y ) ⏟ weight 1 ∧ ( x ∨ ¬ y ) ⏟ weight 1 ∧ ( ¬ x ∨ z ) ⏟ weight 2 + ϵ {\displaystyle F=\underbrace {(x\lor y)} _{{\text{weight }}1}\land \underbrace {(x\lor \lnot y)} _{{\text{weight }}1}\land \underbrace {(\lnot x\lor z)} _{{\text{weight }}2+\epsilon }}
where ϵ > 0 {\displaystyle \epsilon >0} , the (1-1/e)-approximation will set each variable to True with probability 1/2, and so will behave identically to the 1/2-approximation. Assuming that the assignment of x is chosen first during derandomization, the derandomized algorithms will pick a solution with total weight 3 + ϵ {\displaystyle 3+\epsilon } , whereas the optimal solution has weight 4 + ϵ {\displaystyle 4+\epsilon } .
State of the art The state-of-the-art algorithm is due to Avidor, Berkovitch and Zwick, and its approximation ratio is 0.7968. They also give another algorithm whose approximation ratio is conjectured to be 0.8353.
… excerpt ends here. Continue reading the full article.
