O problema padrão 1-em-3 SAT (ou XSAT ou X3SAT) é:
Instância : uma fórmula CNF com todas as cláusulas contendo exatamente 3 literais.
Pergunta : existe uma atribuição satisfatória configurando exatamente 1 literal por cláusula?
O problema é NP-completo e permanece difícil, mesmo se nenhuma variável ocorrer negada. Gostaria de saber se esse problema se torna fácil ou permanece difícil se for necessário que cada variável ocorra pelo menos uma vez de forma positiva e pelo menos uma vez de forma negativa .
A redução habitual do 3SAT mostrando que 1-in-3 SAT é substitui rígidos uma cláusula por cláusulas ( ¬ x ∨ um ∨ b ) , ( y ∨ b ∨ c ) , ( ¬ z ∨ c ∨ d ) onde a , b , c , dsão novos para cada cláusula. Portanto, essa redução não ajuda a responder à minha pergunta. Eu tive problemas para criar um gadget que mostre a dureza dessa variante, pois se exatamente 1 literal em uma cláusula for verdadeiro, então 2 literais não simétricos serão falsos. Se for fácil, pensar em termos de partições do conjunto de cláusulas pode fazê-lo, mas não vejo como.
fonte
Respostas:
Em um comentário, o OP expressou interesse em uma redução que gerou instâncias com 3 variáveis distintas por cláusula. Aqui está uma abordagem simples:
A redução é de 1-em-3 SAT com 3 variáveis distintas por cláusula:
Vamos verificar se essa redução faz o que queremos. As seguintes propriedades são o que queremos:
fonte