真の量化ブール式

計算複雑性理論において、言語TQBF は、真の量化ブール式からなる形式言語です。完全量化ブール式とは、量化命題論理（二階命題論理とも呼ばれる）の式で、文の冒頭で、すべての変数が存在量化子または全称量化子を用いて量化（または束縛）されているものです。このような式は、（自由変数がないため）真または偽のいずれかに等価です。このような式が真と評価される場合、その式は言語 TQBF に属します。これはQSAT（量化SAT ）とも呼ばれます。

計算複雑性理論において、量化ブール式問題（QBF ）は、存在量化子と全称量化子の両方を各変数に適用できるブール充足可能性問題の一般化です。言い換えれば、ブール変数の集合に対する量化された文形式が真か偽かを問う問題です。例えば、以下はQBFの例です。

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

QBF は、多項式空間と無制限の時間で決定論的または非決定論的なチューリング マシンによって解ける問題のクラスであるPSPACEの標準的な完全問題です。 ^{[ 1 ]}抽象構文木の形式で式が与えられた場合、この問題は、式を評価する相互再帰的な手順のセットによって簡単に解くことができます。このようなアルゴリズムは、最悪の場合には線形である木の高さに比例する空間を使用しますが、量化子の数に対して指数関数的な時間を使用します。

MA ⊊ PSPACE が広く信じられているように、QBF は決定論的多項式時間でも確率的多項式時間でも解くことができず、与えられた解を検証することさえできません (実際、充足可能性問題とは異なり、解を簡潔に指定する方法は知られていません)。AP = PSPACEであるため、交代チューリングマシンを使用して線形時間で解くことができます。ここで、 APは交代マシンが多項式時間で解くことができる問題のクラスです。^{[ 2 ]}

画期的な結果IP = PSPACE が示されたとき（対話型証明システムを参照）、それは問題の特定の算術化を解くことによって QBF を解くことができる対話型証明システムを示すことによって行われた。^{[ 3 ]}

QBF式には、有用な標準形がいくつか存在します。例えば、すべての量化子を式の先頭に移動させ、全称量化子と存在量化子を交互に配置する多項式時間多対一還元が存在することが示されています。また、IP = PSPACEの証明で有用であることが証明された別の還元では、各変数の使用箇所と、その変数を束縛する量化子の間に、全称量化子を1つだけ配置します。これは、算術演算の特定の部分式における積の数を制限する上で非常に重要でした。

完全量化ブール式は、プレネックス正規形と呼ばれる非常に特定の形式を持つと想定できます。これは、量化子のみを含む部分と、通常 で表される非量化ブール式を含む部分の 2 つの基本部分から構成されます。${\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})}$

すべての変数が何らかの量化子の範囲内にある場合。ダミー変数を導入することで、前置正規形の任意の式を、存在量化子と全称量化子が交互に現れる文に変換できます。ダミー変数を使用する${\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})}$

2番目の文は同じ真理値を持つが、制限された構文に従っている。完全量化ブール式が前置標準形であると仮定することは、証明においてよく見られる特徴である。

QBFソルバーは、（人工知能における）安全計画を含む計画に適用できます。後者はロボット工学の応用において重要です。^{[ 14 ]} QBFソルバーは、SATベースのソルバーに必要なエンコーディングよりも短いため、境界付きモデル検査にも適用できます。 ^{[ 14 ]}

QBFの評価は、存在量化変数を制御するプレイヤーと全称量化変数を制御するプレイヤー間の2人対戦ゲームと見なすことができます。このため、QBFは反応合成問題をエンコードするのに適しています。^{[ 14 ]}同様に、QBFソルバーはゲーム理論における敵対的ゲームをモデル化するために使用できます。たとえば、QBFソルバーを使用して地理ゲームの勝利戦略を見つけることができ、その後、対話的に自動的にプレイできます。^{[ 15 ]}

QBFソルバーは形式的等価性チェックに使用でき、ブール関数の合成にも使用できます。^{[ 14 ]}

QBFとしてエンコードできるその他の問題の種類には、以下のようなものがあります。

• 連言標準形の不充足式の節が最小不充足部分集合に属するかどうか^{[ 9 ] [ 16 ]}、および充足式中の節が最大充足部分集合に属するかどうかを検出する^{[ 16 ]。}
• 適合計画の符号化^{[ 9 ]}
• ASP関連の問題^{[ 9 ]}
• 抽象的議論^{[ 9 ]}
• 線形時相論理モデル検査^{[ 9 ]}
• 非決定性有限オートマトン言語の包含^{[ 9 ]}
• 分散システムの合成と信頼性^{[ 9 ]}

