Problema de satisfatibilidade booleana - Boolean satisfiability problem

Em lógica e ciência da computação , o problema de satisfatibilidade booleana (às vezes chamado de problema de satisfatibilidade proposicional e abreviado de SATISFIABILIDADE , SAT ou B-SAT ) é o problema de determinar se existe uma interpretação que satisfaça uma dada fórmula booleana . Em outras palavras, ele pergunta se as variáveis ​​de uma dada fórmula booleana podem ser consistentemente substituídas pelos valores VERDADEIRO ou FALSO, de forma que a fórmula seja avaliada como VERDADEIRA . Se for esse o caso, a fórmula é chamada de satisfazível . Por outro lado, se essa atribuição não existir, a função expressa pela fórmula será FALSE para todas as atribuições de variáveis ​​possíveis e a fórmula será insatisfatória . Por exemplo, a fórmula " a AND NOT b " é satisfatória porque podemos encontrar os valores a  = TRUE eb  = FALSE, que tornam ( a AND NOT b ) = TRUE. Em contraste, " a E NÃO a " é insatisfatório.

SAT é o primeiro problema que se provou ser NP-completo ; veja o teorema de Cook-Levin . Isso significa que todos os problemas na classe de complexidade NP , que inclui uma ampla gama de problemas naturais de decisão e otimização, são no máximo tão difíceis de resolver quanto SAT. Não há algoritmo conhecido que resolva de forma eficiente cada problema SAT, e geralmente acredita-se que tal algoritmo não existe; ainda assim, essa crença não foi provada matematicamente, e resolver a questão de se SAT tem um algoritmo de tempo polinomial é equivalente ao problema P versus NP , que é um famoso problema aberto na teoria da computação.

No entanto, a partir de 2007, algoritmos SAT heurísticos são capazes de resolver instâncias de problemas envolvendo dezenas de milhares de variáveis ​​e fórmulas consistindo de milhões de símbolos, o que é suficiente para muitos problemas SAT práticos de, por exemplo, inteligência artificial , design de circuito e automação prova de teorema .

Definições básicas e terminologia

Uma fórmula lógica proposicional , também chamada de expressão booleana , é construída a partir de variáveis , operadores AND ( conjunção , também denotada por ∧), OR ( disjunção , ∨), NOT ( negação , ¬) e parênteses. Uma fórmula é considerada satisfatória se puder se tornar VERDADEIRA atribuindo valores lógicos apropriados (isto é, VERDADEIRO, FALSO) às suas variáveis. O problema de satisfatibilidade booleana (SAT) é, dada uma fórmula, para verificar se é satisfazível. Este problema de decisão é de importância central em muitas áreas da ciência da computação , incluindo ciência da computação teórica , teoria da complexidade , algoritmo , criptografia e inteligência artificial .

Existem vários casos especiais do problema de satisfatibilidade booleana em que as fórmulas devem ter uma estrutura particular. Um literal é uma variável, chamada literal positivo , ou a negação de uma variável, chamada literal negativo . Uma cláusula é uma disjunção de literais (ou um único literal). Uma cláusula é chamada de cláusula de Horn se contiver no máximo um literal positivo. Uma fórmula está na forma normal conjuntiva (CNF) se for uma conjunção de cláusulas (ou uma única cláusula). Por exemplo, x ₁ é um literal positivo, ¬ x ₂ é um literal negativo, x ₁ ∨ ¬ x ₂ é uma cláusula. A fórmula ( x ₁ ∨ ¬ x ₂ ) ∧ (¬ x ₁ ∨ x ₂ ∨ x ₃ ) ∧ ¬ x ₁ está na forma normal conjuntiva; sua primeira e terceira cláusulas são cláusulas de Horn, mas sua segunda cláusula não é. A fórmula é satisfatória, escolhendo x ₁  = FALSO, x ₂  = FALSO e x ₃ arbitrariamente, uma vez que (FALSO ∨ ¬FALSO) ∧ (¬FALSO ∨ FALSO ∨ x ₃ ) ∧ ¬FALSO é avaliado como (FALSO ∨ VERDADEIRO) ∧ (VERDADEIRO ∨ FALSO ∨ x ₃ ) ∧ VERDADEIRO, e por sua vez para VERDADEIRO ∧ VERDADEIRO ∧ VERDADEIRO (ou seja, para VERDADEIRO). Em contraste, a fórmula CNF a ∧ ¬ a , consistindo em duas cláusulas de um literal, é insatisfatória, uma vez que para a = VERDADEIRO ou a = FALSO ela avalia como VERDADEIRO ∧ ¬ VERDADEIRO (ou seja, FALSO) ou FALSO ∧ ¬FALSO (ou seja , novamente FALSE), respectivamente.

Para algumas versões do problema SAT, é útil definir a noção de uma fórmula de forma normal conjuntiva generalizada , viz. como uma conjunção de muitas cláusulas generalizadas arbitrariamente , sendo a última da forma R ( l ₁ , ..., l _n ) para alguma função booleana R e literais (ordinários) l _i . Diferentes conjuntos de funções booleanas permitidas levam a diferentes versões de problemas. Por exemplo, R (¬ x , a , b ) é uma cláusula generalizada, e R (¬ x , a , b ) ∧ R ( b , y , c ) ∧ R ( c , d , ¬ z ) é uma cláusula generalizada forma normal conjuntiva. Esta fórmula é usada abaixo , com R sendo o operador ternário que é TRUE apenas quando exatamente um de seus argumentos o é.

