Editing Cook–Levin theorem (section)

==Complexity==
While the above method encodes a non-deterministic Turing machine in complexity <math>O(\log(p(n))p(n)^3)</math>, the literature describes more sophisticated approaches in complexity <math>O(p(n)\log(p(n)))</math>.<ref>{{cite journal | url=https://www.ccs.neu.edu/home/viola/classes/papers/Schnorr-SatNQL.pdf | author=Claus-Peter Schnorr | title=Satisfiability is quasilinear complete in NQL | journal=Journal of the ACM | volume=25 | number=1 | pages=136&ndash;145 | date=Jan 1978 | doi=10.1145/322047.322060 | s2cid=1929802 }}</ref><ref>{{cite journal | url=https://www.ccs.neu.edu/home/viola/classes/papers/PippengerF-Oblivious.pdf | author=Nicholas Pippenger and Michael J. Fischer | title=Relations among complexity measures | journal=Journal of the ACM | volume=26 | number=2 | pages=361&ndash;381 | date=Apr 1979 | doi=10.1145/322123.322138 | s2cid=2432526 }}</ref><ref>{{cite conference | url= | author=John Michael Robson | title=A new proof of the NP completeness of satisfiability | editor= | work=Proceedings of the 2nd Australian Computer Science Conference | publisher= | pages=62–70 | date=Feb 1979 }}</ref><ref>{{cite journal | author=John Michael Robson | title=An <math>O(T \log T)</math> reduction from RAM computations to satisfiability | journal=Theoretical Computer Science | volume=82 | number=1 | pages=141&ndash;149 | date=May 1991 | doi=10.1016/0304-3975(91)90177-4 | doi-access=free }}</ref><ref>{{cite journal | url=https://www.ccs.neu.edu/home/viola/classes/papers/Cook1988.pdf | author=Stephen A. Cook | title=Short propositional formulas represent nondeterministic computations | journal=Information Processing Letters | volume=26 | number=5 | pages=269&ndash;270 | date=Jan 1988 | doi=10.1016/0020-0190(88)90152-4 }}</ref> The quasilinear result first appeared seven years after Cook's original publication.

The use of SAT to prove the existence of an NP-complete problem can be extended to other computational problems in logic, and to completeness for other [[complexity class]]es.
The [[quantified Boolean formula]] problem (QBF) involves Boolean formulas extended to include nested [[universal quantifier]]s and [[existential quantifier]]s for its variables. The QBF problem can be used to encode computation with a Turing machine limited to [[PSPACE|polynomial space complexity]], proving that there exists a problem (the recognition of true quantified Boolean formulas) that is [[PSPACE-complete]]. Analogously, dependency quantified boolean formulas encode computation with a Turing machine limited to [[NL (complexity)|logarithmic space complexity]], proving that there exists a problem that is [[NL-complete]].<ref>{{cite conference | url=https://ieeexplore.ieee.org/document/4568030 | author1=Gary L. Peterson |author2= John H. Reif | title=Multiple-person alternation | editor1=Ronald V. Book |editor2= Paul Young | book-title=Proc. 20th Annual [[Symposium on Foundations of Computer Science]] (SFCS) | publisher=IEEE | pages=348–363 |  year=1979 }}</ref><ref>{{cite journal | author1=Gary Peterson |author2= John Reif |author3= Salman Azhar | title=Lower bounds for multiplayer noncooperative games of incomplete information | journal=Computers & Mathematics with Applications | volume=41 | number=7&ndash;8 | pages=957&ndash;992 | date=Apr 2001 | doi=10.1016/S0898-1221(00)00333-3 | doi-access=free }}</ref>