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:
Primeiro, instale o SAT e aplique o teorema de Cook-Levin para reduzi-lo ao circuito do SAT.
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.
fonte
Respostas:
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}
withs1
es2
novas variáveis cujo valor dependerá de qual variável na cláusula original for verdadeirafonte
fonte
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:
fonte
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
fonte