Usando as leis da álgebra booleana , toda fórmula lógica proposicional pode ser transformada em uma forma normal conjuntiva equivalente, que pode, entretanto, ser exponencialmente mais longa. Por exemplo, transformar a fórmula ( x ₁ ∧ y ₁ ) ∨ ( x ₂ ∧ y ₂ ) ∨ ... ∨ ( x _n ∧ y _n ) na forma normal conjuntiva resulta

( x ₁  ∨  x ₂  ∨ ... ∨  x _n ) ∧

( y ₁  ∨  x ₂  ∨ ... ∨  x _n ) ∧

( x ₁  ∨  y ₂  ∨ ... ∨  x _n ) ∧

( y ₁  ∨  y ₂  ∨ ... ∨  x _n ) ∧ ... ∧

( x ₁  ∨  x ₂  ∨ ... ∨  y _n ) ∧

( y ₁  ∨  x ₂  ∨… ∨  y _n ) ∧

( x ₁  ∨  y ₂  ∨ ... ∨  y _n ) ∧

( y ₁  ∨  y ₂  ∨… ∨  y _n ) ;

enquanto o primeiro é uma disjunção de n conjunções de 2 variáveis, o último consiste em 2 ⁿ cláusulas de n variáveis.

Complexidade e versões restritas

Satisfatibilidade irrestrita (SAT)

SAT foi o primeiro problema NP-completo conhecido , como provado por Stephen Cook na Universidade de Toronto em 1971 e independentemente por Leonid Levin na National Academy of Sciences em 1973. Até então, o conceito de um problema NP-completo não mesmo existir. A prova mostra como cada problema de decisão na classe de complexidade NP pode ser reduzido ao problema SAT para fórmulas CNF, às vezes chamado de CNFSAT . Uma propriedade útil da redução de Cook é que ela preserva o número de respostas aceitáveis. Por exemplo, decidir se um dado grafo tem uma coloração tripla é outro problema em NP; se um gráfico tiver 17 3 cores válidas, a fórmula SAT produzida pela redução de Cook-Levin terá 17 atribuições satisfatórias.

NP-completude refere-se apenas ao tempo de execução das instâncias de pior caso. Muitos dos casos que ocorrem em aplicações práticas podem ser resolvidos muito mais rapidamente. Consulte Algoritmos para resolver o SAT abaixo.

SAT é trivial se as fórmulas se restringem àquelas na forma normal disjuntiva , ou seja, são uma disjunção de conjunções de literais. Tal fórmula é de fato satisfatória se e somente se pelo menos uma de suas conjunções é satisfatória, e uma conjunção é satisfatória se e somente se ela não contém xe NÃO x para alguma variável x . Isso pode ser verificado em tempo linear. Além disso, se eles estão restritos a estar na forma normal disjuntiva completa , na qual cada variável aparece exatamente uma vez em cada conjunção, eles podem ser verificados em tempo constante (cada conjunção representa uma atribuição satisfatória). Mas pode levar tempo e espaço exponencial para converter um problema SAT geral para a forma normal disjuntiva; para um exemplo de troca "∧" e "∨" na acima exemplo blow-up exponencial de forma normal conjuntiva.

3-satisfatibilidade

A instância 3-SAT ( x ∨ x ∨ y ) ∧ (¬ x ∨ ¬ y ∨ ¬ y ) ∧ (¬ x ∨ y ∨ y ) reduzida a um problema de clique . Os vértices verdes formam um 3-clique e correspondem à atribuição satisfatória x = FALSE, y = TRUE.

Como o problema de satisfatibilidade para fórmulas arbitrárias, determinar a satisfatibilidade de uma fórmula na forma normal conjuntiva onde cada cláusula é limitada a no máximo três literais é NP-completo também; esse problema é denominado 3-SAT , 3CNFSAT ou 3-satisfatibilidade . Para reduzir o problema SAT irrestrito para 3-SAT, transforme cada cláusula l ₁ ∨ ⋯ ∨ l _n em uma conjunção de n - 2 cláusulas

( l ₁ ∨ l ₂ ∨ x ₂ ) ∧

(¬ x ₂ ∨ l ₃ ∨ x ₃ ) ∧

(¬ x ₃ ∨ l ₄ ∨ x ₄ ) ∧ ⋯ ∧

(¬ x _{n - 3} ∨ l _{n - 2} ∨ x _{n - 2} ) ∧

(¬ x _{n - 2} ∨ l _{n - 1} ∨ l _n )

onde x ₂ , ⋯,  x _{n - 2} são variáveis ​​novas que não ocorrem em outro lugar. Embora as duas fórmulas não sejam logicamente equivalentes , elas são equitativas . A fórmula resultante da transformação de todas as cláusulas é no máximo 3 vezes mais longa que a original, ou seja, o crescimento do comprimento é polinomial.

3-SAT é um dos 21 problemas NP-completos de Karp e é usado como ponto de partida para provar que outros problemas também são NP-difíceis . Isso é feito por redução em tempo polinomial de 3-SAT para o outro problema. Um exemplo de problema em que esse método foi usado é o problema do clique : dada uma fórmula CNF consistindo de cláusulas c , o grafo correspondente consiste em um vértice para cada literal e uma aresta entre cada dois literais não contraditórios de cláusulas diferentes, cf. foto. O gráfico tem um c -clique se e somente se a fórmula for satisfatória.

Existe um algoritmo aleatório simples devido a Schöning (1999) que roda no tempo (4/3) ⁿ onde n é o número de variáveis ​​na proposição 3-SAT, e consegue com alta probabilidade decidir corretamente o 3-SAT.

