Maximum satisfiability problem

Template:Short description 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\vee x_1)\wedge (x_0\vee \mathrm{\neg }{x}_1)\wedge (\mathrm{\neg }{x}_0\vee x_1)\wedge (\mathrm{\neg }{x}_0\vee \mathrm{\neg }{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.Template:Sfn

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 Template:Var variables, then this yields a (1 − 2^{−Template:Var})-approximation.Template:Sfn This algorithm can be derandomized using the method of conditional probabilities.Template:Sfn

(1-1/Template:Var)-approximation

MAX-SAT can also be expressed using an integer linear program (ILP). Fix a conjunctive normal form formula Template:Var with variables Template:Var₁, Template:Var₂, ..., Template:Var_n, and let Template:Var denote the clauses of Template:Var. For each clause Template:Var in Template:Var, let Template:Var⁺_Template:Var and Template:Var⁻_Template:Var denote the sets of variables which are not negated in Template:Var, and those that are negated in Template:Var, respectively. The variables Template:Var_Template:Var of the ILP will correspond to the variables of the formula Template:Var, whereas the variables Template:Var_Template:Var will correspond to the clauses. The ILP is as follows:

maximize	$\sum _{c\in C}{w}_c\cdot z_c$		(maximize the weight of the satisfied clauses)
subject to	$z_c\le \sum _{x\in S_c^{+}}{y}_x+\sum _{x\in S_c^{-}}(1-y_x)$	for all $c\in C$	(clause is true iff it has a true, non-negated variable or a false, negated one)
	$z_c\in \{0,1\}$	for all $c\in C$.	(every clause is either satisfied or not)
	$y_x\in \{0,1\}$	for all $x\in F$.	(every variable is either true or false)

The above program can be relaxed to the following linear program Template:Var:

maximize	$\sum _{c\in C}{w}_c\cdot z_c$		(maximize the weight of the satisfied clauses)
subject to	$z_c\le \sum _{x\in S_c^{+}}{y}_x+\sum _{x\in S_c^{-}}(1-y_x)$	for all $c\in C$	(clause is true iff it has a true, non-negated variable or a false, negated one)
	$0\le z_c\le 1$	for all $c\in C$.
	$0\le y_x\le 1$	for all $x\in F$.

The following algorithm using that relaxation is an expected (1-1/e)-approximation:Template:Sfn

1. Solve the linear program Template:Var and obtain a solution Template:Var
2. Set variable Template:Var to be true with probability Template:Var_Template:Var where Template:Var_Template:Var is the value given in Template:Var.

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/Template:Var)-approximation does better when clauses are small. They can be combined as follows:

1. Run the (derandomized) 1/2-approximation algorithm to get a truth assignment Template:Var.
2. Run the (derandomized) (1-1/e)-approximation to get a truth assignment Template:Var.
3. Output whichever of Template:Var or Template:Var maximizes the weight of the satisfied clauses.

This is a deterministic factor (3/4)-approximation.Template:Sfn

Example

On the formula

$$F=\underset{\text{weight }1}{\underbrace{(x\vee y)}}\wedge \underset{\text{weight }1}{\underbrace{(x\vee \mathrm{\neg }y)}}\wedge \underset{\text{weight }2+ϵ}{\underbrace{(\mathrm{\neg }x\vee z)}}$$

where $ϵ>0$, the (1-1/Template:Var)-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 Template:Var is chosen first during derandomization, the derandomized algorithms will pick a solution with total weight $3+ϵ$, whereas the optimal solution has weight $4+ϵ$.Template:Sfn

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.

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:

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

Special cases

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.

• Decision problems:
  • 2SAT
  • 3SAT
• Optimization problems, where the goal is to maximize the number of clauses satisfied:
  • MAX-SAT, and the corresponded weighted version Weighted MAX-SAT
  • MAX-Template:VarSAT, where each clause has exactly Template:Var variables:
    • MAX-2SAT
    • MAX-3SAT
    • MAXEkSAT
  • 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 those problems which can be satisfied by any assignment.
  • The minimum satisfiability problem.
• The MAX-SAT problem can be extended to the case where the variables of the constraint satisfaction problem belong to the set of reals. The problem amounts to finding the smallest q such that the q-relaxed intersection of the constraints is not empty.

See also

• Boolean Satisfiability Problem
• Constraint satisfaction
• Satisfiability modulo theories

External links

• http://www.satisfiability.org/
• https://web.archive.org/web/20060324162911/http://www.iiia.csic.es/~maxsat06/
• http://www.maxsat.udl.cat
• Weighted Max-2-SAT Benchmarks with Hidden Optimum Solutions
• Lecture Notes on MAX-SAT Approximation

References

• Template:Citation