Problema de satisfatibilidade booliana

Na teoria da complexidade computacional, o problema de satisfatibilidade booliana (do inglês boolean satisfiability problem, muitas vezes abreviado como SATISFIABILITY ou SAT) foi o primeiro problema identificado como pertencente à classe de complexidade NP-completo. O problema de satisfatibilidade booliana é o problema de determinar se existe uma determinada valoração para as variáveis de uma determinada fórmula booliana tal que esta valoração satisfaça esta fórmula em questão. Por exemplo, tomando $x_{1},x_{2},x_{3},x_{4}$ como as variáveis boolianas e a expressão $(x_{1}\lor \neg x_{3}\lor x_{4})\land (\neg x_{2}\lor x_{3}\lor \neg x_{4}),$ caso exista uma atribuição de valores de verdade para as variáveis da fórmula que torne a fórmula avaliada VERDADEIRA, esta fórmula é considera satisfatível, em contrapartida se nenhuma atribuição levou a uma avaliação da fórmula como verdadeira, ela é considerada insatisfatível. Para salientar a natureza binária deste problema, ele é referenciado freqüentemente como o problema de satisfatibilidade booliana ou proposicional. A sigla SAT também é geralmente utilizada para denotá-lo, com o entendimento implícito de que a função e suas variáveis recebem valores binários.

Definições básicas, terminologia e aplicações

O problema de satisfatibilidade booliana (SAT) é um problema de decisão, cuja instancia é uma expressão booliana escrita somente com operadores AND, OR, NOT, variáveis, e parênteses. A questão é: dada uma expressão, será que há alguma atribuição de valores VERDADEIROS e FALSOS para as variáveis que torne a expressão inteira verdadeira? Uma fórmula da lógica proposicional é dita satisfatível- ou seja, avaliada como VERDADEIRA - se for possível atribuir valores lógicos a suas variáveis de tal maneira que eles tornem a fórmula verdadeira. A classe de fórmulas satisfatíveis proposicionais é NP-completa. O Problema de satisfatibilidade Proposicional (SAT), que decide se uma dada fórmula proposicional é satisfatível, é de fundamental importância em várias áreas da ciência da computação, incluindo a Teoria da Computação, algoritmos, inteligência artificial, projeto de hardware e verificação.

O problema pode ser significativamente restringido e ainda se manter NP-completo. Aplicando leis de De Morgan, nós podemos supor que operadores NOT, são aplicados diretamente somente sobre variáveis, jamais sobre expressões complexas; nos referimos a variáveis ou suas negações como literais. Por exemplo, ambos $x_{1}$ e $\neg x_{2}$ são literais, o primeiro um literal positivo e o segundo um literal negativo. Se juntarmos um grupo de literais com o símbolo de disjunção (OR), nós formamos uma cláusula, como $(x_{1}\lor \neg x_{2}).$ As fórmulas portanto serão uma conjunção (AND) de cláusulas - esta é chamada forma normal conjuntiva (FNC). Determinar se uma fórmula nesta forma é satisfatível é ainda um problema NP-completo, onde se cada cláusula for limitada a no máximo três literais. Este último problema é chamado 3SAT, 3CNFSAT, ou 3-satisfatibilidade.

Por outro lado, se nós restringirmos cada cláusula à no máximo dois literais, o problema resultante, 2SAT, é um problema Polinomial. Alternativamente, se cada cláusula for uma cláusula de Horn, contendo no máximo um literal positivo, o problema resultante, satisfatibilidade de Horn, é um problema P-completo.

O teorema de Cook prova que o problema de satisfatibilidade booliano é NP-completo, e de fato, este foi o primeiro problema de decisão a ser provado NP-completo. Entretanto, além deste teorema, algoritmos eficientes e resistentes a mudança de escala para SAT foram desenvolvidos desde a última década e contribuíram aos avanços poderosos em nossa habilidade de resolver automaticamente este problema de satisfatibilidade.

SAT também pode ser usado para verificar a equivalência de dois circuitos combinatórios, similar à geração de teste onde dois circuitos alvo são combinados. O resolvedor de SAT procura o caso em que as saídas dos dois circuitos são diferentes.

Complexidade e versões restritas

NP-completude

O problema SAT foi o primeiro problema NP-completo conhecido, como demonstrado por Stephen Cook em 1971 (teorema de Cook). Até essa época, o conceito de um problema NP-completo nem existia. O problema SAT continua NP-completo mesmo se todas as fórmulas estiverem na forma normal conjuntiva com 3 variáveis por cláusula (3-FNC), gerando o problema 3SAT. Isto quer dizer que a expressão tem a forma:

$(x_{11}\lor x_{12}\lor x_{13})\land$

