variante do SAT Crítico

O idioma Critical SAT é definido como o conjunto de fórmulas booleanas tal modo que mas remover qualquer cláusula de torna satisfatório. Sabe-se que o Critical SAT é completo. Gostaria de saber sobre a seguinte variante: dada uma fórmula , é o caso de estar em e de que existe alguma cláusula tal que (em vez de todas as cláusulas, existe uma cláusula) . Essa variante de também está completa?F F ∈ L N S A T f D P C N F F F L N S A T c F ∖ c ∈ S A T D $CNF$$f$$f \in UNSAT$$f$$DP$$CNF$$f$$f$$UNSAT$$c$$f \setminus c \in SAT$$DP$

É claro que seu idioma está no DP. Para mostrar que é difícil para o DP, reduziremos o SAT-UNSAT para o seu idioma, que podemos chamar de CRIT-UNSAT. Dado um par de CNFs , sejam variáveis ​​novas e Aqui significa adicionar a todas as cláusulas de .x , y h = ( f ∨ ¬ x ) ∧ ( g ∨ x ) ∧ ( g ∨ y ) ∧ ¬ x ∧ ( x ∨ ¬ y ) . f ∨ ¬ $(f,g)$$x,y$

Suponha primeiro que seja satisfatório não seja satisfatório. Como não é satisfatório, não é satisfatório. Como é satisfatório, é satisfatório. Assim, está em CRIT-SAT.g g h f h ∖ ¬ x $f$$g$$g$$h$$f$$h \setminus \lnot x$$h$

Por outro lado, suponha que esteja em CRIT-SAT. Como é insatisfatório, é insatisfatório. Para alguma cláusula , é satisfatório. Se então claramente ainda é insatisfatório. Da mesma forma, se então ainda é insatisfatório, devido a . Se ou , ainda é insatisfatório, devido a . Assim, , o que significa queh g c h ∖ c c ∈ f ∨ ¬ x h ∖ c c ∈ g ∨ x h ∖ c g ∨ y c ∈ g ∨ y c = x ∨ ¬ y h ∖ c g ∨ x c = ¬ x h | x = 1$h$$h$$g$$c$$h \setminus c$$c \in f \lor \lnot x$$h \setminus c$$c \in g \lor x$$h \setminus c$$g \lor y$$c \in g \lor y$$c = x \lor \lnot y$$h \setminus c$$g \lor x$$c = \lnot x$$h|_{x=1}$ é satisfatório, isto é, é satisfatório.$f$