Mostrar código-fonte de MAX-3SAT

'''MAX-3SAT''' é um problema em [[complexidade computacional]], uma subárea da [[ciência da computação]]. Este problema generaliza o [[problema da satisfatibilidade booleana]] (SAT), que é um [[problema de decisão]] dentro da teoria da complexidade. E é definido como:

''Dada uma [[Forma normal conjuntiva|3-CNF]] formula Φ (i.e. com no máximo 3 variáveis por cláusula), ache uma atribuição que satisfaz o maior número de cláusulas.''

'''MAX-3SAT''' é um problema canônico completo da classe de complexidade MAXSNP (ver Papadimitriou pg. 314).

== Aproximação ==
A versão de decisião de '''MAX-3SAT''' é [[NP-completa]]. No entanto, uma solução em tempo polinomial somente pode ser alcançada se P = NP. Uma aproximação por um fator de 2 pode ser alcançada com esse simples [[algoritmo]]:
* Coloque como saída a solução em que a maioria das cláusulas sejam satisfeitas, tanto quando todas as variáveis forem verdadeiras ou todas as variáveis fores falsas.
* Cada cláusula é satisfeita por uma das duas soluções, portanto, uma solução satisfaz, pelo menos, metade das cláusulas.
O algoritmo de Karloff-Zwick roda em tempo polinomial e satisfaz ≥ 7/8 das cláusulas.

== Teorema 1 (não-aproximação) ==
O teorema do PCP implica que existe um ε > 0 tal que (1-ε)-aproximação de '''MAX-3SAT''' é [[NP-difícil]].

Prova:

Pelo teorema PCP, qualquer problema NP-completo ''L'' ∈ ''PCP(O(log (n)), O(1))''. Para x ∈ ''L'', uma fórmula [[Forma normal conjuntiva|3-CNF]] Ψ<sub>x</sub> é construída tal que:
* ''x'' ∈ ''L'' ⇒ Ψ<sub>x</sub> é satisfatível
* ''x'' ∉ ''L'' ⇒ não mais que (1-ε)m cláusulas de Ψ<sub>x</sub> são satisfatíveis.
O verificador ''V'' lê todos os bits de uma vez i.e. faz consultas não-adaptativas. Isto é valido, pois o número de consultas permanece constante.
* Considere ''q'' como sendo o número de consultas.
* Enumerando randomicamente todas as strings ''R''<sub>i</sub> ∈ ''V'', obtemos ''poly(x)'' strings desde que o tamanho de cada string ''r(x) = O(log |x|)''.
* Para cada ''R''<sub>i</sub>
** ''V'' escolhe ''q'' posições ''i''<sub>1</sub>,...,''i''<sub>q</sub> e uma função booleana ''f''<sub>R</sub>: {0,1}<sup>q</sup>->{0,1} e aceita se e somente se ''f''<sub>R</sub>(π(i<sub>1</sub>,...,i<sub>q</sub>)). Aqui π se refere a prova obtida pelo oráculo.
O próximo passo é tentar encontrar uma fórmula booleana para simular isto. Introduzimos variáveis booleanas  ''x''<sub>1</sub>,...,''x''<sub>l</sub>, onde ''l'' é o tamanho da prova. Para demonstrar que o Verificador roda em tempo polinomial probabilístico, precisamos de uma correspondência entre o número de cláusulas satisfaríeis e a probabilidade de o Verificador aceitar.
* Para cada R, adicione cláusulas representadas por ''f''<sub>R</sub>(''x''<sub>i1</sub>,...,''x''<sub>iq</sub>) usando 2<sup>q</sup> cláusulas SAT. Cláusulas de tamanho ''q'' são convertidas para tamanho 3 adicionando uma nova variável (auxiliar) e.g. ''x''<sub>2</sub> ∨ ''x''<sub>10</sub> ∨ ''x''<sub>11</sub> ∨ ''x''<sub>12</sub> = ( ''x''<sub>2</sub> ∨ ''x''<sub>10</sub> ∨ ''y''<sub>R</sub>) ∧ ( <math>\bar{y_R}</math> ∨ ''x''<sub>11</sub> ∨ ''x''<sub>12</sub>). Isto requer no máximo de ''q''2<sup>q</sup> cláusulas 3-SAT.
* Se ''z'' ∈ ''L'' então
** existe uma prova π tal que ''V''<sup>π</sup> (''z'') aceita para todo ''R''<sub>i</sub>.
** Todas as cláusulas são satisfeitas se ''x''<sub>''i''</sub> = π(''i'') e a variável auxiliar são adicionadas corretamente.
* Se a entrada ''z'' ∉ ''L'' então
** Para cada atribuição de  ''x''<sub>1</sub>,...,''x''<sub>l</sub> and ''y''<sub>R</sub>'s, a prova correspondente π(''i'') = ''x''<sub>i</sub> causa a rejeição do Verificador para metade de todos os ''R'' ∈ {0,1}<sup>''r''(|''z''|)</sup>.
*** Para cada ''R'', uma cláusula que representa ''f''<sub>R</sub> falha.
*** Portanto a fração <math>\frac{1}{2} \frac{1}{q2^{q}}</math> da cláusula falha.
Pode-se concluir que, se este é válido para todos os problemas de NP-completos, então, o teorema PCP deve ser verdadeiro.

