En la teoría de la complejidad computacional , el lenguaje TQBF es un lenguaje formal que consta de las verdaderas fórmulas booleanas cuantificadas . Una fórmula booleana (completamente) cuantificada es una fórmula en lógica proposicional cuantificada en la que cada variable se cuantifica (o limita ), utilizando cuantificadores existenciales o universales , al comienzo de la oración. Tal fórmula es equivalente a verdadero o falso (ya que no hay variables libres ). Si dicha fórmula se evalúa como verdadera, entonces esa fórmula está en el lenguaje TQBF. También se conoce como QSAT (Quantified SAT).
En teoría de la complejidad computacional, el problema fórmula Boolean cuantificada ( QBF ) es una generalización de la problema satisfacibilidad booleana en la que ambos cuantificadores existenciales y cuantificadores universales se pueden aplicar a cada variable. Dicho de otra manera, pregunta si una forma de oración cuantificada sobre un conjunto de variables booleanas es verdadera o falsa. Por ejemplo, la siguiente es una instancia de QBF:
QBF es el problema canónico completo para PSPACE , la clase de problemas que puede resolver una máquina de Turing determinista o no determinista en un espacio polinomial y en un tiempo ilimitado. [1] Dada la fórmula en forma de árbol de sintaxis abstracta , el problema puede resolverse fácilmente mediante un conjunto de procedimientos recursivos entre sí que evalúan la fórmula. Dicho algoritmo usa un espacio proporcional a la altura del árbol, que es lineal en el peor de los casos, pero usa el tiempo exponencial en el número de cuantificadores.
Siempre que MA ⊊ PSPACE, que se cree ampliamente, QBF no se puede resolver, ni siquiera se puede verificar una solución dada, en tiempo polinomial determinista o probabilístico (de hecho, a diferencia del problema de satisfacibilidad, no existe una forma conocida de especificar una solución de manera sucinta ). Se puede resolver usando una máquina de Turing alternante en tiempo lineal, ya que AP = PSPACE, donde AP es la clase de problemas que las máquinas alternas pueden resolver en tiempo polinomial. [2]
Cuando se mostró el resultado fundamental IP = PSPACE (ver sistema de prueba interactivo ), se hizo exhibiendo un sistema de prueba interactivo que podría resolver QBF al resolver una aritmetización particular del problema. [3]
Las fórmulas QBF tienen varias formas canónicas útiles. Por ejemplo, se puede demostrar que hay una reducción muchos-uno en tiempo polinómico que moverá todos los cuantificadores al frente de la fórmula y los hará alternar entre cuantificadores universales y existenciales. Hay otra reducción que resultó útil en la prueba IP = PSPACE donde no se coloca más de un cuantificador universal entre el uso de cada variable y el cuantificador que une esa variable. Esto fue fundamental para limitar el número de productos en ciertas subexpresiones de la aritmetización.