Content deleted Content added
Siddharthist (talk | contribs) Add section on weighted MAX-SAT, including an ILP, the relaxed LP, and two approximation algorithms from Vazirani |
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 |
||
| (33 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
=== 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 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}}▼
▲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
MAX-SAT can also be expressed using an [[Integer linear program|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: ▼
==== (1-1/{{var|e}})-approximation ====
▲MAX-SAT can also be expressed using an [[
{|
| maximize
Line 66 ⟶ 71:
|}
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 89 ⟶ 111:
==Related problems==
There are many problems related to the satisfiability of conjunctive normal form Boolean formulas.
* [[Decision problem]]s:
* The weighted maximum satisfiability problem (Weighted MAX-SAT) asks for the maximum weight which can be satisfied by any assignment, given a set of weighted clauses.▼
** [[Boolean satisfiability problem|3SAT]]
* The soft satisfiability problem (soft-SAT), given a set of SAT problems, asks for the maximum number of sets which can be satisfied by any assignment.<ref>Josep Argelich and Felip Manyà. [http://www.springerlink.com/content/870v1535q0h51717/ Exact Max-SAT solvers for over-constrained problems]. In Journal of Heuristics 12(4) pp. 375-392. Springer, 2006.</ref>▼
* Optimization problems, where the goal is to maximize the number of clauses satisfied:
▲* The minimum satisfiability problem.
** MAX-SAT, and the corresponded weighted version [[#Weighted MAX-SAT|Weighted MAX-SAT]]
* The MAX-SAT problem can be extended to the case where the variables of the [[constraint satisfaction problem]] belong 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 Transaction on Automatic Control|year=2002|volume=47| url=http://www.ensta-bretagne.fr/jaulin/paper_qminimax.pdf}} </ref>▼
** MAX-{{var|k}}SAT, where each clause has exactly {{var|k}} variables:
*** [[2-satisfiability#Maximum-2-satisfiability|MAX-2SAT]]
*** [[MAX-3SAT]]
*** [[MAXEkSAT]]
▲** The
▲** The soft satisfiability problem (soft-SAT), given a set of SAT problems, asks for the maximum number of
** 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 ==
Line 104 ⟶ 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 112 ⟶ 142:
<references />
* {{Citation| last = Vazirani | first = Vijay V.
|
| title = Approximation Algorithms
| year = 2001
| publisher = Springer-Verlag
| isbn = 978-3-540-65367-
| url = https://doc.lagout.org/science/0_Computer%20Science/2_Algorithms/Approximation%20Algorithms%20%5bVazirani%202010-12-01%5d.pdf
}}
| |||