Content deleted Content added
No edit summary |
m clarified that MAX-SAT is NP-hard as a decision problem. it's said in the same sentence that it's OptP-complete, while OptP and NP belong to different contexts |
||
| (34 intermediate revisions by 24 users not shown) | |||
Line 1:
{{Short description|Problem in computational complexity theory}}
In [[computational complexity theory]], the '''maximum satisfiability problem''' ('''MAX-SAT''') is the problem of determining the maximum number of clauses, of a given [[Propositional formula|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.
Line 9 ⟶ 10:
==Hardness==
The MAX-SAT problem is OptP-complete,<ref>{{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}}</ref> 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 [[approximation algorithm|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.<ref>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.</ref><ref>Christos Papadimitriou. Computational Complexity. Addison-Wesley, 1994.</ref><ref>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.</ref>
== 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.{{sfn|Vazirani|2001|p=131}}<ref>{{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}}</ref><ref>{{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}}</ref>
=== Approximation algorithms ===
<!-- Given a conjunctive normal form formula {{var|F}} with variables {{var|x}}<sub>1</sub>, {{var|x}}<sub>2</sub>, ..., {{var|x}}<sub>n</sub>, -->
==== 1/2-approximation ====
Randomly assigning each variable to be true with probability 1/2 gives an [[Expected value|expected]] [[Approximation algorithm#Performance guarantees|2-approximation]]. More precisely, if each clause has at least {{var|k}} variables, then this yields a (1 − 2<sup>−{{var|k}}</sup>)-approximation.{{sfn|Vazirani|2001|loc=Lemma 16.2}} This algorithm can be [[Randomized algorithm#Derandomization|derandomized]] using the [[method of conditional probabilities]].{{sfn|Vazirani|2001|loc=Section 16.2}}
==== (1-1/{{var|e}})-approximation ====
MAX-SAT can also be expressed using an [[integer linear program]] (ILP). Fix a conjunctive normal form formula {{var|F}} with variables {{var|x}}<sub>1</sub>, {{var|x}}<sub>2</sub>, ..., {{var|x}}<sub>n</sub>, and let {{var|C}} denote the clauses of {{var|F}}. For each clause {{var|c}} in {{var|C}}, let {{var|S}}<sup>+</sup><sub>{{var|c}}</sub> and {{var|S}}<sup>−</sup><sub>{{var|c}}</sub> 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}}<sub>{{var|x}}</sub> of the ILP will correspond to the variables of the formula {{var|F}}, whereas the variables {{var|z}}<sub>{{var|c}}</sub> will correspond to the clauses. The ILP is as follows:
{|
| maximize
| <math>\sum_{c \in C} w_c\cdot z_c</math>
|
| (maximize the weight of the satisfied clauses)
|-
| subject to
| <math>z_c\leq\sum_{x\in S_c^+} y_x+\sum_{x\in S_c^-} (1-y_x)</math>
| for all <math>c\in C</math>
| (clause is true [[If and only if|iff]] it has a true, non-negated variable or a false, negated one)
|-
|
| <math>z_c \in \{0,1\}</math>
| for all <math>c\in C</math>.
| (every clause is either satisfied or not)
|-
|
| <math>y_x \in \{0,1\}</math>
| for all <math>x\in F</math>.
| (every variable is either true or false)
|}
The above program can be [[Linear programming relaxation|relaxed]] to the following linear program {{var|L}}:
{|
| maximize
| <math>\sum_{c \in C} w_c\cdot z_c</math>
|
| (maximize the weight of the satisfied clauses)
|-
| subject to
| <math>z_c\leq\sum_{x\in S_c^+} y_x+\sum_{x\in S_c^-} (1-y_x)</math>
| for all <math>c\in C</math>
| (clause is true [[If and only if|iff]] it has a true, non-negated variable or a false, negated one)
|-
|
| <math>0\leq z_c \leq 1</math>
| for all <math>c\in C</math>.
|-
|
| <math>0\leq y_x\leq 1</math>
| for all <math>x\in F</math>.
|}
The following algorithm using that relaxation is an expected (1-1/[[E (mathematical constant)|e]])-approximation:{{sfn|Vazirani|2001|p=136}}
# Solve the linear program {{var|L}} and obtain a solution {{var|O}}
# Set variable {{var|x}} to be true with probability {{var|y}}<sub>{{var|x}}</sub> where {{var|y}}<sub>{{var|x}}</sub> is the value given in {{var|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/{{var|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 {{var|X}}.
# Run the (derandomized) (1-1/e)-approximation to get a truth assignment {{var|Y}}.
# 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}}
===== Example =====
On the formula
:<math display="block">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}</math>
where <math>\epsilon >0</math>, 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 <math>3+\epsilon</math>, whereas the optimal solution has weight <math>4+\epsilon</math>.{{sfn|Vazirani|2001|loc=Example 16.11}}
==== State of the art ====
The state-of-the-art algorithm is due to Avidor, Berkovitch and Zwick,<ref>{{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}}</ref><ref name="t481">{{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 }}</ref> 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 [[0-1 integer programming|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 algorithm]]s
and [[Metaheuristic|heuristics]]<ref>{{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 }}</ref>
There are several solvers submitted to the last Max-SAT Evaluations:
Line 30 ⟶ 111:
==Related problems==
There are many problems related to the satisfiability of conjunctive normal form Boolean formulas.
* [[Decision problem]]s:
** [[2-satisfiability|2SAT]]
** [[Boolean satisfiability problem|3SAT]]
* Optimization problems, where the goal is to maximize the number of clauses satisfied:
** MAX-SAT, and the corresponded weighted version [[#Weighted MAX-SAT|Weighted MAX-SAT]]
** MAX-{{var|k}}SAT, where each clause has exactly {{var|k}} variables:
*** [[2-satisfiability#Maximum-2-satisfiability|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.<ref>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.</ref>
** 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.<ref>{{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}}</ref>
== See also ==
Line 45 ⟶ 134:
== External links ==
* 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]
Line 52 ⟶ 141:
== References ==
<references />
* {{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]]
| |||