Fórmula booleana cuantificada verdadera

En la teoría de la complejidad computacional , el lenguaje TQBF es un lenguaje formal que consta de fórmulas booleanas cuantificadas verdaderas . Una fórmula booleana (completamente) cuantificada es una fórmula en lógica proposicional cuantificada (también conocida como lógica proposicional de segundo orden ) donde cada variable se cuantifica (o se vincula ) al comienzo de la oración mediante cuantificadores existenciales o universales . Dicha fórmula es equivalente a verdadero o falso (ya que no hay variables libres ). Si dicha fórmula se evalúa como verdadera, entonces pertenece al lenguaje TQBF. También se conoce como QSAT (Quantified SAT ).

En la teoría de la complejidad computacional, el problema de la fórmula booleana cuantificada ( QBF ) es una generalización del problema de satisfacibilidad booleana en el que se pueden aplicar tanto cuantificadores existenciales como universales a cada variable. Dicho de otro modo, plantea la cuestión de si una fórmula proposicional cuantificada sobre un conjunto de variables booleanas es verdadera o falsa. Por ejemplo, el siguiente es un caso de QBF:

${\displaystyle \forall x\ \exists y\ \exists z\ ((x\lor z)\land y)}$

QBF es el problema completo canónico para PSPACE , la clase de problemas resolubles por una máquina de Turing determinista o no determinista en espacio polinomial y tiempo ilimitado. ^{[ 1 ]} Dada la fórmula en forma de árbol de sintaxis abstracta , el problema se puede resolver fácilmente mediante un conjunto de procedimientos mutuamente recursivos que evalúan la fórmula. Dicho algoritmo utiliza espacio proporcional a la altura del árbol, que es lineal en el peor de los casos, pero utiliza tiempo exponencial en el número de cuantificadores.

Siempre que MA ⊊ PSPACE, como se cree ampliamente, QBF no puede resolverse, ni siquiera puede verificarse una solución dada, en tiempo polinomial determinista o probabilístico (de hecho, a diferencia del problema de satisfacibilidad, no se conoce ninguna forma de especificar una solución de manera concisa). Puede resolverse utilizando una máquina de Turing alternante en tiempo lineal, ya que AP = PSPACE, donde AP es la clase de problemas que las máquinas alternantes pueden resolver en tiempo polinomial. ^{[ 2 ]}

Cuando se mostró el resultado fundamental IP = PSPACE (véase el sistema de prueba interactivo ), se hizo exhibiendo un sistema de prueba interactivo que podía resolver QBF resolviendo una aritmetización particular del problema. ^{[ 3 ]}

Las fórmulas QBF poseen varias formas canónicas útiles. Por ejemplo, se puede demostrar que existe una reducción de muchos a uno en tiempo polinomial que desplaza todos los cuantificadores al principio de la fórmula, alternando entre cuantificadores universales y existenciales. Existe otra reducción que resultó útil en la demostración de IP = PSPACE, donde no se coloca más de un cuantificador universal entre el uso de cada variable y el cuantificador que la vincula. Esto fue crucial para limitar el número de productos en ciertas subexpresiones de la aritmetización.

Se puede asumir que una fórmula booleana totalmente cuantificada tiene una forma muy específica, llamada forma normal prenexa . Tiene dos partes básicas: una porción que contiene solo cuantificadores y una porción que contiene una fórmula booleana no cuantificada que generalmente se denota como${\displaystyle \displaystyle \phi }$. Si hay${\displaystyle \displaystyle n}$Variables booleanas, la fórmula completa se puede escribir como

${\displaystyle \displaystyle \exists x_{1}\forall x_{2}\exists x_{3}\cdots Q_{n}x_{n}\phi (x_{1},x_{2},x_{3},\dots ,x_{n})}$

donde cada variable cae dentro del alcance de algún cuantificador. Al introducir variables ficticias, cualquier fórmula en forma normal prenexa puede convertirse en una oración donde se alternan cuantificadores existenciales y universales. Usando la variable ficticia${\displaystyle \displaystyle y_{1}}$,

${\displaystyle \displaystyle \exists x_{1}\exists x_{2}\phi (x_{1},x_{2})\quad \mapsto \quad \exists x_{1}\forall y_{1}\exists x_{2}\phi (x_{1},x_{2})}$

La segunda oración tiene el mismo valor de verdad, pero sigue la sintaxis restringida. Suponer que las fórmulas booleanas totalmente cuantificadas están en forma normal prenexa es una característica frecuente de las demostraciones.

