Regra de resolução completa para 1-in-k sentado

Question

No CNF SAT, cada cláusula (A ou B ou C ou ...) deve conter pelo menos um verdadeiro literal.A regra de resolução se aplica ao par de cláusulas que têm exatamente um literal oposto.

(a ou b ou c) e (! a ou d ou e)=> (b ou c ou d ou e)

Eu digo que esta regra está completa, no sentido de que, se uma fórmula é insatisfatória, posso provar que aplicando a regra exaustivamente (em instâncias difíceis, uma quantidade exponencial de vezes) até que uma cláusula vazia seja produzida.Se uma fórmula tiver uma solução única, posso aplicar a regra até que cada cláusula unitária seja produzida.

1-in-k sáb é uma variante completa NP, onde exatamente uma variável por cláusula (A, B, C, ....)= 1 é verdadeira.Dado um par de cláusula com um literal oposto, e nenhum literal comum, eu também posso produzir um terceiro:

(a, b, c)= 1 e (! a, d, e)= 1=> (b, c, d, e)= 1

pergunta : Esta regra é completa para fórmulas 1-in-K exclusivamente satisfatórias?

Answer 1

Você está tratando a resolução como se fosse uma regra puramente sintática.Ele funciona dessa maneira com cláusulas tradicionais do CNF porque isso corresponde à regra subjacente de inferência.Mas uma cláusula CNF com a restrição adicionada de apenas um literal permissão para ser verdadeira não corresponde mais ao que a regra de resolução pode ser válida válida.

a expressão booleana $ (a \ lor b) \ terra (\ lnot {a} \ lor \ lnot {b}) \ terra (\ lnot {a} \ lor b) $ é insatisfatório como um 1-in-k-sit fmula, mas aplicar ingenuamente a regra de resolução produz $ a= FALSE, B= TRUE$ como uma solução (errada).