TQBF問題

計算複雑性理論において、言語TQBFは量化された真のブール式からなる形式言語である。(完全に)量化されたブール式とは、すべての変数が存在量化子や全称量化子を用いて式の先頭で量化(束縛)された限定命題論理の式である。自由変数が存在しないため、そのような式は真あるいは偽と同値である。もし真と同値ならば、その式は言語TQBFの要素である。この言語はQSAT(量化されたSAT, Quantified SAT)としても知られている。

概要

計算複雑性理論において、量化されたブール式問題(QBF)は充足可能性問題の一般化であり、変数を存在量化子でも全称量化子でも量化することができる。言い換えると、QBFはブール変数の集合の上の量化された式が真か偽かを問うものである。例えば、以下の式はQBFのインスタンスである:

$\forall x\ \exists y\ \exists z\ ((x\lor z)\land y)$

QBFは標準的なPSPACE完全問題である。PSPACEは決定性、あるいは非決定性チューリングマシンで多項式領域および無制限の時間で解ける問題のクラスである。 式を抽象構文木の形で与えれば、この問題は式を評価するような再帰的な手続きによって簡単に解くことができる。このアルゴリズムの領域計算量は木の高さに比例し、最悪ケースでは線型であるが、時間計算量は量化子の個数に関する指数である。

広く信じられている MA ⊊ PSPACEという仮定の下で、QBFは決定性チューリングマシンでも確率的チューリングマシンでも、多項式時間では解くことも与えられた解を検証することもできない。実際、充足可能性問題とは異なり、解を簡潔に指定する方法は知られていない。交代チューリングマシンを使えば線型時間で自明に解けるが、AP = PSPACEなのでこれは当然である(APは交代チューリングマシンで多項式時間で解ける問題の集合)。

独創的な結果IP = PSPACE(参考:対話型証明系)が示されたとき、その証明はQBFを解くことのできる対話型証明系を示すことで行われた。

QBFの式にはたくさんの有用な標準形が存在する。例えば、すべての量化子を式の先頭に移動するような多項式時間多対一帰着が存在することが示せる。さらに別の有用な帰着も存在する。それは各変数の使用とその量化子による束縛の間には高々1つの全称量化子しか存在しないような論理式への帰着であり、IP = PSPACEの証明で用いられた。 QBF formulas have a number of useful canonical forms. For example, it can be shown that there is a polynomial-time many-one reduction that will move all quantifiers to the front of the formula and make them alternate between universal and existential quantifiers. There is another reduction that proved useful in the IP = PSPACE proof where no more than one universal quantifier is placed between each variable's use and the quantifier binding that variable. This was critical in limiting the number of products in certain subexpressions of the arithmetization.