Los solucionadores QBF se pueden aplicar a la planificación (en inteligencia artificial), incluida la planificación segura; esta última es fundamental en aplicaciones de robótica. ^{[ 14 ]} Los solucionadores QBF también se pueden aplicar a la verificación de modelos acotados , ya que proporcionan una codificación más corta que la que se necesitaría para un solucionador basado en SAT. ^{[ 14 ]}

La evaluación de un QBF puede considerarse un juego de dos jugadores entre un jugador que controla variables cuantificadas existencialmente y un jugador que controla variables cuantificadas universalmente. Esto hace que los QBF sean adecuados para codificar problemas de síntesis reactiva . ^{[ 14 ]} De manera similar, los solucionadores de QBF pueden usarse para modelar juegos adversariales en teoría de juegos . Por ejemplo, los solucionadores de QBF pueden usarse para encontrar estrategias ganadoras para juegos de geografía , que luego pueden jugarse automáticamente de forma interactiva. ^{[ 15 ]}

Los solucionadores QBF se pueden utilizar para la comprobación de equivalencia formal y también para sintetizar funciones booleanas. ^{[ 14 ]}

Otros tipos de problemas que pueden codificarse como QBF incluyen:

• Detectar si una cláusula en una fórmula insatisfacible en forma normal conjuntiva pertenece a algún subconjunto mínimamente insatisfacible ^{[ 9 ] [ 16 ]} y si una cláusula en una fórmula satisfacible pertenece a un subconjunto máximamente satisfacible ^{[ 16 ]}
• Codificaciones de planificación conforme ^{[ 9 ]}
• Problemas relacionados con ASP ^{[ 9 ]}
• Argumentación abstracta ^{[ 9 ]}
• Verificación de modelos de lógica temporal lineal ^{[ 9 ]}
• Inclusión de lenguajes de autómatas finitos no deterministas ^{[ 9 ]}
• Síntesis y fiabilidad de sistemas distribuidos ^{[ 9 ]}

El problema de satisfacibilidad estocástica (conocido como SSAT) es una extensión de TQBF que agrega un cuantificador R aleatorio, considera la cuantificación universal como minimización y la cuantificación existencial como maximización, y pregunta si la probabilidad representada por la fórmula excede un umbral dado. ^{[ 17 ]}

QBF también puede extenderse para tener cuantificadores de Henkin . ^{[ 8 ]}

El lenguaje TQBF sirve en la teoría de la complejidad como el problema canónico PSPACE-completo . Ser PSPACE-completo significa que un lenguaje está en PSPACE y que el lenguaje también es PSPACE-difícil . El algoritmo anterior muestra que TQBF está en PSPACE. Demostrar que TQBF es PSPACE-difícil requiere demostrar que cualquier lenguaje en la clase de complejidad PSPACE puede reducirse a TQBF en tiempo polinomial. Es decir,

${\displaystyle \forall L\in {\mathsf {PSPACE}},L\leq _{p}\mathrm {TQBF} .}$

Esto significa que, para un lenguaje PSPACE L, se puede decidir si una entrada x está en L comprobando si${\displaystyle f(x)}$está en TQBF, para alguna función f que debe ejecutarse en tiempo polinomial (en relación con la longitud de la entrada). Simbólicamente,

${\displaystyle x\in L\iff f(x)\in \mathrm {TQBF} .}$

Demostrar que TQBF es PSPACE-difícil requiere especificar f .

Supongamos entonces que L es un lenguaje PSPACE. Esto significa que L puede ser decidido por una máquina de Turing determinista de espacio polinomial (DTM). Esto es muy importante para la reducción de L a TQBF, porque las configuraciones de cualquier máquina de Turing de este tipo pueden representarse como fórmulas booleanas, con variables booleanas que representan el estado de la máquina, así como el contenido de cada celda en la cinta de la máquina de Turing, con la posición del cabezal de la máquina de Turing codificada en la fórmula mediante el orden de la fórmula. En particular, nuestra reducción utilizará las variables${\displaystyle c_{1}}$y${\displaystyle c_{2}}$, que representan dos posibles configuraciones del DTM para L y un número natural t, en la construcción de un QBF${\displaystyle \phi _{c_{1},c_{2},t}}$lo cual es cierto si y solo si el DTM para L puede pasar de la configuración codificada en${\displaystyle c_{1}}$a la configuración codificada en${\displaystyle c_{2}}$en no más de t pasos. La función f , entonces, se construirá a partir del DTM para L a QBF${\displaystyle \phi _{c_{\text{start}},c_{\text{accept}},T}}$, dónde${\displaystyle c_{start}}$es la configuración inicial del DTM,${\displaystyle c_{\text{accept}}}$es la configuración de aceptación del DTM, y T es el número máximo de pasos que el DTM podría necesitar para pasar de una configuración a otra. Sabemos que T = O (exp( n ^k )) para algún k , donde n es la longitud de la entrada, porque esto limita el número total de configuraciones posibles del DTM relevante. Por supuesto, el DTM no puede tomar más pasos de los que hay configuraciones posibles para alcanzar.${\displaystyle c_{\mathrm {accept} }}$a menos que entre en un bucle, en cuyo caso nunca llegará.${\displaystyle c_{\mathrm {accept} }}$de todos modos.