A hipótese de tempo exponencial afirma que nenhum algoritmo pode resolver 3-SAT (ou mesmo k -SAT para qualquer ) em exp ( o ( n )) tempo (ou seja, fundamentalmente mais rápido do que exponencial em n ). ${\ displaystyle k> 2}$

Selman, Mitchell e Levesque (1996) fornecem dados empíricos sobre a dificuldade de fórmulas 3-SAT geradas aleatoriamente, dependendo de seus parâmetros de tamanho. A dificuldade é medida em número de chamadas recursivas feitas por um algoritmo DPLL .

3-satisfatibilidade pode ser generalizada para k-satisfatibilidade ( k-SAT , também k-CNF-SAT ), quando as fórmulas em CNF são consideradas com cada cláusula contendo até k literais. No entanto, como para qualquer k ≥ 3, esse problema não pode ser nem mais fácil do que 3-SAT nem mais difícil do que SAT, e os dois últimos são NP-completos, então devem ser k-SAT.

Alguns autores restringem k-SAT a fórmulas CNF com exatamente k literais . Isso também não leva a uma classe de complexidade diferente, pois cada cláusula l ₁ ∨ ⋯ ∨ l _j com j < k literais pode ser preenchida com variáveis ​​fictícias fixas para l ₁ ∨ ⋯ ∨ l _j ∨ d _{j +1} ∨ ⋯ ∨ d _k . Depois de preencher todas as cláusulas, 2 ^k -1 cláusulas extras devem ser anexadas para garantir que apenas d ₁ = ⋯ = d _k = FALSE possa levar a uma atribuição satisfatória. Como k não depende do comprimento da fórmula, as cláusulas extras levam a um aumento constante no comprimento. Pelo mesmo motivo, não importa se literais duplicados são permitidos nas cláusulas, como em ¬ x ∨ ¬ y ∨ ¬ y .

Exatamente-1 3-satisfatibilidade

Esquerda: redução de Schaefer de uma cláusula 3-SAT x ∨ y ∨ z . O resultado de R é VERDADEIRO (1) se exatamente um de seus argumentos for VERDADEIRO e FALSO (0) caso contrário. Todas as 8 combinações de valores para x , y , z são examinadas, uma por linha. As novas variáveis a , ..., f podem ser escolhidas para satisfazer todas as cláusulas (exatamente um argumento verde para cada R ) em todas as linhas, exceto a primeira, onde x ∨ y ∨ z é FALSE. À direita: uma redução mais simples com as mesmas propriedades.

Uma variante do problema de 3-satisfatibilidade é o 3-SAT um em três (também conhecido como 1 em 3 SAT e exatamente 1 3-SAT ). Dada uma forma normal conjuntiva com três literais por cláusula, o problema é determinar se existe uma atribuição de verdade para as variáveis ​​de modo que cada cláusula tenha exatamente um literal VERDADEIRO (e, portanto, exatamente dois literais FALSO). Em contraste, o 3-SAT comum requer que cada cláusula tenha pelo menos um literal VERDADEIRO. Formalmente, um problema um em três 3-SAT é dado como uma forma normal conjuntiva generalizada com todas as cláusulas generalizadas usando um operador ternário R que é VERDADEIRO apenas se exatamente um de seus argumentos o for. Quando todos os literais de uma fórmula um-em-três 3-SAT são positivos, o problema de satisfatibilidade é chamado de um-em-três 3-SAT positivo .

Um em três 3-SAT, junto com seu caso positivo, é listado como problema NP-completo "OA4" na referência padrão, Computadores e Intratabilidade: Um Guia para a Teoria de NP-Completude por Michael R. Garey e David S. Johnson . Um em três 3-SAT foi provado ser NP-completo por Thomas Jerome Schaefer como um caso especial do teorema da dicotomia de Schaefer , que afirma que qualquer problema generalizando a satisfatibilidade booleana de uma certa maneira está na classe P ou é NP- completo.

Schaefer oferece uma construção que permite uma redução fácil de tempo polinomial de 3-SAT para um em três 3-SAT. Seja "( x ou y ou z )" uma cláusula em uma fórmula 3CNF. Adicione seis novas variáveis ​​booleanas a , b , c , d , e e f , para serem usadas para simular esta cláusula e nenhuma outra. Então a fórmula R ( x , a , d ) ∧ R ( y , b , d ) ∧ R ( a , b , e ) ∧ R ( c , d , f ) ∧ R ( z , c , FALSO) é satisfatória por alguma configuração das variáveis ​​frescas se e somente se pelo menos um de x , y ou z for TRUE, veja a figura (à esquerda). Assim, qualquer instância de 3-SAT com cláusulas m e variáveis n pode ser convertida em uma instância de 3-SAT um-em-três equisatisfatória com cláusulas de 5 m e variáveis n +6 m . Outra redução envolve apenas quatro variáveis ​​novas e três cláusulas: R (¬ x , a , b ) ∧ R ( b , y , c ) ∧ R ( c , d , ¬ z ), veja a figura (direita).

Satisfabilidade não totalmente igual a 3

Outra variante é o problema de satisfatibilidade não totalmente igual a 3 (também chamado de NAE3SAT ). Dada uma forma normal conjuntiva com três literais por cláusula, o problema é determinar se uma atribuição às variáveis ​​existe de forma que em nenhuma cláusula todos os três literais tenham o mesmo valor verdade. Esse problema também é NP-completo, mesmo que nenhum símbolo de negação seja admitido, pelo teorema da dicotomia de Schaefer.

SAT linear

