Fórmula booleana cuantificada verdadera

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 la 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).

Visión general

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:

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

QBF es el problema canónico completo de PSPACE , la clase de problemas que puede resolver una máquina de Turing determinista o no determinista en un espacio polinomial y 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 hay forma conocida de especificar una solución sucintamente ). 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 de varios 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.

Prenex forma normal

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

${\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. Mediante la introducción de variables ficticias, cualquier fórmula en forma normal prenex se puede convertir en una oración en la que 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. Asumir que las fórmulas booleanas totalmente cuantificadas están en forma normal prenex es una característica frecuente de las demostraciones.

Solucionadores QBF

Ingenuo

Es posible que esta sección contenga investigaciones originales . Por favor, mejorarlo mediante la verificación de las afirmaciones hechas y la adición de citas en línea . Deben eliminarse las declaraciones que solo contengan investigaciones originales. ( Mayo de 2021 ) ( Obtenga información sobre cómo y cuándo eliminar este mensaje de plantilla )

Existe un algoritmo recursivo simple para determinar si un QBF está en TQBF (es decir, es verdadero). Dado algo de QBF

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

Si la fórmula no contiene cuantificadores, podemos simplemente devolver la fórmula. De lo contrario, quitamos el primer cuantificador y comprobamos los dos valores posibles para la primera variable:

${\displaystyle A=Q_{2}x_{2}\cdots Q_{n}x_{n}\phi (0,x_{2},\dots ,x_{n}),}$

${\displaystyle B=Q_{2}x_{2}\cdots Q_{n}x_{n}\phi (1,x_{2},\dots ,x_{n}).}$

Si , entonces regresa . Si , entonces regresa . ^[4]${\displaystyle Q_{1}=\exists }$${\displaystyle A\lor B}$${\displaystyle Q_{1}=\forall }$${\displaystyle A\land B}$

¿Qué tan rápido se ejecuta este algoritmo? Para cada cuantificador en el QBF inicial, el algoritmo realiza dos llamadas recursivas solo en un subproblema linealmente más pequeño. Esto le da al algoritmo un tiempo de ejecución exponencial O (2 n ) . ^{[ cita requerida ]}

¿Cuánto espacio usa este algoritmo? Dentro de cada invocación del algoritmo, necesita almacenar los resultados intermedios de calcular A y B. Cada llamada recursiva quita un cuantificador, por lo que la profundidad recursiva total es lineal en el número de cuantificadores. Las fórmulas que carecen de cuantificadores se pueden evaluar en espacio logarítmico en el número de variables. El QBF inicial se cuantificó por completo, por lo que hay al menos tantos cuantificadores como variables. Por lo tanto, este algoritmo usa el espacio O ( n + log n ) = O ( n ). Esto hace que el lenguaje TQBF forme parte de la clase de complejidad PSPACE . ^{[ cita requerida ]}

Lo último

Esta sección necesita expansión . Puede ayudar añadiéndole . ( Mayo de 2021 )

A pesar de la integridad PSPACE de QBF, se han desarrollado muchos solucionadores para resolver estos casos. (Esto es análogo a la situación con SAT , la versión de cuantificador existencial único; aunque es NP-completo , todavía es posible resolver muchas instancias de SAT de forma heurística). ^{[5] [6]} El caso donde solo hay 2 cuantificadores , conocido como 2QBF, ha recibido una atención especial. ^{[7] [ palabras de comadreja ]}

El concurso de solucionadores QBF QBFEVAL se ha estado ejecutando más o menos anualmente desde 2004; ^{[5] [6] Los} solucionadores deben leer instancias en formato QDIMACS y en los formatos QCIR o QAIGER. ^[8] Los solucionadores de QBF de alto rendimiento generalmente usan QDPLL (una generalización de DPLL ) o CEGAR. ^{[5] [6] [7] La} investigación sobre la resolución de QBF comenzó con el desarrollo de DPLL con retroceso para QBF en 1998, seguido de la introducción del aprendizaje de cláusulas y la eliminación de variables en 2002; ^{[9] por lo} tanto, en comparación con la resolución SAT, que ha estado en desarrollo desde la década de 1960, QBF es un campo de investigación relativamente joven a partir de 2017. ^{[9] [ palabras de comadreja ]}

Algunos solucionadores QBF destacados incluyen:

• CADET, que resuelve fórmulas booleanas cuantificadas restringidas a la alternancia de un cuantificador (con la capacidad de calcular funciones de Skolem ), basadas en la determinación incremental ^{[ aclaración necesaria ]} y con la capacidad de probar sus respuestas. ^[10]
• CAQE: un solucionador basado en CEGAR para fórmulas booleanas cuantificadas; ganador de las últimas ediciones de QBFEVAL. ^[11]
• DepQBF: un solucionador basado en búsquedas para fórmulas booleanas cuantificadas ^[12]
• sKizzo: el primer solucionador en usar skolemization simbólico, extraer certificados de satisfacibilidad, usar un motor de inferencia híbrido, implementar ramificaciones abstractas, lidiar con cuantificadores limitados y enumerar asignaciones válidas, y ganador de QBFEVAL 2005, 2006 y 2007. ^[13]

Aplicaciones

Esta sección necesita expansión . Puede ayudar añadiéndole . ( Mayo de 2021 )

Los solucionadores de QBF se pueden aplicar a la planificación (en inteligencia artificial), incluida la planificación segura; este último es crítico 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 verse como 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 se pueden usar para modelar juegos adversarios en la teoría de juegos . Por ejemplo, los solucionadores de QBF se pueden utilizar para encontrar estrategias ganadoras para juegos de geografía , que luego se pueden jugar automáticamente de forma interactiva. ^[15]

Los solucionadores de QBF se pueden usar para la verificación de equivalencia formal y también se pueden usar para sintetizar funciones booleanas. ^[14]

Otros tipos de problemas que se pueden codificar como QBF incluyen:

• Detectar si una cláusula en una fórmula no satisfactoria en forma conjuntiva normal pertenece a algún subconjunto mínimamente insatisfactorio ^{[9] [16]} y si una cláusula en una fórmula satisfactoria pertenece a un subconjunto máximamente satisfactorio ^[16]
• Codificaciones de planificación conforme ^{[9] [ aclaración necesaria ]}
• Problemas relacionados con ASP ^{[9] [ aclaración necesaria ]}
• Argumentación abstracta ^{[9] [ aclaración necesaria ]}
• Comprobación del modelo de lógica temporal lineal ^{[9] [ aclaración necesaria ]}
• Inclusión de lenguaje autómata finito no determinista ^{[9] [ aclaración necesaria ]}
• Síntesis y fiabilidad de los sistemas distribuidos ^{[9] [ aclaración necesaria ]}

Extensiones

En QBFEVAL 2020, se introdujo una "pista DQBF" en la que se permitía que las instancias tuvieran cuantificadores de Henkin (expresados ​​en formato DQDIMACS). ^[8]

Completitud de PSPACE

El lenguaje TQBF sirve en la teoría de la complejidad como el problema canónico completo de PSPACE . Ser PSPACE-completo significa que un idioma está en PSPACE y que el idioma también es PSPACE-hard . El algoritmo anterior muestra que TQBF está en PSPACE. Mostrar que TQBF es PSPACE-hard requiere mostrar 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, si una entrada x está en L puede decidirse verificando si está en TQBF, para alguna función f que se requiere que se ejecute en tiempo polinomial (en relación con la longitud de la entrada). Simbólicamente,${\displaystyle f(x)}$

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

Demostrar que TQBF es PSPACE-hard, requiere la especificación de f .

Entonces, suponga que L es un lenguaje PSPACE. Esto significa que L puede decidirse mediante una máquina de Turing determinista del espacio polinómico (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 se pueden representar 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 de la cabeza de la máquina de Turing codificada en la fórmula por el orden de la fórmula. En particular, nuestra reducción utilizará las variables y , que representan dos configuraciones posibles del DTM para L, y un número natural t, en la construcción de un QBF que es verdadero si y solo si el DTM para L puede ir de la configuración codificada en${\displaystyle c_{1}}$${\displaystyle c_{2}}$${\displaystyle \phi _{c_{1},c_{2},t}}$${\displaystyle c_{1}}$a la configuración codificada en no más de t pasos. La función f , entonces, se construirá a partir del DTM para L a QBF , donde es la configuración inicial del DTM, 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 la otra. Sabemos que T = O (exp ( n )) , donde n es la longitud de la entrada, porque limita el número total de configuraciones posibles del DTM relevante. Por supuesto, no puede dar al DTM más pasos de los que existen posibles configuraciones para alcanzar a menos que entre en un bucle, en cuyo caso nunca llegará de todos modos.${\displaystyle c_{2}}$${\displaystyle \phi _{c_{\text{start}},c_{\text{accept}},T}}$${\displaystyle c_{start}}$${\displaystyle c_{\text{accept}}}$${\displaystyle c_{\mathrm {accept} }}$${\displaystyle c_{\mathrm {accept} }}$

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 ) está en L a la cuestión de si QBF , es decir , está en TQBF. El resto de esta demostración prueba que f se puede calcular en tiempo polinomial.${\displaystyle c_{\text{start}}}$${\displaystyle \phi _{c_{\text{start}},c_{\text{accept}},T}}$${\displaystyle f(w)}$

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

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

${\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 pregunta de si se puede llegar en t pasos a la pregunta de si llega a un punto medio en pasos, que a su vez llega en pasos. La respuesta a la última pregunta, por supuesto, da la respuesta a la primera.${\displaystyle c_{1}}$${\displaystyle c_{2}}$${\displaystyle c_{1}}$${\displaystyle m_{1}}$${\displaystyle t/2}$${\displaystyle c_{2}}$${\displaystyle t/2}$

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 es solo un punto medio; para t mayor, hay más paradas en el camino, por así decirlo). Por lo tanto, el tiempo requerido para evaluar de forma recursiva 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 y sobre los pares de configuración (por ejemplo, ), lo que evita que la longitud de la fórmula se expanda debido a capas recursivas. Esto produce la siguiente interpretación de :${\displaystyle m_{1}}$${\displaystyle \phi _{c_{1},c_{2},t}}$${\displaystyle c_{3}}$${\displaystyle c_{4}}$${\displaystyle \{(c_{1},m_{1}),(m_{1},c_{2})\}}$${\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 }).}$

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

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