En esta etapa de la demostración, ya hemos reducido la cuestión de si una fórmula de entrada w (codificada, por supuesto, en${\displaystyle c_{\text{start}}}$) está en L respecto a la cuestión de si el QBF${\displaystyle \phi _{c_{\text{start}},c_{\text{accept}},T}}$, es decir,${\displaystyle f(w)}$, está en TQBF. El resto de esta demostración prueba que f se puede calcular en tiempo polinomial.

Para${\displaystyle t=1}$, cálculo de${\displaystyle \phi _{c_{1},c_{2},t}}$Es sencillo: o una de las configuraciones cambia a la otra en un solo paso, o no. Dado que la máquina de Turing que representa nuestra fórmula es determinista, esto no supone ningún problema.

Para${\displaystyle t>1}$, cálculo de${\displaystyle \phi _{c_{1},c_{2},t}}$implica una evaluación recursiva, buscando un llamado "punto medio".${\displaystyle m_{1}}$En este caso, reescribimos la fórmula de la siguiente manera:

${\displaystyle \phi _{c_{1},c_{2},t}=\exists m_{1}(\phi _{c_{1},m_{1},\lceil t/2\rceil }\wedge \phi _{m_{1},c_{2},\lceil t/2\rceil }).}$

Esto convierte la cuestión de si${\displaystyle c_{1}}$puede alcanzar${\displaystyle c_{2}}$en pasos a la cuestión de si${\displaystyle c_{1}}$llega a un punto medio${\displaystyle m_{1}}$en${\displaystyle t/2}$escalones, que a su vez llega${\displaystyle c_{2}}$en${\displaystyle t/2}$pasos. La respuesta a la segunda pregunta, por supuesto, da la respuesta a la primera.

Ahora, t solo está limitado por T, que es exponencial (y por lo tanto no polinomial) en la longitud de la entrada. Además, cada capa recursiva prácticamente duplica la longitud de la fórmula. (La variable${\displaystyle m_{1}}$es solo un punto medio; para valores mayores de t, hay más paradas en el camino, por así decirlo.) Entonces, el tiempo requerido para evaluar recursivamente${\displaystyle \phi _{c_{1},c_{2},t}}$De esta manera también podría ser exponencial, simplemente porque la fórmula podría volverse exponencialmente grande. Este problema se resuelve cuantificando universalmente usando variables.${\displaystyle c_{3}}$y${\displaystyle c_{4}}$sobre los pares de configuración (por ejemplo,${\displaystyle \{(c_{1},m_{1}),(m_{1},c_{2})\}}$), lo que impide que la longitud de la fórmula se expanda debido a capas recursivas. Esto produce la siguiente interpretación de${\displaystyle \phi _{c_{1},c_{2},t}}$:

${\displaystyle \phi _{c_{1},c_{2},t}=\exists m_{1}\forall (c_{3},c_{4})\in \{(c_{1},m_{1}),(m_{1},c_{2})\}(\phi _{c_{3},c_{4},\lceil t/2\rceil }).}$

Esta versión de la fórmula se puede calcular en tiempo polinomial, ya que cualquier instancia de ella se puede calcular en tiempo polinomial. El par ordenado cuantificado universalmente simplemente nos dice que cualquier elección de${\displaystyle (c_{3},c_{4})}$está hecho,${\displaystyle \phi _{c_{1},c_{2},t}\iff \phi _{c_{3},c_{4},\lceil t/2\rceil }}$.

De este modo,${\displaystyle \forall L\in {\mathsf {PSPACE}},L\leq _{p}\mathrm {TQBF} }$Por lo tanto, TQBF es PSPACE-difícil. Junto con el resultado anterior de que TQBF está en PSPACE, esto completa la prueba de que TQBF es un lenguaje PSPACE-completo.

(Esta demostración sigue  en lo esencial a Sipser 2006, págs. 310-313. Papadimitriou 1994 también incluye una demostración).

Esta construcción se puede ejecutar en el espacio logarítmico, lo que significa que TQBF es PSPACE-completo en el sentido de reducción muchos-uno en el espacio logarítmico . ^{[ 18 ]}