Uma fórmula 3-SAT é Linear SAT ( LSAT ) se cada cláusula (vista como um conjunto de literais) cruza no máximo uma outra cláusula e, além disso, se duas cláusulas se cruzam, então elas têm exatamente um literal em comum. Uma fórmula LSAT pode ser descrita como um conjunto de intervalos semifechados separados em uma linha. Decidir se uma fórmula LSAT é satisfatória ou não é NP-completo.

2-satisfatibilidade

SAT é mais fácil se o número de literais em uma cláusula for limitado a no máximo 2, caso em que o problema é chamado de 2-SAT . Este problema pode ser resolvido em tempo polinomial, e de fato está completo para a classe de complexidade NL . Se, adicionalmente, todos ou operações em literais são alterados para XOR operações, o resultado é chamado exclusivo-ou 2-satisfatibilidade , que é uma completa problema para a classe de complexidade SL = L .

Satisfazibilidade de chifre

O problema de decidir a satisfatibilidade de uma dada conjunção de cláusulas de Horn é chamado de satisfatibilidade de Horn ou HORN-SAT . Ele pode ser resolvido em tempo polinomial por uma única etapa do algoritmo de propagação de Unidade , que produz o modelo mínimo único do conjunto de cláusulas de Horn (escrito o conjunto de literais atribuídos a TRUE). A satisfação do chifre é P-completa . Pode ser visto como a versão de P do problema de satisfatibilidade booleana. Além disso, decidir a verdade das fórmulas de Horn quantificadas pode ser feito em tempo polinomial.

As cláusulas de Horn são interessantes porque são capazes de expressar a implicação de uma variável a partir de um conjunto de outras variáveis. De fato, uma dessas cláusulas ¬ x ₁ ∨ ... ∨ ¬ x _n ∨ y pode ser reescrita como x ₁ ∧ ... ∧ x _n → y , ou seja, se x ₁ , ..., x _n são todos VERDADEIROS , então y também precisa ser TRUE.

Uma generalização da classe das fórmulas de Horn é aquela das fórmulas renomeadas de Horn, que é o conjunto de fórmulas que podem ser colocadas na forma de Horn substituindo algumas variáveis ​​por suas respectivas negações. Por exemplo, ( x ₁ ∨ ¬ x ₂ ) ∧ (¬ x ₁ ∨ x ₂ ∨ x ₃ ) ∧ ¬ x ₁ não é uma fórmula de Horn, mas pode ser renomeada para a fórmula de Horn ( x ₁ ∨ ¬ x ₂ ) ∧ (¬ x ₁ ∨ x ₂ ∨ ¬ y ₃ ) ∧ ¬ x ₁ introduzindo y ₃ como negação de x ₃ . Em contraste, nenhuma renomeação de ( x ₁ ∨ ¬ x ₂ ∨ ¬ x ₃ ) ∧ (¬ x ₁ ∨ x ₂ ∨ x ₃ ) ∧ ¬ x ₁ leva a uma fórmula de Horn. A verificação da existência de tal substituição pode ser feita em tempo linear; portanto, a satisfatibilidade de tais fórmulas está em P, pois pode ser resolvida realizando primeiro essa substituição e, em seguida, verificando a satisfatibilidade da fórmula de Horn resultante.

Uma fórmula com 2 cláusulas pode ser insatisfeita (vermelho), 3-satisfeito (verde), xor-3-satisfeito (azul) ou / e 1 em 3-satisfeito (amarelo), dependendo da contagem VERDADEIRA-literal em a primeira (hor) e a segunda (vert) cláusula.

Satisfazibilidade de XOR

Outro caso especial é a classe de problemas em que cada cláusula contém operadores OR XOR (ou seja, exclusivos ou ) em vez de operadores OR (simples). Isso está em P , uma vez que uma fórmula XOR-SAT também pode ser vista como um sistema de equações lineares mod 2, e pode ser resolvida em tempo cúbico por eliminação gaussiana ; veja a caixa para um exemplo. Esta reformulação é baseada no parentesco entre álgebras booleanas e anéis booleanos , e no fato de que o módulo aritmético dois forma um corpo finito . Uma vez que a XOR b XOR c avalia para TRUE se e somente se exatamente 1 ou 3 membros de { a , b , c } são TRUE, cada solução do problema 1-em-3-SAT para uma dada fórmula CNF também é uma solução do problema XOR-3-SAT e, por sua vez, cada solução de XOR-3-SAT é uma solução de 3-SAT, cf. foto. Como consequência, para cada fórmula CNF, é possível resolver o problema XOR-3-SAT definido pela fórmula, e com base no resultado inferir que o problema 3-SAT é solucionável ou que o 1-em-3- O problema do SAT não tem solução.

Desde que as classes de complexidade P e NP não sejam iguais , nem 2-, nem Horn-, nem XOR-satisfatibilidade é NP-completa, ao contrário de SAT.

Teorema da dicotomia de Schaefer

As restrições acima (CNF, 2CNF, 3CNF, Horn, XOR-SAT) limitam as fórmulas consideradas como conjunções de subfórmulas; cada restrição estabelece uma forma específica para todas as subfórmulas: por exemplo, apenas cláusulas binárias podem ser subfórmulas em 2CNF.

O teorema da dicotomia de Schaefer afirma que, para qualquer restrição às funções booleanas que podem ser usadas para formar essas subfórmulas, o problema de satisfatibilidade correspondente está em P ou NP-completo. A associação em P da satisfatibilidade das fórmulas 2CNF, Horn e XOR-SAT são casos especiais deste teorema.

A tabela a seguir resume algumas variantes comuns do SAT.

Extensões do SAT