(Esta prueba sigue a Sipser 2006 pp. 310-313 en todos los aspectos esenciales. Papadimitriou 1994 también incluye una prueba).

Miscelánea

• Un subproblema importante en TQBF es el problema de satisfacibilidad booleano . En este problema, desea saber si una fórmula booleana determinada se puede convertir en verdadera con alguna asignación de variables. Esto es equivalente al TQBF usando solo cuantificadores existenciales:${\displaystyle \phi }$
  $${\displaystyle \exists x_{1}\cdots \exists x_{n}\phi (x_{1},\ldots ,x_{n})}$$
  Este es también un ejemplo del resultado más grande 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 que existe una TM V politemporal, un verificador, tal que para toda la entrada xy 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 }$$
  tal que donde los 's son vectores de variables booleanas.${\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}$${\displaystyle {\vec {x_{i}}}}$
• Es importante señalar que mientras TQBF el lenguaje se define como la colección de fórmulas booleanas cuantificadas verdaderas, la abreviatura TQBF se usa a menudo (incluso en este artículo) para representar una fórmula booleana totalmente cuantificada, a menudo simplemente llamada QBF (booleana cuantificada fórmula, entendida como "total" o "totalmente" cuantificada). Es importante distinguir contextualmente entre los dos usos de la abreviatura TQBF al leer la literatura.
• Un TQBF se puede considerar como un juego entre dos jugadores, con movimientos alternos. Las variables cuantificadas existencialmente son equivalentes a la noción de que un jugador dispone de un movimiento en un turno. Las variables cuantificadas universalmente significan que el resultado del juego no depende del movimiento que haga un jugador en ese turno. Además, un TQBF cuyo primer cuantificador es existencial corresponde a un juego de fórmula en el que el primer jugador tiene una estrategia ganadora.
• Un TQBF para el que la fórmula cuantificada está en 2-CNF puede resolverse en tiempo lineal , mediante un algoritmo que implica un fuerte análisis de conectividad de su gráfico de implicaciones . El problema de 2-satisfacibilidad es un caso especial de TQBF para estas fórmulas, en las que cada cuantificador es existencial. ^{[17] [18]}
• Existe un tratamiento sistemático de versiones restringidas de fórmulas booleanas cuantificadas (que dan clasificaciones de tipo Schaefer) proporcionado en un artículo expositivo de Hubie Chen. ^[19]
• Planar TQBF, generalizando Planar SAT , fue probado PSPACE-completo por D. Lichtenstein. ^[20]

