Redução direta de SAT para 3-SAT

18

Aqui, o objetivo é reduzir um problema arbitrário de SAT para 3-SAT em tempo polinomial usando o menor número de cláusulas e variáveis. Minha pergunta é motivada pela curiosidade. Menos formalmente, eu gostaria de saber: "Qual é a redução 'mais natural' de SAT para 3-SAT?"

Agora, a redução que eu sempre vi nos livros de texto é mais ou menos assim:

  1. Primeiro, instale o SAT e aplique o teorema de Cook-Levin para reduzi-lo ao circuito do SAT.

  2. Em seguida, você conclui o trabalho pela redução padrão do circuito SAT para 3-SAT, substituindo portas por cláusulas.

Enquanto isso funciona, as cláusulas 3-SAT resultantes acabam parecendo quase nada com as cláusulas SAT com as quais você começou, devido à aplicação inicial do teorema de Cook-Levin.

Alguém pode ver como fazer a redução mais diretamente, pulando a etapa do circuito intermediário e indo diretamente para o 3-SAT? Eu ficaria feliz com uma redução direta no caso especial do n-SAT.

(Eu acho que existem algumas vantagens entre o tempo de computação e o tamanho da saída. Claramente, uma solução degenerada - embora felizmente inadmissível, a menos que P = NP - seria apenas resolver o problema do SAT e emitir uma solução trivial. Instância -SAT ...)

EDIT: Com base na resposta da catraca, está claro agora que a redução para n-SAT é um tanto trivial (e que eu realmente deveria ter pensado nisso um pouco mais cuidadosamente antes de postar). Estou deixando essa questão em aberto um pouco, caso alguém saiba a resposta para a situação mais geral, caso contrário, simplesmente aceitarei a resposta da catraca.

Mikola
fonte
7
Não entendo o uso de Cook-Levin em (1). Boolean-formula-SAT já não é um caso especial do circuit-SAT no qual a estrutura gráfica do circuito é uma árvore?
Luca Trevisan

Respostas:

28

Cada cláusula SAT possui 1, 2, 3 ou mais variáveis. A cláusula de 3 variáveis ​​pode ser copiada sem problemas

As cláusulas 1 e 2 variáveis {a1}e {a1,a2}podem ser expandidas para {a1,a1,a1}e {a1,a2,a1}respectivamente.

A cláusula com mais de 3 variáveis {a1,a2,a3,a4,a5}pode ser expandida para {a1,a2,s1}{!s1,a3,s2}{!s2,a4,a5}with s1e s2novas variáveis ​​cujo valor dependerá de qual variável na cláusula original for verdadeira

