# 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.

## 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
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.
* 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.