$(x_{21}\lor x_{22}\lor x_{23})\land$

$(x_{31}\lor x_{32}\lor x_{33})\land \ldots$

onde cada $x$ é uma variável ou uma negação de uma variável literal, e cada variável pode aparecer mais de uma vez em cada fórmula.

Uma propriedade útil da redução de Cook é que ela preserva o número de respostas aceitas. Por exemplo, se um gráfo tem 17 3-colorações válidas, a fórmula produzida para o SAT pela redução de Cook terá 17 valorações satisfatíveis.

2-satisfatibilidade

O problema SAT é mais fácil de resolver se as fórmulas forem restringidas àquelas na forma normal disjuntiva, isto é, se elas forem disjunção ( $\lor$ ) de termos, onde cada termo é uma conjunção ( $\land$ ) de literais. Tal fórmula é de fato satisfatível se e somente se pelo menos um de seus termos for satisfatível, e um termo é satisfatível se e somente se não contiver $x$ e $\neg x$ para alguma variável $x.$ Isto pode ser verificado em um tempo polinomial.

SAT também é mais fácil se o número de literais em uma cláusula for limitado a 2, em cujo caso o problema será chamado 2SAT (2-satisfatibilidade). Este problema pode também ser resolvido em tempo polinomial, e de fato é completo para a classe NL. Similarmente, se limitarmos o número de literais por cláusula a 2 e trocarmos as AND-operações por operações de XOR, o resultado é 2-satisfatibilidade com OU-exclusivo, um problema completo para SL = L (Symmetric Logspace ou Sym-L). Uma das restrições mais importantes do SAT é HORNSAT, onde a fórmula é uma conjunção de cláusulas de Horn. Este problema é resolvido pelo algoritmo de satisfatibilidade de Horn em tempo polinomial, e é, na realidade, P-completo. Pode-se vê-lo como a versão P do problema de satisfatibilidade booliana.

Desde que as classes de complexidade P e NP não sejam iguais, nenhumas destas restrições é NP-completa, ao contrário do que acontece com SAT. A hipótese que P e NP não são iguais continua em aberto.

3-satisfatibilidade

O 3-satisfatibilidade é um caso especial de $k$ -satisfatibilidade ( $k$ -SAT), ou simplesmente satisfatibilidade (SAT), no que cada cláusula contem exatamente $k$ = 3 literais. Era um dos 21 problemas NP-completos de Karp.

Eis um exemplo:

$E=(x_{1}\lor \neg x_{2}\lor \neg x_{3})\land (x_{1}\lor x_{2}\lor x_{4})$

E tem duas cláusulas (denotadas por parênteses), quatro literais $(x_{1},x_{2},x_{3},x_{4}),$ e $k=3$ (três literais por cláusula).

Para resolver esta instância do problema de decisão devemos determinar se há um valor de verdade (VERDADEIRO ou FALSO) que podemos atribuir a cada um dos literais de $x_{1}$ a $x_{4}$ de modo que a expressão inteira seja VERDADEIRA. Nesta instância, existe uma tal atribuição ( $x_{1}$ = VERDADEIRO, $x_{2}$ = VERDADEIRO, $x_{3}$ =VERDADEIRO, $x_{4}$ =VERDADEIRO), assim a resposta a esta instância é SIM. Esta é uma entre muitas atribuições possíveis. Com efeito, qualquer atribuição que faça $x_{1}$ = VERDADEIRO é suficiente para tornar a expressão inteira VERDADEIRA. Se não houvesse nenhuma atribuição com esta propriedade, a resposta seria NÃO.

Uma vez que $k$ -SAT (o caso geral) se reduz a 3-SAT, e 3-SAT pode ser demonstrado que é NP-completo, logo podemos usar isto para demonstrar que outros problemas também são NP-completos. Isto é feito mostrando como uma solução para outro problema poderia ser usado para resolver 3-SAT. Um exemplo do problema onde este método tem sido usado é Clique. Geralmente é mais fácil usar reduções de 3-SAT do que SAT para problemas onde pesquisadores estão tentando provar a NP-completude.

O 3-SAT pode ser mais restringido ao 3SAT Um-em-três , onde nós perguntamos se exatamente uma das variáveis em cada cláusula é verdadeira, ao invés de ao menos uma. 3SAT Um-em-três ainda é NP-completo.

Extensões do SAT

Uma extensão que ganhou popularidade significativa desde 2003 é o problema de satisfatibilidade módulo teorias, que permite enriquecer as fórmulas na FNC com restrições lineares, vetores, restrições de que todas as variáveis são distintas, funções não interpretadas, etc. Tais extensões são tipicamente NP-completas, mas já estão disponíveis resolvedores bastante eficientes que são capazes de lidar com muitos tipos de restrições desse gênero.