notas y referencias

1. M. Garey y D. Johnson (1979). Computadoras e intratabilidad: una guía para la teoría de NP-Completeness . WH Freeman, San Francisco, California. ISBN 0-7167-1045-5.
2. A. Chandra, D. Kozen y L. Stockmeyer (1981). "Alternancia" . Revista de la ACM . 28 (1): 114-133. doi : 10.1145 / 322234.322243 .
3. Adi Shamir (1992). "Ip = Pspace" . Revista de la ACM . 39 (4): 869–877. doi : 10.1145 / 146585.146609 . S2CID 315182 . 
4. Arora, Sanjeev; Barak, Boaz (2009), "Complejidad espacial" , Computational Complexity , Cambridge: Cambridge University Press, págs. 78–94, doi : 10.1017 / cbo9780511804090.007 , ISBN 978-0-511-80409-0, consultado el 26 de mayo de 2021
5. "Página de inicio de QBFEVAL" . www.qbflib.org . Consultado el 13 de febrero de 2021 .
6. "Solucionadores de QBF | Más allá de NP" . beyondnp.org . Consultado el 13 de febrero de 2021 .
7. Balabanov, Valeriy; Roland Jiang, Jie-Hong; Scholl, Christoph; Mishchenko, Alan; K. Brayton, Robert (2016). "2QBF: desafíos y soluciones" (PDF) . Conferencia internacional sobre teoría y aplicaciones de las pruebas de satisfacción : 453–459. Archivado (PDF) desde el original el 13 de febrero de 2021, a través de SpringerLink.
8. "QBFEVAL'20" . www.qbflib.org . Consultado el 29 de mayo de 2021 .
9. Lonsing, Florian (diciembre de 2017). "Introducción a la resolución de QBF" (PDF) . www.florianlonsing.com . Consultado el 29 de mayo de 2021 .
10. Rabe, Markus N. (15 de abril de 2021), MarkusRabe / cadet , consultado el 6 de mayo de 2021
11. Tentrup, Leander (2021-05-06), ltentrup / caqe , consultado 2021-05-06
12. "DepQBF Solver" . lonsing.github.io . Consultado el 6 de mayo de 2021 .
13. "sKizzo - un solucionador de QBF" . www.skizzo.site . Consultado el 6 de mayo de 2021 .
14. Shukla, Ankit; Biere, Armin; Seidl, Martina; Pulina, Luca (2019). Una encuesta sobre aplicaciones de fórmulas booleanas cuantificadas (PDF) . 2019 IEEE 31st International Conference on Tools for Artificial Intelligence. págs. 78–84. doi : 10.1109 / ICTAI.2019.00020 . Consultado el 29 de mayo de 2021 .
15. Shen, Zhihe. Uso de QBF Solvers para resolver juegos y acertijos (PDF) (Tesis). Boston College.
16. Janota, Mikoláš; Marques-Silva, Joao (2011). Sobre la decisión de ser miembro de MUS con QBF . Principios y práctica de la programación de restricciones - CP 2011. 6876 . págs. 414–428. doi : 10.1007 / 978-3-642-23786-7_32 . ISBN 978-3-642-23786-7.
17. Krom, Melven R. (1967). "El problema de decisión para una clase de fórmulas de primer orden en las que todas las disyunciones son binarias". Zeitschrift für Mathematische Logik und Grundlagen der Mathematik . 13 (1–2): 15–20. doi : 10.1002 / malq.19670130104 ..
18. Aspvall, Bengt; Plass, Michael F .; Tarjan, Robert E. (1979). "Un algoritmo de tiempo lineal para probar la verdad de ciertas fórmulas booleanas cuantificadas" (PDF) . Cartas de procesamiento de información . 8 (3): 121-123. doi : 10.1016 / 0020-0190 (79) 90002-4 . .
19. Chen, Hubie (diciembre de 2009). "Un encuentro de lógica, complejidad y álgebra". Encuestas de computación ACM . ACM. 42 (1): 1–32. arXiv : cs / 0611018 . doi : 10.1145 / 1592451.1592453 . S2CID 11975818 . 
20. Lichtenstein, David (1 de mayo de 1982). "Fórmulas planas y sus usos" . Revista SIAM de Computación . 11 (2): 329–343. doi : 10.1137 / 0211025 . ISSN 0097-5397 . 

• Fortnow y Homer (2003) proporcionan algunos antecedentes históricos para PSPACE y TQBF.
• Zhang (2003) proporciona algunos antecedentes históricos de las fórmulas booleanas.
• Arora, Sanjeev. (2001). COS 522: Complejidad computacional . Lecture Notes, Universidad de Princeton. Consultado el 10 de octubre de 2005.
• Fortnow, Lance y Steve Homer. (2003, junio). Una breve historia de la complejidad computacional . The Computational Complexity Column, 80. Consultado el 9 de octubre de 2005.
• Papadimitriou, CH (1994). Complejidad computacional. Lectura: Addison-Wesley.
• Sipser, Michael. (2006). Introducción a la Teoría de la Computación. Boston: Tecnología del curso Thomson.
• Zhang, Lintao. (2003). Buscando la verdad: Técnicas para la satisfacibilidad de fórmulas booleanas . Consultado el 10 de octubre de 2005.

Ver también

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

enlaces externos

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