確率的充足可能性問題（SSATとして知られる）は、ランダム化R量化子を追加し、全称量化を最小化、存在量化を最大化とみなし、式で表される確率が与えられた閾値を超えるかどうかを問うTQBFの拡張である。^{[ 17 ]}

QBFはヘンキン量化子を持つように拡張することもできます。^{[ 8 ]}

TQBF 言語は、複雑性理論において、標準的なPSPACE 完全問題として扱われます。PSPACE 完全であるということは、言語が PSPACE に属し、かつPSPACE 困難であることを意味します。上記のアルゴリズムは、TQBF が PSPACE に属することを示しています。TQBF が PSPACE 困難であることを示すには、複雑性クラス PSPACE に属する任意の言語が多項式時間で TQBF に還元できることを示す必要があります。つまり、

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

これは、PSPACE言語Lの場合、入力xがLに含まれるかどうかは、${\displaystyle f(x)}$TQBF には、入力の長さに対して多項式時間で実行する必要がある関数f が含まれています。記号的には、

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

TQBFがPSPACE困難であることを証明するには、fの指定が必要です。

そこで、LがPSPACE言語であると仮定します。これは、Lが多項式空間決定性チューリングマシン（DTM）によって決定可能であることを意味します。これは、LをTQBFに還元する上で非常に重要です。なぜなら、そのようなチューリングマシンの構成はブール式で表現でき、ブール変数はマシンの状態とチューリングマシンテープ上の各セルの内容を表し、チューリングマシンのヘッドの位置は式の順序によって式に符号化されるからです。特に、私たちの還元では、変数を使用します。${\displaystyle c_{1}}$そして${\displaystyle c_{2}}$これは、L の DTM の 2 つの可能な構成を表し、自然数t は QBF を構築します。${\displaystyle \phi _{c_{1},c_{2},t}}$これは、L の DTM がエンコードされた構成から変更できる場合に限り真である。${\displaystyle c_{1}}$エンコードされた構成へ${\displaystyle c_{2}}$t ステップ以内で。関数fは、L の DTM から QBF を構築します。${\displaystyle \phi _{c_{\text{start}},c_{\text{accept}},T}}$、 どこ${\displaystyle c_{start}}$これはDTMの初期構成です。${\displaystyle c_{\text{accept}}}$は DTM の受理構成であり、T は DTM がある構成から別の構成へ移動するために必要な最大ステップ数です。T = O (exp( n k )) となることがわかっています。ここでnは入力の^長さです。これは、関連する DTM の可能な構成の総数を制限するからです。もちろん、DTM が到達可能な構成の数を超えるステップ数を必要とすることはありません。${\displaystyle c_{\mathrm {accept} }}$ループに入らない限り、到達することはありません${\displaystyle c_{\mathrm {accept} }}$ともかく。

証明のこの段階で、入力式w (もちろんエンコードされている) が${\displaystyle c_{\text{start}}}$) は、QBF が${\displaystyle \phi _{c_{\text{start}},c_{\text{accept}},T}}$つまり、${\displaystyle f(w)}$はTQBFに含まれる。この証明の残りの部分は、fが多項式時間で計算できることを証明する。

のために${\displaystyle t=1}$計算${\displaystyle \phi _{c_{1},c_{2},t}}$これは単純明快です。一方の構成が他方の構成に1ステップで変化するか、変化しないかのどちらかです。私たちの式が表すチューリングマシンは決定論的であるため、これは問題になりません。

のために${\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 }).}$

これは、${\displaystyle c_{1}}$到達できる${\displaystyle c_{2}}$t のステップで、${\displaystyle c_{1}}$中間点に達する${\displaystyle m_{1}}$で${\displaystyle t/2}$階段、それ自体が到達する${\displaystyle c_{2}}$で${\displaystyle t/2}$手順。後者の質問への答えは、もちろん前者の質問への答えにもなります。

ここで、t は T によってのみ制限されますが、T は入力の長さに対して指数関数的（したがって多項式ではない）です。さらに、各再帰層は、式の長さを実質的に2倍にします。（変数${\displaystyle m_{1}}$（これは中間点の 1 つにすぎません。t が大きいほど、途中に停車する場所が増える、と言ってもよいでしょう。）したがって、再帰的に評価するのに必要な時間は${\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 }).}$

