Problema de satisfatibilidade máxima 📖 Wikipedia

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.

A formula para a forma normal conjuntiva

${\displaystyle (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.

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]

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.

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.

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]

• Problema de satisfatibilidade booliana
• Satisfação de restrições

• 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