Maximum satisfiability problem


In computational complexity theory, the maximum satisfiability problem 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
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 NP-hard, 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 variables, then this yields a -approximation. This algorithm can be derandomized using the method of conditional probabilities.

(1-1/)-approximation

MAX-SAT can also be expressed using an integer linear program. Fix a conjunctive normal form formula with variables 1, 2,..., n, and let denote the clauses of. For each clause in, let + and − denote the sets of variables which are not negated in, and those that are negated in, respectively. The variables of the ILP will correspond to the variables of the formula, whereas the variables will correspond to the clauses. The ILP is as follows:
The above program can be relaxed to the following linear program :
The following algorithm using that relaxation is an expected -approximation:
  1. Solve the linear program and obtain a solution
  2. Set variable to be true with probability where is the value given in.
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 -approximation does better when clauses are small. They can be combined as follows:
  1. Run the 1/2-approximation algorithm to get a truth assignment.
  2. Run the -approximation to get a truth assignment.
  3. Output whichever of or maximizes the weight of the satisfied clauses.
This is a deterministic factor -approximation.

Example

On the formula
where, the -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 is chosen first during derandomization, the derandomized algorithms will pick a solution with total weight, whereas the optimal solution has weight.

Solvers

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 in general be solved exactly, and one must often resort to approximation algorithms
and heuristics
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. 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.

Related problems

There are many problems related to the satisfiability of conjunctive normal form Boolean formulas.