O problema de satisfatibilidade parece tornar-se mais difícil (PSPACE-completo) se nós permitirmos quantificadores tais como o “para todo” e o “existencial” que ligam as variáveis boolianas. Um exemplo de tal expressão seria:

$\forall x\exists y\exists z((x\lor y\lor z)\land (\lnot x\lor \lnot y\lor \lnot z))$

Se usarmos somente quantificadores $\exists ,$ este é ainda o problema SAT. Se nós permitirmos somente quantificadores $\forall ,$ ele se transforma no problema de tautologia Co-NP-completo. Se permitirmos ambos, o problema é chamado de problema da fórmula booliana quantificada (QBF), que pode ser mostrado PSPACE-completo. Acredita-se amplamente que os problemas PSPACE-completos sejam estritamente mais difíceis do que qualquer problema em NP, embora isto ainda não tenha sido demonstrado. .

O problema de satisfatibilidade máxima, uma generalização em FNP do SAT, pergunta pelo número máximo de cláusulas que podem ser satisfeitas por uma atribuição qualquer. Este problema tem algoritmos de aproximação eficientes, mas é NP-difícil de se resolver de forma exata. Pior ainda, o problema é APX-completo, o que significa que não há nenhum esquema de aproximação em tempo polinomial para este problema a menos que P=NP.

Algoritmos para resolver o SAT

Há classes de algoritmos de alto desempenho para resolver instâncias de SAT na prática: variantes modernas do Algoritmo DPLL, tais como o Algoritmo Chaff,e algoritmos estocásticos de busca local, tais como WalkSAT.

Um resolvedor SAT do tipo DPLL emprega um procedimento sistemático de busca por backtracking para explorar o espaço (de tamanho exponencial) das atribuições das variáveis procurando atribuições que satisfaçam as fórmulas em questão. O procedimento básico da busca foi proposto em dois artigos inovadores no início dos anos 60 e é, hoje em dia, geralmente designado como o algoritmo de Davis-Putnam-Logemann-Loveland (DPLL). Os resolvedores modernos de SAT (desenvolvidos nos últimos dez anos) aperfeiçoam o algoritmo de busca básico do tipo DPLL com análise eficiente de conflito, aprendizagem de cláusula, backtracking não-cronológico (também conhecido como backjumping), assim como a propagação da unidade dos “dois literais vigiados”(Two Watched Literals), ramificação adaptável, e reinícios aleatórios. Verifica-se empiricamente que tais “acréscimos” à busca sistemática básica são essenciais para resolver as instâncias longas do problema SAT que se levantam em Automação de design eletrônico. Os resolvedores SAT modernos estão causando também um impacto significativo nos campos da verificação de software, da resolução de restrições na inteligência artificial, e da pesquisa operacional, entre outros. Há resolvedores poderosos disponíveis em domínio público, e eles são muito fáceis de usar. Em particular, o MiniSAT, que ganhou a competição de SAT de 2005, tem apenas cerca de 600 linhas de código.

Algoritmos Genéticos e outros métodos de busca local estocástica de uso geral estão sendo usados também para resolver problemas SAT, especialmente quando não há ou há apenas um conhecimento limitado da estrutura específica das instâncias do problema a serem resolvidas. Determinados tipos de instâncias longas aleatórias satisfatíveis de SAT podem ser resolvidas pela propagação dos literais vigiados. Em particular no design e na verificação de hardware, a satisfatibilidade e outras propriedades lógicas de uma fórmula proposicional dada são às vezes decididas baseadas em uma representação da fórmula como um diagrama de decisão binária(BDD).

A satisfatibilidade proposicional tem várias generalizações, incluindo a satisfatibilidade para o problema da fórmula booliana quantificada, para a lógica clássica de primeira e de segunda ordem(LCPO e LCSO, respectivamente), para problemas de satisfação de restrições, para a programação de inteiros 0-1, e para o problema de satisfatibilidade máxima.

Muitos outros problemas de decisão, tais como os problemas de coloração de grafos, problemas de planejamento, e problemas de agendamento, podem ser facilmente codificados em termos de SAT.

Ver também

Referências

Analise de Algoritmos SAT para Resolução de Problemas Multivalorados - Jacques Fux
SILVA, F. C. ; FINGER, M. ; MELO, A. C. V. (2006). Lógica para Computação]. São Paulo: Thomson Learning. ISBN 8522105170. Consultado em 30 de junho de 2007. Arquivado do original em 30 de setembro de 2007

Este artigo sobre matemática é um esboço. Você pode ajudar a Wikipédia expandindo-o.