Uma extensão que ganhou popularidade significativa desde 2003 são as teorias do módulo de satisfazibilidade ( SMT ) que podem enriquecer fórmulas CNF com restrições lineares, matrizes, restrições totalmente diferentes, funções não interpretadas , etc. Essas extensões geralmente permanecem NP-completas, mas os solucionadores muito eficientes são agora disponível que pode lidar com muitos desses tipos de restrições.

O problema de satisfatibilidade torna-se mais difícil se os quantificadores "para todos" ( ∀ ) e "existe" ( ∃ ) forem permitidos para ligar as variáveis ​​booleanas. Um exemplo de tal expressão seria ∀ x ∀ y ∃ z ( x ∨ y ∨ z ) ∧ (¬ x ∨ ¬ y ∨ ¬ z ) ; é válido, uma vez que para todos os valores de x e y , um valor apropriado de z podem ser encontrados, viz. z = TRUE se ambos x e y são FALSA, e z = FALSE outra. O próprio SAT (tacitamente) usa apenas ∃ quantificadores. Se apenas ∀ quantificadores forem permitidos, o chamado problema de tautologia é obtido, que é co-NP-completo . Se ambos os quantificadores forem permitidos, o problema é chamado de problema de fórmula booleana quantificada ( QBF ), que pode ser mostrado como PSPACE completo . É amplamente aceito que os problemas de PSPACE-completo são estritamente mais difíceis do que qualquer problema em NP, embora isso ainda não tenha sido provado. Usando sistemas P altamente paralelos , os problemas QBF-SAT podem ser resolvidos em tempo linear.

O SAT comum pergunta se há pelo menos uma atribuição de variável que torna a fórmula verdadeira. Uma variedade de variantes lidam com o número de tais atribuições:

• MAJ-SAT pergunta se a maioria de todas as atribuições tornam a fórmula VERDADEIRA. É conhecido por ser completo para PP , uma classe probabilística.
• #SAT , o problema de contar quantas atribuições de variáveis ​​satisfazem uma fórmula, é um problema de contagem, não um problema de decisão, e é # P-completo .
• UNIQUE SAT é o problema de determinar se uma fórmula tem exatamente uma atribuição. É completo para US , a classe de complexidade que descreve problemas solucionáveis ​​por uma máquina de Turing de tempo polinomial não determinística que aceita quando há exatamente um caminho de aceitação não determinístico e rejeita o contrário.
• UNAMBIGUOUS-SAT é o nome dado ao problema de satisfatibilidade quando a entrada é restrita a fórmulas com no máximo uma atribuição satisfatória. O problema também é chamado de USAT . Um algoritmo de solução para UNAMBIGUOUS-SAT pode exibir qualquer comportamento, incluindo looping sem fim, em uma fórmula com várias atribuições satisfatórias. Embora esse problema pareça mais fácil, Valiant e Vazirani mostraram que se houver um algoritmo prático (isto é , tempo polinomial aleatório ) para resolvê-lo, todos os problemas em NP podem ser resolvidos com a mesma facilidade.
• MAX-SAT , o problema de máxima satisfazibilidade , é uma generalização FNP do SAT. Ele pede o número máximo de cláusulas que podem ser satisfeitas por qualquer atribuição. Tem algoritmos de aproximação eficientes , mas é NP-difícil de resolver exatamente. Pior ainda, é APX -completo, o que significa que não há esquema de aproximação de tempo polinomial (PTAS) para este problema, a menos que P = NP.
• WMSAT é o problema de encontrar uma atribuição de peso mínimo que satisfaça uma fórmula booleana monótona (ou seja, uma fórmula sem qualquer negação). Pesos de variáveis ​​proposicionais são dados na entrada do problema. O peso de uma atribuição é a soma dos pesos das variáveis ​​verdadeiras. Esse problema é NP-completo (ver Th. 1 de).

Outras generalizações incluem satisfatibilidade para lógica de primeira e segunda ordem , problemas de satisfação de restrição , programação inteira 0-1 .

Autorredutibilidade

O problema SAT é auto-redutível , ou seja, cada algoritmo que responde corretamente se uma instância de SAT é solucionável pode ser usado para encontrar uma atribuição satisfatória. Primeiro, a pergunta é feita com base na fórmula Φ fornecida. Se a resposta for "não", a fórmula não é satisfatória. Caso contrário, a pergunta é feita na fórmula parcialmente instanciada Φ { x ₁ = TRUE} , ou seja, Φ com a primeira variável x ₁ substituída por TRUE, e simplificada de acordo. Se a resposta for "sim", então x ₁ = VERDADEIRO; caso contrário, x ₁ = FALSO. Os valores de outras variáveis ​​podem ser encontrados posteriormente da mesma maneira. No total, n + 1 execuções do algoritmo são necessárias, onde n é o número de variáveis ​​distintas em Φ.

Esta propriedade de autorredutibilidade é usada em vários teoremas da teoria da complexidade:

NP ⊆ P / poli ⇒ PH = Σ ₂   ( teorema de Karp-Lipton )

NP ⊆ BPP ⇒ NP = RP

P = NP ⇒ FP = FNP

Algoritmos para resolver SAT

