maximum satisfiability problem

The conjunctive normal form formula

:$(x\_0\backslash lor\; x\_1)\backslash land(x\_0\backslash lor\backslash lnot\; x\_1)\backslash land(\backslash lnot\; x\_0\backslash lor\; x\_1)\backslash land(\backslash lnot\; x\_0\backslash lor\backslash 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.

The MAX-SAT problem is OptP-complete,{{Cite journal|author = M. Krentel|title = The complexity of optimization problems| journal = Journal of Computer and System Sciences|volume = 36|pages=490–509|year=1988| issue=3 | doi=10.1016/0022-0000(88)90039-6 | hdl=1813/6559 |hdl-access=free}} 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.Mark Krentel. [https://www.sciencedirect.com/science/article/pii/0022000088900396/pdf?md5=6fa18c741f2eb2d204433ebf681c0c70&pid=1-s2.0-0022000088900396-main.pdf The Complexity of Optimization Problems]. Proc. of STOC '86. 1986.Christos Papadimitriou. Computational Complexity. Addison-Wesley, 1994.Cohen, Cooper, Jeavons. [https://www.researchgate.net/profile/Martin_Cooper3/publication/221632891_Lecture_Notes_in_Computer_Science/links/02e7e5343108bf0ed3000000/Lecture-Notes-in-Computer-Science.pdf A complete characterization of complexity for boolean constraint optimization problems]. CP 2004.

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.{{sfn|Vazirani|2001|p=131}}{{Cite journal|last1=Borchers|first1=Brian|last2=Furman|first2=Judith|date=1998-12-01|title=A Two-Phase Exact Algorithm for MAX-SAT and Weighted MAX-SAT Problems|journal=Journal of Combinatorial Optimization|language=en|volume=2|issue=4|pages=299–306|doi=10.1023/A:1009725216438|s2cid=6736614|issn=1382-6905}}{{Cite book|url=https://books.google.com/books?id=_GOVQRL50kcC&dq=weighted+max+sat&pg=PA393|title=Satisfiability Problem: Theory and Applications : DIMACS Workshop, March 11-13, 1996|last1=Du|first1=Dingzhu|last2=Gu|first2=Jun|last3=Pardalos|first3=Panos M.|date=1997-01-01|publisher=American Mathematical Soc.|isbn=9780821870808|language=en|pages=393}}

Randomly assigning each variable to be true with probability 1/2 gives an expected 2-approximation. More precisely, if each clause has at least {{var|k}} variables, then this yields a (1 − 2^−{{var|k}})-approximation.{{sfn|Vazirani|2001|loc=Lemma 16.2}} This algorithm can be derandomized using the method of conditional probabilities.{{sfn|Vazirani|2001|loc=Section 16.2}}

MAX-SAT can also be expressed using an integer linear program (ILP). Fix a conjunctive normal form formula {{var|F}} with variables {{var|x}}₁, {{var|x}}₂, ..., {{var|x}}_n, and let {{var|C}} denote the clauses of {{var|F}}. For each clause {{var|c}} in {{var|C}}, let {{var|S}}⁺_{{var|c}} and {{var|S}}⁻_{{var|c}} denote the sets of variables which are not negated in {{var|c}}, and those that are negated in {{var|c}}, respectively. The variables {{var|y}}_{{var|x}} of the ILP will correspond to the variables of the formula {{var|F}}, whereas the variables {{var|z}}_{{var|c}} will correspond to the clauses. The ILP is as follows:

The above program can be relaxed to the following linear program {{var|L}}:

The following algorithm using that relaxation is an expected (1-1/e)-approximation:{{sfn|Vazirani|2001|p=136}}

1. Solve the linear program {{var|L}} and obtain a solution {{var|O}}
2. Set variable {{var|x}} to be true with probability {{var|y}}_{{var|x}} where {{var|y}}_{{var|x}} is the value given in {{var|O}}.

This algorithm can also be derandomized using the method of conditional probabilities.

The 1/2-approximation algorithm does better when clauses are large whereas the (1-1/{{var|e}})-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 {{var|X}}.
2. Run the (derandomized) (1-1/e)-approximation to get a truth assignment {{var|Y}}.
3. Output whichever of {{var|X}} or {{var|Y}} maximizes the weight of the satisfied clauses.

This is a deterministic factor (3/4)-approximation.{{sfn|Vazirani|2001|loc=Theorem 16.9}}

On the formula

:$$F=\backslash underbrace\{(x\backslash lor\; y)\}\_\{\backslash text\{weight\; \}1\}\backslash land\; \backslash underbrace\{(x\backslash lor\backslash lnot\; y)\}\_\{\backslash text\{weight\; \}1\}\backslash land\backslash underbrace\{(\backslash lnot\; x\backslash lor\; z)\}\_\{\backslash text\{weight\; \}2+\backslash epsilon\}$$

where $\backslash epsilon\; >0$, the (1-1/{{var|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 {{var|x}} is chosen first during derandomization, the derandomized algorithms will pick a solution with total weight $3+\backslash epsilon$, whereas the optimal solution has weight $4+\backslash epsilon$.{{sfn|Vazirani|2001|loc=Example 16.11}}

The state-of-the-art algorithm is due to Avidor, Berkovitch and Zwick,{{cite book | last1=Avidor | first1=Adi | last2=Berkovitch | first2=Ido | last3=Zwick | first3=Uri | title=Approximation and Online Algorithms | chapter=Improved Approximation Algorithms for MAX NAE-SAT and MAX SAT | publisher=Springer Berlin Heidelberg | publication-place=Berlin, Heidelberg | volume=3879 | date=2006 | isbn=978-3-540-32207-8 | doi=10.1007/11671411_3 | pages=27–40}}{{cite journal | last1=Makarychev | first1=Konstantin | last2=Makarychev | first2=Yury | title=Approximation Algorithms for CSPs | journal=Drops-Idn/V2/Document/10.4230/Dfu.vol7.15301.287 | date=2017 | issn=1868-8977 | doi=10.4230/DFU.VOL7.15301.287 | page=39 pages, 753340 bytes| doi-access=free }} and its approximation ratio is 0.7968. They also give another algorithm whose approximation ratio is conjectured to be 0.8353.

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{{cite book | chapter-url=https://link.springer.com/chapter/10.1007/978-1-4613-0303-9_2 | doi=10.1007/978-1-4613-0303-9_2 | chapter=Approximate Algorithms and Heuristics for MAX-SAT | title=Handbook of Combinatorial Optimization | date=1998 | last1=Battiti | first1=Roberto | last2=Protasi | first2=Marco | pages=77–148 | isbn=978-1-4613-7987-4 }}

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.

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.

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-{{var|k}}SAT, where each clause has exactly {{var|k}} 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.Josep Argelich and Felip Manyà. [https://doi.org/10.1007%2Fs10732-006-7234-9 Exact Max-SAT solvers for over-constrained problems]. In Journal of Heuristics 12(4) pp. 375-392. Springer, 2006.
• 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.{{cite journal|last1=Jaulin|first1=L.|last2=Walter|first2=E.| title=Guaranteed robust nonlinear minimax estimation| journal=IEEE Transactions on Automatic Control|year=2002|volume=47|issue=11|pages=1857–1864|doi=10.1109/TAC.2002.804479| url=http://www.ensta-bretagne.fr/jaulin/paper_qminimax.pdf}}

• Boolean Satisfiability Problem
• Constraint satisfaction
• Satisfiability modulo theories

• http://www.satisfiability.org/
• https://web.archive.org/web/20060324162911/http://www.iiia.csic.es/~maxsat06/
• http://www.maxsat.udl.cat
• [http://www.nlsde.buaa.edu.cn/~kexu/benchmarks/max-sat-benchmarks.htm Weighted Max-2-SAT Benchmarks with Hidden Optimum Solutions]
• [http://www.cs.tau.ac.il/~azar/Methods-Class6.pdf Lecture Notes on MAX-SAT Approximation]

• {{Citation| last = Vazirani | first = Vijay V.

| author-link = Vijay Vazirani

| title = Approximation Algorithms

| year = 2001

| publisher = Springer-Verlag

| isbn = 978-3-540-65367-7

| url = https://doc.lagout.org/science/0_Computer%20Science/2_Algorithms/Approximation%20Algorithms%20%5bVazirani%202010-12-01%5d.pdf

}}

Category:Logic in computer science

Category:Combinatorial optimization

Category:Satisfiability problems