この式のバージョンは、実際には多項式時間で計算できます。なぜなら、そのどのインスタンスも多項式時間で計算できるからです。全称量化された順序対は、どの選択でも、${\displaystyle (c_{3},c_{4})}$作られる、${\displaystyle \phi _{c_{1},c_{2},t}\iff \phi _{c_{3},c_{4},\lceil t/2\rceil }}$。

したがって、${\displaystyle \forall L\in {\mathsf {PSPACE}},L\leq _{p}\mathrm {TQBF} }$したがって、TQBFはPSPACE困難である。TQBFがPSPACEに属するという上記の結果と合わせると、TQBFがPSPACE完全言語であることの証明が完了する。

（この証明は、Sipser 2006 pp.  310–313 にほぼ準拠している。Papadimitriou 1994 にも証明が掲載されている。）

この構成は対数空間で実行できるため、TQBF は対数空間多対一還元という意味で PSPACE 完全である。^{[ 18 ]}

• TQBFにおける重要な副問題の1つは、ブール充足可能性問題です。この問題では、与えられたブール式が充足可能かどうかを知りたいと考えます。${\displaystyle \phi }$変数の割り当てによって、これは真となる。これは、存在量化子のみを使用したTQBFと同等である。$${\displaystyle \exists x_{1}\cdots \exists x_{n}\phi (x_{1},\ldots ,x_{n})}$$これは、より大きな結果 NP ⊆ PSPACE の一例でもあり、これは、NTM (非決定性チューリングマシン)によって受理される言語の証明に対する多項式時間検証器が、証明を格納するために多項式空間を必要とするという観察から直接導かれるものです。
• 多項式階層( PH )のどのクラスもTQBF が困難な問題です。言い換えれば、すべての入力 x とある定数 i に対して、多項式時間 TM V と検証器が存在するすべての言語 L のクラスでは、$${\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}$$特定のQBF式が与えられており、それは次のように表される。$${\displaystyle \exists \phi }$$ そのため${\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}}}}$はブール変数のベクトルです。
• TQBFという言語は真の量化ブール式の集合として定義されていますが、略語TQBFは（この記事でも）完全に量化されたブール式、つまり単にQBF（量化ブール式、つまり「完全に」または「完全に」量化された式）を表すためによく使われることに注意が必要です。文献を読む際には、TQBFという略語の2つの使い方を文脈に応じて区別することが重要です。
• TQBFは、2人のプレイヤーが交互に手番を行うゲームと考えることができます。存在量化変数は、プレイヤーがターンごとに手を打つことができるという概念と同等です。全称量化変数は、ゲームの結果がそのターンにおけるプレイヤーの手番の行動に依存しないことを意味します。また、最初の量化子が存在量化であるTQBFは、先手プレイヤーが必勝戦略を持つ数式ゲームに対応します。
• 量化式が2-CNFである TQBF は、その含意グラフの強力な連結性解析を含むアルゴリズムによって線形時間で解くことができます。2-充足可能性問題は、すべての量化子が存在量化子であるこれらの式の TQBF の特殊なケースです。^{[ 19 ] [ 20 ]}
• Hubie Chenによる解説論文では、量化ブール式の制限付きバージョン（シェーファー型分類を与える）の体系的な扱いが提供されています。^{[ 21 ]}
• 平面SATを一般化した平面TQBFは、D. LichtensteinによってPSPACE完全であることが証明された。^{[ 22 ]}

• Fortnow & Homer (2003) は、PSPACE と TQBF の歴史的背景についていくつか述べている。
• Zhang（2003）はブール式の歴史的背景について述べている。
• Arora, Sanjeev. (2001). COS 522: 計算複雑性. 講義ノート、プリンストン大学。2005年10月10日取得。
• Fortnow, Lance & Steve Homer. (2003年6月). 計算複雑性の短い歴史. 欧州理論計算機科学協会紀要、計算複雑性コラム、80. 2024年5月14日取得。
• Papadimitriou, CH (1994). 計算複雑性。Reading : Addison-Wesley.
• Sipser, Michael. (2006). 計算理論入門. ボストン: Thomson Course Technology.
• 張林濤 (2003). 真理の探求：ブール式の充足可能性の手法. 2005年10月10日取得。

• クック・レヴィン定理は、SATがNP完全であることを述べている。
• 一般地理学

• 定量化ブール式ライブラリ（QBFLIB）
• 量化ブール式に関する国際ワークショップ