Como o problema SAT é NP-completo, apenas algoritmos com complexidade exponencial de pior caso são conhecidos por ele. Apesar disso, algoritmos eficientes e escaláveis ​​para SAT foram desenvolvidos durante os anos 2000 e contribuíram para avanços dramáticos em nossa capacidade de resolver automaticamente instâncias de problemas envolvendo dezenas de milhares de variáveis ​​e milhões de restrições (ou seja, cláusulas). Exemplos de tais problemas em automação de projeto eletrônico (EDA) incluem verificação de equivalência formal , verificação de modelo , verificação formal de microprocessadores em pipeline , geração automática de padrão de teste , roteamento de FPGAs , problemas de planejamento e programação e assim por diante. Um mecanismo de resolução de SAT agora é considerado um componente essencial na caixa de ferramentas EDA .

Um solucionador DPLL SAT emprega um procedimento sistemático de pesquisa de retrocesso para explorar o espaço (de tamanho exponencial) de atribuições de variáveis ​​em busca de atribuições satisfatórias. O procedimento básico de pesquisa foi proposto em dois artigos seminais no início dos anos 1960 (ver referências abaixo) e agora é comumente referido como algoritmo Davis-Putnam-Logemann-Loveland ("DPLL" ou "DLL"). Muitas abordagens modernas para a resolução prática de SAT são derivadas do algoritmo DPLL e compartilham a mesma estrutura. Freqüentemente, eles apenas melhoram a eficiência de certas classes de problemas SAT, como instâncias que aparecem em aplicações industriais ou instâncias geradas aleatoriamente. Teoricamente, limites inferiores exponenciais foram provados para a família de algoritmos DPLL.

Algoritmos que não fazem parte da família DPLL incluem algoritmos de busca local estocástica . Um exemplo é WalkSAT . Os métodos estocásticos tentam encontrar uma interpretação satisfatória, mas não podem deduzir que uma instância SAT é insatisfatória, ao contrário de algoritmos completos, como DPLL.

Em contraste, algoritmos aleatórios como o algoritmo PPSZ de Paturi, Pudlak, Saks e Zane definem variáveis ​​em uma ordem aleatória de acordo com algumas heurísticas, por exemplo, resolução de largura limitada . Se a heurística não conseguir encontrar a configuração correta, a variável será atribuída aleatoriamente. O algoritmo PPSZ tem um tempo de execução de 3-SAT. Este era o tempo de execução mais conhecido para este problema até uma melhoria recente de Hansen, Kaplan, Zamir e Zwick que tem um tempo de execução para 3-SAT e atualmente o tempo de execução mais conhecido para k-SAT, para todos os valores de k. No cenário com muitas atribuições satisfatórias, o algoritmo aleatório de Schöning tem um limite melhor. ${\ displaystyle O (1.308 ^ {n})}$${\ displaystyle O (1.307 ^ {n})}$

Os solucionadores SAT modernos (desenvolvidos na década de 2000) vêm em dois sabores: "orientados para o conflito" e "antecipados". Ambas as abordagens descendem do DPLL. Solucionadores de conflitos , como aprendizagem de cláusula baseada em conflito (CDCL), aumentam o algoritmo de pesquisa DPLL básico com análise de conflito eficiente, aprendizagem de cláusula, retrocesso não cronológico (também conhecido como salto de retorno ), bem como unidade de "dois literais observados" propagação , ramificação adaptativa e reinicializações aleatórias. Esses "extras" para a pesquisa sistemática básica foram empiricamente mostrados como essenciais para lidar com as grandes instâncias de SAT que surgem na automação de projeto eletrônico (EDA). Implementações bem conhecidas incluem Chaff e GRASP . Os solucionadores de previsão reforçaram especialmente as reduções (indo além da propagação da cláusula de unidade) e as heurísticas, e geralmente são mais fortes do que os solucionadores de conflito em instâncias difíceis (enquanto os solucionadores de conflito podem ser muito melhores em grandes instâncias que realmente têm um instância fácil dentro).

Os solucionadores SAT modernos também estão tendo um impacto significativo nos campos de verificação de software, solução de restrições em inteligência artificial e pesquisa operacional, entre outros. Solucionadores poderosos estão disponíveis como software livre e de código aberto . Em particular, o MiniSAT voltado para conflitos , que foi relativamente bem-sucedido na competição SAT de 2005 , tem apenas cerca de 600 linhas de código. Um solver Parallel SAT moderno é o ManySAT. Ele pode alcançar acelerações superlineares em importantes classes de problemas. Um exemplo de solucionadores prospectivos é march_dl , que ganhou um prêmio na competição SAT de 2007 .

Certos tipos de grandes instâncias satisfatórias aleatórias de SAT podem ser resolvidos por propagação de pesquisa (SP). Particularmente em aplicações de design e verificação de hardware , a satisfatibilidade e outras propriedades lógicas de uma dada fórmula proposicional às vezes são decididas com base em uma representação da fórmula como um diagrama de decisão binário (BDD).

Quase todos os solucionadores de SAT incluem tempos limite, então eles serão encerrados em um tempo razoável, mesmo que não consigam encontrar uma solução. Diferentes solucionadores de SAT acharão diferentes instâncias fáceis ou difíceis, e alguns se destacam em provar insatisfação e outros em encontrar soluções. Todos esses comportamentos podem ser vistos nos concursos de resolução do SAT.

Resolução paralela de SAT

Os solucionadores SAT paralelos vêm em três categorias: portfólio, dividir e conquistar e algoritmos de busca local paralela . Com portfólios paralelos, vários solucionadores SAT diferentes são executados simultaneamente. Cada um deles resolve uma cópia da instância SAT, enquanto os algoritmos de divisão e conquista dividem o problema entre os processadores. Existem diferentes abordagens para paralelizar algoritmos de busca local.