== Teorema 2 ==
Hosted <ref><cite class="citation journal" contenteditable="false">Håstad, Johan (2001). </cite></ref> demonstra um resultado mais conciso do Teorema 1, i.e. o valor mais conhecido para ε.

Construimos um verificador PCP para 3-SAT que lê somente 3 bits da prova.

''Pra cada ε > 0, existe um verificador PCP M para 3-SAT que lê uma string aleatória r de tamanho O(log(n)) e computa o resultado das posições i<sub>r</sub>, j<sub>r</sub>, k<sub>r</sub> na prova π e um bit b<sub>r</sub>. E aceita se somente se''

''π(i<sub>r</sub>) ⊕ π(j<sub>r</sub>) ⊕ π(k<sub>r</sub>) ⊕ = b<sub>r</sub>.''

O Verificador tem completude(1-ε) e solidez 1/2 + ε (referente a PCP ([[complexidade]])). O Verificador satisfaz

<math>z \in L \implies \exists \pi Pr[V^{\pi} (x) = 1] \ge 1 - \epsilon</math>

<math>z \not \in L \implies \forall \pi Pr[V^{\pi} (x) = 1] \le \frac{1}{2} + \epsilon</math>

Na primeira das duas equações onde temos a igualdade "=1" como costume, uma poderia encontrar a prova π resolvendo o sistema linear de equações (ver MAX-3LIN-EQN) implicando que [[P versus NP|P = NP]].
* Se z ∈ ''L'', uma fração ≥ (1- ε) de cláusulas são satisfeitas.
* Se z ∉ ''L'', então para uma (1/2- ε) fração de ''R'', 1/4 cláusulas são contraditas.
Isso é suficiente para provar a dificuldade da taxa de aproximação

<math>\frac{1-\frac{1}{4}(\frac{1}{2}-\epsilon)}{1-\epsilon} = \frac{7}{8} + \epsilon'</math>

