El lenguaje Critical SAT se define como el conjunto de fórmulas booleanas f tal que f ∈ U N S A T, pero eliminar cualquier cláusula de f lo hace satisfactorio. Se sabe que el SAT crítico es D P -completo. Me pregunto acerca de la siguiente variante: dada una fórmula C N F f , ¿es el caso que f está en U N S A T y que existe alguna cláusula c tal que f ∖ c ∈ (en lugar de para todas las cláusulas, existe una cláusula). ¿Esta variante D P -completa también?
Está claro que su idioma está en DP. Para demostrar que es DP-hard, le daremos una reducción de SAT-UNSAT a su idioma, lo que podemos llamar CRIT-UNSAT. Dado un par de CNF , que x , y sean variables frescas, y que h = ( f ∨ ¬ x ) ∧ ( g ∨ x ) ∧ ( g ∨ y ) ∧ ¬ x ∧ ( x ∨ ¬ y ) . Aquí f ∨
Supongamos primero que es satisfactoria yg no es satisfactoria. Como g no es satisfactoria, h no es satisfactoria. Como f es satisfactoria, h ∖ ¬ x es satisfactoria. Por lo tanto, h está en CRIT-SAT.
Por el contrario, suponga que está en CRIT-SAT. Como h es insatisfactorio, g es insatisfactorio. Para alguna cláusula c , h ∖ c es satisfactoria. Si c ∈ f ∨ ¬ x entonces claramente h ∖ c sigue siendo insatisfactorio. Del mismo modo, si c ∈ g ∨ x entonces h ∖ c sigue siendo insatisfactorio, debido a g ∨ y . Si c ∈ g ∨ y o c = luego h ∖ c sigue siendo insatisfactorio, debido a g ∨ x . Entonces c = ¬ x , lo que significa que h | x = 1 es satisfactoria, es decir, f es satisfactoria.