catraca arrepiante
fonte
6
Cuidado. Quem disse que a entrada no SAT deve ter "cláusulas"?
Jeffε
6
A questão disse: "Eu iria mesmo ser feliz com uma redução direta no caso especial de n-SAT"
Ryan Williams
Sim, isso funciona! Acho que deveria ter pensado um pouco mais cuidadosamente antes de adicionar essa última linha, mas se eu não receber uma resposta para a pergunta mais geral, aceitarei isso.
Mikola
1
@ Mikola Talvez a transformação Tseitin ou Plaisted-Greenbaum lhe dê 3CNF? (Eu não estou completamente certo que eu entendo a pergunta totalmente :))
Mikolas
Fiquei me perguntando por que a extensão especificamente para k = 1 mencionada pela catraca não está aparecendo em nenhum livro (pelo menos as que encontrei até agora). Meu raciocínio é que, por definição, um literal pode ser 'não a1', que não pode ser estendido como {a1, a1, a1}. Por outro lado, você não pode fazer {'not a1', 'not a1', 'not a1]}, pois precisa de outra lógica para identificar se o sat original inclui um literal negado ou não. Esta é a razão (presumivelmente) de todos os autores, incluindo Michael R. Garey e David S. Johnson, que usaram uma extensão diferente apresentada por 'Carlos Linares López' em seu post aqui.
KGhatak 6/09
27

nn

Bart Jansen
fonte
19

Se você precisar de uma redução de k-SAT para 3-SAT, a resposta da catraca funcionará bem.

Se você deseja uma redução direta da fórmula proposicional genérica para o CNF (e para o 3-SAT), então - pelo menos da "perspectiva do SAT solucionador" - acho que a resposta para sua pergunta Qual é a redução 'mais natural' ... ? , é: Não há redução 'natural' !

Das conclusões do Capítulo 2 - "Codificações da CNF" do (muito bom) livro: Manual de Satisfação :

...
Geralmente, existem muitas maneiras de modelar um determinado problema na CNF, e poucas diretrizes são conhecidas para escolher entre elas. Geralmente, há uma variedade de recursos de problemas para modelar como variáveis, e alguns podem levar considerações consideráveis ​​para serem descobertas. As codificações de tseitina são compactas e mecanizáveis, mas na prática nem sempre levam ao melhor modelo, e algumas subformulas podem ser melhor expandidas. Algumas cláusulas podem ser omitidas por considerações de polaridade, e cláusulas implícitas de quebra de simetria ou de bloqueio podem ser adicionadas. Codificações diferentes podem ter vantagens e desvantagens diferentes, como tamanho ou densidade da solução, e o que é uma vantagem para um solucionador SAT pode ser uma desvantagem para outro. Em suma, a modelagem da CNF é uma arte e devemos frequentemente prosseguir por intuição e experimentação.
...

O algoritmo mais conhecido é o algoritmo Tseitin (G. Tseitin. Sobre a complexidade da derivação no cálculo proposicional. Automação de raciocínio: papéis clássicos em lógica computacional, 2: 466-483, 1983. Springer-Verlag.)

Para uma boa introdução às codificações CNF, leia o livro sugerido Handbook o Satisfability . Você também pode ler alguns trabalhos recentes e consultar as referências; por exemplo:

  • P. Jackson e D. Sheridan. Conversões de forma de cláusula para circuitos booleanos. Em HH Hoos e DG Mitchell, editores, Theory and Applications of Satisfiability Testing, 7ª Conferência Internacional, SAT 2004 , volume 3542 do LNCS, páginas 183–198. Springer, 2004. (que visa reduzir o número de cláusulas)
  • P. Manolios, D. Vroon, circuito eficiente para conversão CNF. Em Teoria e Aplicações de Testes de Satisfação - SAT 2007 (2007), pp. 4-9
Marzio De Biasi
fonte
15

Deixe-me postar outra solução semelhante à de Ratchel, mas um pouco diferente. Isso é retirado diretamente do capítulo 9 da 2ª edição do "The Algorithm Design Manual" de Steven Skiena

  • Se a cláusula tiver apenas um literal C = {z1}, crie duas novas variáveis ​​v1 e v2 e quatro novas cláusulas tridimensionais: {v1, v2, z1}, {! V1, v2, z1}, {v1,! v2, z1} e {! v1,! v2, z1}. Observe que a única maneira pela qual todas as quatro cláusulas podem ser satisfeitas simultaneamente é se z1 = T, o que também significa que o C original será satisfeito
  • Se a cláusula tiver dois literais, C = {z1, z2}, crie uma nova variável v1 e duas novas cláusulas: {v1, z1, z2} e {! V1, z1, z2}. Novamente, a única maneira de satisfazer essas duas cláusulas é ter pelo menos uma de z1 e z2 verdadeira, satisfazendo C
  • Se a cláusula tiver três literais, C = {z1, z2, z3}, basta copiar C na instância 3-SAT inalterada
  • Se a cláusula tiver mais de 3 literais C = {z1, z2, ..., zn}, crie n-3 novas variáveis ​​e n-2 novas cláusulas em uma cadeia, onde para 2 <= j <= n-2 , Cij = {v1, j-1, zj + 1,! Vi, j}, Ci1 = {z1, z2,! Vi, 1} e Ci, n-2 = {vi, n-3, zn-1, zn}
Carlos Linares López
fonte
1
@TayfunPay Você pode explicar por que considera esta solução mais correta? Duplicar variáveis ​​parece mais natural para mim e não viola nenhuma definição do 3SAT que eu já vi. Existe alguma tecnicidade que melhore essa solução?
Crockeea