A Competição Internacional de Solucionador de SAT tem uma trilha paralela que reflete os avanços recentes na solução de SAT paralela. Em 2016, 2017 e 2018, os benchmarks foram executados em um sistema de memória compartilhada com 24 núcleos de processamento , portanto, os solucionadores destinados a memória distribuída ou processadores manycore podem ter ficado aquém.

Portfólios

Em geral, não existe um solucionador de SAT com melhor desempenho do que todos os outros solucionadores em todos os problemas de SAT. Um algoritmo pode funcionar bem para instâncias problemáticas com as quais outras pessoas lutam, mas terá um desempenho pior com outras instâncias. Além disso, dada uma instância SAT, não há uma maneira confiável de prever qual algoritmo resolverá essa instância de maneira particularmente rápida. Essas limitações motivam a abordagem de portfólio paralelo. Um portfólio é um conjunto de algoritmos diferentes ou configurações diferentes do mesmo algoritmo. Todos os solucionadores em um portfólio paralelo são executados em processadores diferentes para resolver o mesmo problema. Se um solucionador for encerrado, o solucionador de portfólio relata que o problema pode ser satisfatório ou insatisfatório de acordo com esse solucionador. Todos os outros solucionadores são encerrados. Diversificar portfólios incluindo uma variedade de solucionadores, cada um com um bom desempenho em um conjunto diferente de problemas, aumenta a robustez do solucionador.

Muitos solucionadores usam internamente um gerador de números aleatórios . Diversificar suas sementes é uma forma simples de diversificar um portfólio. Outras estratégias de diversificação envolvem habilitar, desabilitar ou diversificar certas heurísticas no solver sequencial.

Uma desvantagem das carteiras paralelas é a quantidade de trabalho duplicado. Se o aprendizado de cláusula for usado nos solucionadores sequenciais, o compartilhamento de cláusulas aprendidas entre os solucionadores em execução paralela pode reduzir o trabalho duplicado e aumentar o desempenho. No entanto, mesmo simplesmente executando um portfólio dos melhores solucionadores em paralelo torna-se um solucionador paralelo competitivo. Um exemplo desse solucionador é o PPfolio. Ele foi projetado para encontrar um limite inferior para o desempenho que um solucionador SAT paralelo deve ser capaz de oferecer. Apesar da grande quantidade de trabalho duplicado devido à falta de otimizações, ele teve um bom desempenho em uma máquina de memória compartilhada. HordeSat é um solucionador de portfólio paralelo para grandes clusters de nós de computação. Ele usa instâncias configuradas de forma diferente do mesmo solucionador sequencial em seu núcleo. Particularmente para instâncias SAT rígidas, o HordeSat pode produzir acelerações lineares e, portanto, reduzir significativamente o tempo de execução.

Nos últimos anos, os solucionadores de SAT de portfólio paralelo têm dominado a trilha paralela das Competições Internacionais de Solucionador de SAT . Exemplos notáveis ​​de tais solucionadores incluem Plingeling e mcomsps indolor.

Dividir e conquistar

Em contraste com as carteiras paralelas, a divisão e conquista paralela tenta dividir o espaço de pesquisa entre os elementos de processamento. Algoritmos de divisão e conquista, como o DPLL sequencial, já aplicam a técnica de divisão do espaço de busca, portanto, sua extensão para um algoritmo paralelo é direta. No entanto, devido a técnicas como propagação de unidade, após uma divisão, os problemas parciais podem diferir significativamente em complexidade. Portanto, o algoritmo DPLL normalmente não processa cada parte do espaço de pesquisa na mesma quantidade de tempo, resultando em um problema desafiador de balanceamento de carga .

Fase de cubo para a fórmula . A heurística de decisão escolhe quais variáveis ​​(círculos) atribuir. Depois que a heurística de corte decide interromper a ramificação adicional, os problemas parciais (retângulos) são resolvidos independentemente usando CDCL.${\ displaystyle F}$

Devido ao retrocesso não cronológico, a paralelização da aprendizagem de cláusulas orientada por conflito é mais difícil. Uma maneira de superar isso é o paradigma Cube-and-Conquer . Ele sugere a resolução em duas fases. Na fase do "cubo", o problema é dividido em muitos milhares, até milhões, de seções. Isso é feito por um solucionador antecipado, que encontra um conjunto de configurações parciais chamadas "cubos". Um cubo também pode ser visto como uma conjunção de um subconjunto de variáveis ​​da fórmula original. Em conjunto com a fórmula, cada um dos cubos forma uma nova fórmula. Essas fórmulas podem ser resolvidas independentemente e simultaneamente por solucionadores orientados a conflitos. Como a disjunção dessas fórmulas é equivalente à fórmula original, o problema é relatado como satisfazível, se uma das fórmulas for satisfazível. O solucionador antecipado é favorável para problemas pequenos, mas difíceis, por isso é usado para dividir gradualmente o problema em vários subproblemas. Esses subproblemas são mais fáceis, mas ainda grandes, o que é a forma ideal para um solucionador voltado para conflitos. Além disso, os solucionadores com visão futura consideram todo o problema, enquanto os solucionadores orientados para o conflito tomam decisões com base em informações que são muito mais locais. Existem três heurísticas envolvidas na fase de cubo. As variáveis ​​nos cubos são escolhidas pela heurística de decisão. A heurística de direção decide qual atribuição de variável (verdadeira ou falsa) explorar primeiro. Em casos de problemas satisfatórios, escolher primeiro um ramo satisfatório é benéfico. A heurística de corte decide quando parar de expandir um cubo e, em vez disso, encaminhá-lo para um solucionador sequencial baseado em conflito. De preferência, os cubos são de resolução semelhante.