• Un subproblema importante en TQBF es el problema de satisfacibilidad booleana . En este problema, se desea saber si una fórmula booleana dada es verdadera.${\displaystyle \phi }$puede hacerse verdadero con alguna asignación de variables. Esto es equivalente al TQBF usando solo cuantificadores existenciales:$${\displaystyle \exists x_{1}\cdots \exists x_{n}\phi (x_{1},\ldots ,x_{n})}$$Este es también un ejemplo del resultado más amplio NP ⊆ PSPACE que se deriva directamente de la observación de que un verificador de tiempo polinomial para una prueba de un lenguaje aceptado por una NTM ( máquina de Turing no determinista ) requiere espacio polinomial para almacenar la prueba.
• Cualquier clase en la jerarquía polinomial ( PH ) tiene TQBF como un problema difícil. En otras palabras, para la clase que comprende todos los lenguajes L para los cuales existe una TM polinomial V, un verificador, tal que para toda entrada x y alguna constante i,$${\displaystyle x\in L\Leftrightarrow \exists y_{1}\forall y_{2}\cdots Q_{i}y_{i}\ V(x,y_{1},y_{2},\dots ,y_{i})\ =\ 1}$$que tiene una formulación QBF específica que se da como$${\displaystyle \exists \phi }$$ de tal manera que${\displaystyle \exists {\vec {x_{1}}}\forall {\vec {x_{2}}}\cdots Q_{i}{\vec {x_{i}}}\ \phi ({\vec {x_{1}}},{\vec {x_{2}}},\dots ,{\vec {x_{i}}})\ =\ 1}$donde el${\displaystyle {\vec {x_{i}}}}$son vectores de variables booleanas.
• Es importante señalar que, si bien el lenguaje TQBF se define como el conjunto de fórmulas booleanas cuantificadas verdaderas, la abreviatura TQBF se usa con frecuencia (incluso en este artículo) para referirse a una fórmula booleana totalmente cuantificada, a menudo denominada simplemente QBF (fórmula booleana cuantificada, entendida como "totalmente" cuantificada). Es importante distinguir, en función del contexto, entre los dos usos de la abreviatura TQBF al consultar la bibliografía.
• Un TQBF puede considerarse un juego entre dos jugadores, con turnos alternos. Las variables cuantificadas existencialmente equivalen a la noción de que un jugador tiene un movimiento disponible en su turno. Las variables cuantificadas universalmente implican que el resultado del juego no depende del movimiento que realice un jugador en ese turno. Asimismo, un TQBF cuyo primer cuantificador es existencial corresponde a un juego de fórmula en el que el primer jugador posee una estrategia ganadora.
• Un TQBF cuya fórmula cuantificada está en 2-CNF puede resolverse en tiempo lineal mediante un algoritmo que implica un análisis de conectividad fuerte de su grafo de implicación . El problema de 2-satisfacibilidad es un caso especial de TQBF para estas fórmulas, en el que cada cuantificador es existencial. ^{[ 19 ] [ 20 ]}
• En un artículo divulgativo de Hubie Chen se ofrece un tratamiento sistemático de las versiones restringidas de fórmulas booleanas cuantificadas (que dan lugar a clasificaciones de tipo Schaefer). ^{[ 21 ]}
• Planar TQBF, que generaliza Planar SAT , fue demostrado PSPACE-completo por D. Lichtenstein. ^{[ 22 ]}

• Fortnow y Homer (2003) proporcionan algunos antecedentes históricos sobre PSPACE y TQBF.
• Zhang (2003) proporciona algunos antecedentes históricos de las fórmulas booleanas.
• Arora, Sanjeev. (2001). COS 522: Complejidad Computacional . Apuntes de clase, Universidad de Princeton. Recuperado el 10 de octubre de 2005.
• Fortnow, Lance y Steve Homer. (2003, junio). Una breve historia de la complejidad computacional . Boletín de la Asociación Europea de Ciencias de la Computación Teórica , Columna de Complejidad Computacional, 80. Recuperado el 14 de mayo de 2024.
• Papadimitriou, CH (1994). Complejidad computacional. Reading: Addison-Wesley.
• Sipser, Michael. (2006). Introducción a la teoría de la computación. Boston: Thomson Course Technology.
• Zhang, Lintao. (2003). En busca de la verdad: Técnicas para la satisfacibilidad de fórmulas booleanas . Recuperado el 10 de octubre de 2005.

• Teorema de Cook-Levin , que establece que SAT es NP-completo.
• Geografía generalizada

• La biblioteca de fórmulas booleanas cuantificadas (QBFLIB)
• Taller internacional sobre fórmulas booleanas cuantificadas