Cuantificadores universales en QBFS

Question

He estado buscando reducciones a / desde el idioma de TQBF y he logrado quedarse atascado en algo que casi ciertamente no es cierto (o, si es cierto, le estoy perdiendo un costo computacional significativo asociado con él) con Respeto a simplificar las instancias de TQBF.

Por el bien de la simplicidad, restrinja la atención a las instancias de TQBF en forma normal de PRENEX y CNF sin variables libres. Mi hipótesis (que sospecho firmemente es incorrecta, pero no ha podido encontrar un contador) es que tal TQBF es satisfactorio si es satisfactorio, si y solo si el TQBF que resulta de eliminar todas las instancias de las variables cuantificadas universalmente de la oración es satisfactoria. Por ejemplo, tome la siguiente instancia:

$ \ existe A \ forall b \ existe c \ forall d $ $ \ psi (a, b, c , d) $

$ \ psi (a, b, c, d)= (\ neg A \ vee b \ vee c) \ wedge (\ neg b \ vee \ net c \ vee d) \ wedge (A \ vee c \ vee \ neg d) $

Primero, sostengo que este ejemplo no es satisfactorio (fácilmente verificable a mano). Si aplicamos el método que describe anteriormente, obtenemos el siguiente "Core":

$ \ existe A \ existe C $ $ \ phi (a, c) $ , < / p>

$ \ phi (a, c)= (\ neg A \ vee c) \ wedge (\ neg c) \ wedge (A \ vee c) $

que claramente no es satisfactorio. Si en lugar de este ejemplo miramos esto:

$ \ existe A \ forall b \ existe c \ forall d $ $ \ psi (a, b, c , d) $

$ \ psi (a, b, c, d)= (\ neg A \ vee b \ vee \ neg c) \ wedge (\ net b \ vee c \ vee d) \ wedge (A \ vee c \ vee \ neg d) $

que claramente es satisfactorio (se establece C para verdadero, A a FALSO) y que tiene un "núcleo" de

$ \ existe A \ existe C $ $ \ phi (a, c) $ , < / p>

$ \ phi (a, c)= (\ neg A \ vee \ neg c) \ wedge (c) \ wedge (A \ vee c) $

que también es satisfactorio con la misma configuración variable.

Si este método siempre funciona, eso parece implicar que hay una reducción de TQBF a SAT en tiempo lineal en el número de cuantificadores universales y el número de apariciones de las variables cuantificadas universalmente en la fórmula, lo que muestra que TQBF es NP-Complete (ya se sabe que es PSPACE-complete y, por lo tanto, NP-HARD, por lo que si está en NP, es NP-Completa) y, además, que NP= PSPACE. Me sorprendería por completo si este es el caso, pero no he podido encontrar un contraejemplo (o un costo computacional que falta en la reducción que lo hace no el tiempo polinomial). ¿Qué estoy perdiendo?

Answer 1

Tu intuición era correcta. No funciona. Aquí hay un contraejemplo.

Considerar $ \ forall a \ existes b \ varphi (a, b) $ donde $ \ varphi (a, b)= (A \ lor \ NET B) \ Land (\ NEG A \ LOR B) $ . Esta afirmación se evalúa a VERDADERO.

Sin embargo, si eliminamos $ a $ siguiendo su procedimiento, obtenemos $ \ existes b \ psi (b) $ donde $ \ psi (b)= ((\ neg b) \ tierra (b)) $ ; y esa afirmación se evalúa a FALSO.

Una forma de entender por qué su método no funciona es que $ \ forall A \ existe B \ Varphi (A, B) $ no es equivalente a $ \ existe B \ Forlall A \ Varphi (A, B) $ . A lo sumo su método podría funcionar si todos los $ \ forall $ están en el interior, es decir, para una oración del formulario $ \ existes \ cdots \ existes \ forall \ cdots \ forall $ , pero no para ningún otro patrón de $ \ existe $ y $ \ forall $ .