Content deleted Content added
No edit summary |
Siddharthist (talk | contribs) Add section on weighted MAX-SAT, including an ILP, the relaxed LP, and two approximation algorithms from Vazirani |
||
Line 12:
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. The Complexity of Optimization Problems. Proc. of STOC '86. 1986.</ref><ref>Christos Papadimitriou. Computational Complexity. Addison-Wesley, 1994.</ref><ref>Cohen, Cooper, Jeavons. 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}}
=== 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>, -->
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}}
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:
{|
| 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|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.
==Solvers==
Line 52 ⟶ 111:
== References ==
<references />
* {{Citation| last = Vazirani | first = Vijay V.
| authorlink = Vijay Vazirani
| title = Approximation Algorithms
| year = 2001
| publisher = Springer-Verlag
| isbn = 3-540-65367-8
| url = http://www.cc.gatech.edu/fac/Vijay.Vazirani/book.pdf
}}
[[Category:Logic in computer science]]
| |||