Treengeling é um exemplo de solucionador paralelo que aplica o paradigma Cube-and-Conquer. Desde a sua introdução em 2012, teve vários sucessos na Competição Internacional SAT Solver . Cube-and-Conquer foi usado para resolver o problema dos triplos Booleanos Pitagóricos .

Pesquisa local

Uma estratégia em direção a um algoritmo de busca local paralelo para resolver SAT é tentar várias inversões de variáveis ​​simultaneamente em unidades de processamento diferentes. Outra é aplicar a abordagem de portfólio mencionada anteriormente; no entanto, o compartilhamento de cláusulas não é possível, uma vez que os solucionadores de pesquisas locais não produzem cláusulas. Como alternativa, é possível compartilhar as configurações que são produzidas localmente. Essas configurações podem ser usadas para orientar a produção de uma nova configuração inicial quando um solucionador local decidir reiniciar sua pesquisa.

Veja também

• Núcleo insatisfatório
• Teorias do módulo de satisfação
• Contando SAT
• Planar SAT
• Algoritmo de Karloff-Zwick
• Satisfatibilidade do circuito

Notas

Referências

As referências são ordenadas por data de publicação:

links externos

• SAT Game - tente resolver um problema de satisfatibilidade booleana você mesmo

Formato de problema SAT

Um problema SAT é frequentemente descrito no formato DIMACS-CNF : um arquivo de entrada em que cada linha representa uma única disjunção. Por exemplo, um arquivo com duas linhas

1 -5 4 0
-1 5 3 4 0

representa a fórmula "( x ₁ ∨ ¬ x ₅ ∨ x ₄ ) ∧ (¬ x ₁ ∨ x ₅ ∨ x ₃ ∨ x ₄ )".

Outro formato comum para esta fórmula é a representação ASCII de 7 bits "(x1 | ~ x5 | x4) & (~ x1 | x5 | x3 | x4)".

• BCSAT é uma ferramenta que converte arquivos de entrada em formato legível para o formato DIMACS-CNF.

Solucionadores de SAT online

• BoolSAT - Resolve fórmulas no formato DIMACS-CNF ou em um formato mais amigável: "a e não b ou a". É executado em um servidor.
• Logictools - Fornece diferentes solucionadores em javascript para aprendizagem, comparação e hackeamento. É executado no navegador.
• minisat-in-your-browser - Resolve fórmulas no formato DIMACS-CNF. É executado no navegador.
• SATRennesPA - Resolve fórmulas escritas de uma forma amigável. É executado em um servidor.
• somerby.net/mack/logic - Resolve fórmulas escritas em lógica simbólica. É executado no navegador.

Solucionadores SAT offline

• MiniSAT - formato DIMACS-CNF e formato OPB para o solucionador de restrições Pseudo-Booleano que o acompanha MiniSat +
• Lingeling - ganhou a medalha de ouro em uma competição SAT 2011.
  • PicoSAT - um solucionador anterior do grupo Lingeling.
• Sat4j - formato DIMACS-CNF. Código-fonte Java disponível.
• Glicose - formato DIMACS-CNF.
• RSat - ganhou a medalha de ouro em uma competição SAT 2007.
• UBCSAT . Suporta cláusulas não ponderadas e ponderadas, ambas no formato DIMACS-CNF. Código-fonte C hospedado no GitHub .
• CryptoMiniSat - ganhou a medalha de ouro em uma competição SAT 2011. Código-fonte C ++ hospedado no GitHub . Tenta colocar muitos recursos úteis do núcleo MiniSat 2.0, PrecoSat ver 236 e Glucose em um pacote, adicionando muitos novos recursos
• Spear - Suporta aritmética de vetor de bits. Pode usar o formato DIMACS-CNF ou o formato Spear .
  • HyperSAT - Escrito para experimentar a poda do espaço de busca do cubo B. Ganhou o 3º lugar em uma competição SAT 2005. Um solucionador anterior e mais lento dos desenvolvedores do Spear.
• BASolver
• ArgoSAT
• Fast SAT Solver - baseado em algoritmos genéticos .
• zChaff - não é mais compatível.
• BCSAT - formato de circuito booleano legível (também converte este formato para o formato DIMACS-CNF e se vincula automaticamente ao MiniSAT ou zChaff).
• gini - Solucionador de SAT em linguagem Go com ferramentas relacionadas.
• gophersat - Solucionador de SAT em linguagem Go que também pode lidar com problemas pseudo-booleanos e MAXSAT.
• CLP (B) - Programação de lógica de restrição booleana, por exemplo SWI-Prolog .

Aplicativos SAT

• WinSAT v2.04 : Um aplicativo SAT baseado em Windows feito especialmente para pesquisadores.

Conferências

• Conferência Internacional sobre Teoria e Aplicações de Testes de Satisfação

Publicações

• Journal on Satisfiability, Boolean Modeling and Computation
• Propagação de pesquisa

Benchmarks

• Benchmarks de SAT satisfatórios forçados
• Benchmarks de verificação de software
• Fadi Aloul SAT Benchmarks

Resolução SAT em geral:

• http://www.satlive.org
• http://www.satisfiability.org

Avaliação de solucionadores SAT

• Avaliação anual de solucionadores SAT
• Resultados da avaliação dos solucionadores SAT para 2008
• Competições SAT internacionais
• História

Mais informações sobre o SAT:

• SAT e MAX-SAT para o pesquisador leigo
• SAT / SMT por exemplo

Este artigo inclui material de uma coluna no boletim eletrônico ACM SIGDA pelo Prof. Karem Sakallah
O texto original está disponível aqui