Problema de satisfatibilidade booliana

Na teoria da complexidade computacional, o problema de satisfazibilidade 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.

Consiste em determinar se existe alguma combinação das entradas de uma fórmula booliana tal que esta fórmula em questão seja avaliada VERDADEIRA.

Por exemplo, considere as variáveis boolianas $x_{1},x_{2},x_{3}$ e a expressão $(x_{1}\lor \neg x_{3})\land (\neg x_{2}\lor x_{3})$. Caso exista algum conjunto de valores para $x_{1},x_{2},x_{3}$ que torne a expressão VERDADEIRA, então esta fórmula é considerada satisfazível. Por outro lado, caso a fórmula seja FALSA para todas as combinações possíveis de $x_{1},x_{2},x_{3}$, então ela é considerada insatisfazível.

Para salientar a natureza binária deste problema, ele é referenciado frequentemente como o problema de satisfazibilidade 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 satisfazibilidade booliana (SAT) é um problema de decisão, cuja instância é 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 combinaçã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 satisfazível 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 satisfazíveis proposicionais é NP-completa. O Problema de Satisfazibilidade Proposicional (SAT), que decide se uma dada fórmula proposicional é satisfazí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 as Leis de De Morgan, é possível 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 é satisfazí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-satisfazibilidade.

Por outro lado, se nós restringirmos cada cláusula a 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, satisfazibilidade de Horn, é um problema P-completo.

O teorema de Cook prova que o problema de satisfazibilidade 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 satisfazibilidade.

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-completo

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 grafo tem 17 3-colorações válidas, a fórmula produzida para o SAT pela redução de Cook terá 17 combinações de entradas que a satisfazem.

2-satisfazibilidade

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 satisfazível se e somente se pelo menos um de seus termos for satisfazível, e um termo é satisfazí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-satisfazibilidade). 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-satisfazibilidade 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 satisfazibilidade de Horn em tempo polinomial, e é, na realidade, P-completo. Pode-se vê-lo como a versão P do problema de satisfazibilidade booliana.

Supondo 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 de que P e NP não são iguais continua em aberto.

3-satisfazibilidade

O 3-satisfazibilidade é um caso especial de $k$-satisfazibilidade ($k$-SAT), ou simplesmente satisfazibilidade (SAT), no que cada cláusula contém 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 satisfazibilidade 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 satisfazibilidade 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 satisfazibilidade 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 satisfazibilidade 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 satisfazibilidade proposicional tem várias generalizações, incluindo a satisfazibilidade 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 satisfazibilidade 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 codificados em termos de SAT.

Ver também

• Problema de roteamento de veículos
• Problema do caixeiro viajante
• Algoritmo de Davis-Putnam
• Algoritmo DPLL
• Algoritmo Chaff
• NP-completo
• NP (complexidade)
• SAT
• Forma normal conjuntiva
• Cláusula de Horn
• Função booliana (lógica)
• Domínio booliano
• SAT (desambiguação)

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  !CS1 manut: Nomes múltiplos: lista de autores (link)