== Problemas relacionados ==
'''MAX-3SAT(B)''' é restrito ao caso especial de '''MAX-3SAT''' onde cada variável ocorre no máximo em B cláusulas. Antes que o teorema PCP fosse provado, Papadimitriou and Yannakakis<ref>Christos Papadimitriou and Mihalis Yannakakis, Optimization, approximation, and complexity classes, Proceedings of the twentieth annual ACM symposium on Theory of computing, p.229-234, May 02–04, 1988.</ref> mostraram que para alguma constante fixa B, o problema é MAX SNP-difícil. Consequentemente com o teorema PCP, é também APX-difícil. Isto é útil porque '''MAX-3SAT(B)''' também pode ser usado para obter uma redução PTAS-preserving de forma que '''MAX-3SAT''' não pode. Provas de valores explícitos de ''B'' incluem: todo ''B ≥ 13'',<ref>Rudich et al., "Computational Complexity Theory," IAS/Park City Mathematics Series, 2004 page 108 [[:en:Special:BookSources/082182872X|ISBN 0-8218-2872-X]]</ref><ref>Sanjeev Arora, "[http://www.cs.princeton.edu/~arora/pubs/thesis.pdf Probabilistic Checking of Proofs and Hardness of Approximation Problems]," Revised version of a dissertation submitted at CS Division, U C Berkeley, in August 1994. </ref> e todo ''B ≥ 3''<ref name="acgkmsp">Ausiello, G., Crescenzi, P., Gambosi, G., Kann, V., Marchetti Spaccamela, A., and Protasi, M. (1999), Complexity and Approximation. </ref> (que é a melhor possibilidade).

Além disso, embora o problema de decisão 2SAT é solúvel em tempo polinomial, '''MAX-2SAT(3)''' também é  APX-defícil.<ref name="acgkmsp">Ausiello, G., Crescenzi, P., Gambosi, G., Kann, V., Marchetti Spaccamela, A., and Protasi, M. (1999), Complexity and Approximation. </ref>

A melhor possibilidade para taxa de aproximação para '''MAX-3SAT(B),''' como uma função de ''B,'' é no mínimo <math>7/8+\Omega(1/B)</math> e no máximo <math>7/8+O(1/\sqrt{B})</math>,<ref>Luca Trevisan. 2001. </ref> a não ser que '''NP'''='''RP'''. Alguns limites explicates das constantes de aproximação para certos valores de ''B'' são conhecidos.<ref>On some tighter inapproximability results, Piotr Berman and Marek Karpinski, Proc. </ref>
<ref>P. Berman and M. Karpinski, Improved Approximation Lower Bounds on Small Occurrence Optimization, 
[http://eccc.hpi-web.de/report/2003/008/ ECCC TR 03-008 (2003)]
</ref>
<ref>P. Berman, M. Karpinski and A. D. Scott, Approximation Hardness and Satisfiability of Bounded Occurrence Instances of SAT,
[http://eccc.hpi-web.de/report/2003/022/ ECCC TR 03-022 (2003)].</ref> Berman, Karpinski e Scott provaram que as instâncias "criticas" de '''MAX-3SAT''' na qual cada literal ocorre exatamente duas vezes, e cada cláusula tem tamanho 3, o problema é aproximado-difícil para algum fator constante.<ref>P. Berman, M. Karpinski and A. D. Scott, Approximation Hardness of Short Symmetric Instances of MAX-3SAT,
[http://eccc.hpi-web.de/report/2003/049/ ECCC TR 03-049 (2003).]</ref>

MAX-EkSAT é a versão parametrizada de '''MAX-3SAT''' onde cada cláusula tem exatamente <math>k</math> literais, para ''k'' ≥ 3. E pode ser eficientemente aproximada com uma taxa de aproximação de <math>1- (1/2)^{k}</math> usando ideias de teoria da codificação.

Foi provado que instâncias aleatórias de '''MAX-3SAT''' podem ser aproximadas por um fator de 9/8.<ref>W.F.de la Vega and M.Karpinski, 9/8-Approximation Algorithm for Random MAX-3SAT,
[http://eccc.hpi-web.de/report/2002/070/ ECCC TR 02-070 (2002)];RAIRO-Operations Research 41(2007),pp.95-107]</ref><div> <nowiki>[[Categoria:teoria da computação]]</nowiki><br>
</div>

== Referências ==
{{Reflist}}[http://www.cs.berkeley.edu/~luca/notes/ Lecture Notes from University of California, Berkeley]
[https://web.archive.org/web/20100702120650/http://www.cse.buffalo.edu/~atri/courses/coding-theory/ Coding theory notes at University at Buffalo]

[[Categoria:Complexidade]]
[[Categoria:Ciência da computação teórica]]