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

A formula para a forma normal conjuntiva

(x_{0}\lor x_{1})\land (x_{0}\lor \lnot x_{1})\land (\lnot x_{0}\lor x_{1})\land (\lnot x_{0}\lor \lnot x_{1})

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

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

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

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

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

Referências

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

Ligações externas

http://www.satisfiability.org/ Em falta ou vazio |título= (ajuda)
https://web.archive.org/web/20060324162911/http://www.iiia.csic.es/~maxsat06/ Em falta ou vazio |título= (ajuda)
http://www.maxsat.udl.cat Em falta ou vazio |título= (ajuda)
Weighted Max-2-SAT Benchmarks with Hidden Optimum Solutions
Lecture Notes on MAX-SAT Approximation

[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

[1]

[2]

[3]

[4]

[5]

[6]