[Resource Topic] 2022/929: PH = PSPACE

Welcome to the resource topic for 2022/929


Authors: Valerii Sopin


In this paper we show that PSPACE is equal to 4th level in the polynomial hierarchy. We also deduce a lot of important consequences. True quantified Boolean formula is indeed generalisation of the Boolean Satisfiability Problem, where determining of interpretation that satisfies a given Boolean formula is replaced by existence of Boolean functions that makes a given QBF to be tautology. Such functions are called the Skolem functions. The essential idea of the proof is to show that for any (fully) quantified Boolean formula ϕ we can obtain a formula ϕ′ which is in the forth level of the polynomial hierarchy, no more than polynomial in the size of a given ϕ, such that the truth of ϕ can be determined from the truth of ϕ′. The idea is to skolemize, and then use additional formulas from the second level of the polynomial hierarchy inside the skolemized prefix to enforce that the skolem variables indeed depend only on the universally quantified variables they are supposed to. However, some dependence is lost when the quantification is reversed. It is called “XOR issue” in the paper because the functional dependence can be expressed by means of an XOR formula. Thus, it is needed to locate these XORs. The last can be done locally for each leaf/ branch/ iteration (keep in mind the algebraic normal form (ANF)), i.e. in polynomial time, since all arguments are specified.

ePrint: https://eprint.iacr.org/2022/929

See all topics related to this paper.

Feel free to post resources that are related to this paper below.

Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.

For more information, see the rules for Resource Topics .