Regla completa de resolución para 1-IN-K SAT

Question

En CNF SAT, cada cláusula (A o B o C o ...) debe contener al menos un verdadero literal.La regla de resolución se aplica al par de cláusulas que tienen exactamente un literal opuesto.

(A o B o C) y (! A o D o E)=> (B o C o D o E)

Digo que esta regla está completa, en el sentido de que si una fórmula es insatisfactoria, puedo probarlo aplicando la regla de manera exhaustiva (en instancias difíciles, una cantidad exponencial de veces) hasta que se produce una cláusula vacía.Si una fórmula tiene una solución única, puedo aplicar la regla hasta que se produce cada cláusula de unidad.

1-IN-K SAT es una variante completa de NP, donde exactamente una variable por cláusula (A, B, C, ....)= 1 es cierta.Dado un par de cláusulas con un literal opuesto, y no es literal común, también puedo producir un tercero:

(A, B, C)= 1 y (! A, D, E)= 1=> (B, C, D, E)= 1

Pregunta : ¿Es esta regla completa para las fórmulas 1 en K insatisfactorias y de manera única?

Answer 1

Estás tratando la resolución como si fuera una regla puramente sintáctica.Funciona de esa manera con las cláusulas CNF tradicionales porque corresponde a la regla subyacente de la inferencia.Pero una cláusula de CNF con la restricción adicional de un solo literal que se permite ser cierto, ya no corresponde a lo que se puede aplicar la regla de la resolución.

la expresión booleana $ (A \ lor b) \ land (\ lnot {a} \ lor \ lnot {b}) \ land (\ lnot {a} \ lor b) $ es insatisfiable como una fórmula 1-in-k-sat pero aplicando ingenuamente la regla de la resolución produce $ a= false, b= verdadero$ como una solución (incorrecta).