Wikipédia

Problema de satisfatibilidade máxima

Na teoria da complexidade computacional, o problema satisfatibilidade máxima (MAX-SAT) é o problema de determinar o número máximo de cláusulas, de uma determinada fórmula booleana na Forma normal conjuntiva, a qual pode ser feita verdadeira por uma atribuição de valores verdadeiros para as variáveis ​​de a fórmula. É uma generalização do Problema de satisfatibilidade booliana, que pergunta se existe uma atribuição verdadeira que faz todas as cláusulas verdade.

Exemplo editar

A formula para a forma normal conjuntiva

 

não é satisfativel: não importa qual valores verdade são atribuídos às suas duas variáveis​​, pelo menos uma das suas quatro cláusulas será falsa. No entanto, é possível atribuir valores de tal maneira a tornar três dos quatro cláusulas verdadeiras; na verdade, cada atribuição verdade vai fazer isso. Portanto , se esta fórmula é dada como um exemplo do problema MAX-SAT, a solução para o problema é o número três.

Difícil editar

O problema MAX-SAT é NP-difícil, desde a sua solução leva facilmente à solução do Problema de satisfatibilidade booliana, que é NP-completo. Também é difícil encontrar uma solução aproximada do problema, que satisfaça uma série de cláusulas dentro de um grau de aproximação que garante a solução ideal. Mais precisamente , o problema é APX-completo, e não admite Assim, o esquema de aproximação em tempo polinomial, a menos que P = NP.[1][2][3]

Resolvedores editar

Muitos resolvedores exatos para MAX-SAT foram desenvolvidos durante os últimos anos, e muitos deles foram apresentados na conferência sobre o problema da satisfatibilidade booleana e problemas relacionados, a SAT Conferência. Em 2006, a SAT Conferência acolheu a primeira avaliação de desempenho de MAX-SAT, comparando os solucionadores práticos para MAX-SAT, como tem feito no passado para o problema satisfatibilidade pseudo-booleana e o problema da fórmula booleana quantificada. Devido à sua natureza NP-Difícil, casos MAX-SAT de grande porte não podem ser resolvido precisamente, e deve-se recorrer a grau de aproximação e heurísticas [4]

Existem vários resolvedores submetidos às últimas avaliações de MAX-SAT:

  • Baseado em Branch and bound: Clone, MaxSatz (based on Satz), IncMaxSatz, IUT_MaxSatz, WBO, GIDSHSat.
  • Baseado em Satisfatibilidade: SAT4J, QMaxSat.
  • Baseado em Insatisfatibilidade: msuncore, WPM1, PM2.

Casos especiais editar

MAX-SAT é uma das extensões de optimização do Problema de satisfatibilidade booliana, o qual é o problema de determinar se as variáveis ​​de uma dada fórmula booleana podem ser atribuídas de modo a tornar a fórmula de avaliar para CERTO. Se as cláusulas são restritas a ter no máximo 2 literais , como em 2-satisfatibilidade, temos o problema MAX-2SAT. Se eles são restritas a no máximo 3 literais por cláusula , como em 3-satisfatibilidade, temos o problema MAX-3SAT.

Problemas relacionados editar

Existem várias extensões para MAX-SAT:

  • O problema satisfatibilidade máxima ponderada (Weighted MAX-SAT ou MAX-SAT ponderado) pede o peso máximo que pode ser satisfeito por qualquer atribuição, dado um conjunto de cláusulas ponderadas.
  • O problema satisfatibilidade máxima parcial (PMAX-SAT) pede o número máximo de cláusulas que podem ser satisfeitas por qualquer atribuição de um determinado subconjunto de cláusulas. O resto das cláusulas devem ser satisfeitas.
  • O problema satisfatibilidade suave (soft-SAT), dado um conjunto de problemas SAT, pede o número máximo de conjuntos que pode ser satisfeita por qualquer atribuição.[5]
  • O problema mínimo satisfatibilidade .
  • O problema MAX- SAT pode ser estendido para o caso em que as variáveis ​​do problema de Satisfação de restrições pertencem o conjunto de reais. O problema equivale a encontrar o menor q de tal modo que a intersecção q-interseção relaxada não está vazia. [6]

Ver também editar

Referências

  1. ↑ Mark Krentel. The Complexity of Optimization Problems. Proc. of STOC '86. 1986.
  2. ↑ Christos Papadimitriou. Computational Complexity. Addison-Wesley, 1994.
  3. ↑ Cohen, Cooper, Jeavons. A complete characterization of complexity for boolean constraint optimization problems. CP 2004.
  4. ↑ R. Battiti and M. Protasi. Approximate Algorithms and Heuristics for MAX-SAT Handbook of Combinatorial Optimization, Vol 1, 1998, 77-148, Kluwer Academic Publishers.
  5. ↑ Josep Argelich and Felip Manyà. Exact Max-SAT solvers for over-constrained problems. In Journal of Heuristics 12(4) pp. 375-392. Springer, 2006.
  6. ↑ Jaulin, L.; Walter, E. (2002). «Guaranteed robust nonlinear minimax estimation» (PDF). IEEE Transaction on Automatic Control. 47 

Ligações externas editar

Obtida de "https://pt.wikipedia.org/w/index.php?title=Problema_de_satisfatibilidade_máxima&oldid=67141313"