真定量ブール式

計算複雑性理論において、言語TQBF は、真量化ブール式で構成される形式言語です。（完全に）量化ブール式は、量化命題論理（第二階命題論理とも呼ばれる）における式であり、文の先頭で存在量指定子または全称量指定子を使用して、すべての変数が量化（またはバインド）されます。このような式は、真または偽のいずれかに相当します（自由変数がないため）。このような式が真と評価される場合、その式は言語 TQBF です。これはQSAT（量化SAT） とも呼ばれます。

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

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

QBFはPSPACEの標準的な完全問題であり、 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がTQBFであるかどうか（つまり真であるかどうか）を判断するための単純な再帰アルゴリズムがある。あるQBFが与えられたとき

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

数式に量指定子が含まれていない場合は、数式をそのまま返すことができます。それ以外の場合は、最初の量指定子を削除し、最初の変数の両方の可能な値を確認します。

${\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}).}$

の場合、 を返します。 の場合、 を返します。^[4]${\displaystyle Q_{1}=\exists }$${\displaystyle A\or B}$${\displaystyle Q_{1}=\forall }$${\displaystyle A\land B}$

このアルゴリズムはどのくらい速く実行されるでしょうか? 初期 QBF のすべての量指定子に対して、アルゴリズムは線形に小さいサブ問題に対してのみ 2 回の再帰呼び出しを行います。これにより、アルゴリズムの実行時間は指数関数的にO(2 ⁿ )になります。^{[引用が必要]}

このアルゴリズムはどのくらいのスペースを使用するのでしょうか。アルゴリズムの各呼び出し内で、A と B の計算の中間結果を保存する必要があります。再帰呼び出しごとに 1 つの量指定子が取り出されるため、再帰の深さの合計は量指定子の数に比例します。量指定子のない式は、変数の数の対数スペースで評価できます。初期の QBF は完全に量指定されているため、少なくとも変数と同じ数の量指定子があります。したがって、このアルゴリズムはO ( n + log n ) = O ( n ) のスペースを使用します。これにより、TQBF 言語はPSPACE 複雑性クラスの一部になります。^{[引用が必要]}

QBF は PSPACE 完全であるにもかかわらず、これらの例を解くためのソルバーが数多く開発されてきた。(これは、単一存在量指定子バージョンであるSATの場合と類似している。NP完全であるにもかかわらず、多くの SAT 例をヒューリスティックに解くことは可能である。) ^{[5] [6]}量指定子が 2 つしかない場合 (2QBF と呼ばれる) は、特に注目されている。^{[7] [ウイズルワード]}

QBFソルバーのコンペティションQBFEVALは、2004年以来、ほぼ毎年開催されています。^{[5] [6]}ソルバーは、QDIMACS形式と、QCIRまたはQAIGER形式のいずれかのインスタンスを読み込む必要があります。^[8]高性能なQBFソルバーは、通常、QDPLL（DPLLの一般化）またはCEGARを使用します。^{[5] [6] [7]} QBF解決の研究は、1998年にQBF用のバックトラッキングDPLLの開発から始まり、その後、2002年に節学習と変数除去が導入されました。^[9]そのため、1960年代から開発が進められているSAT解決と比較すると、QBFは2017年時点では比較的新しい研究分野です。^{[9] [ウイーゼルワード]}

著名な QBF ソルバーには次のようなものがあります。

• CADETは、増分決定論^{[説明が必要]}に基づいて、 1つの量指定子の交替に制限された量指定ブール式を解き、その答えを証明する機能を備えています（スコーレム関数を計算する機能を備えています）。 ^[10]
• CAQE - 定量化されたブール式のためのCEGARベースのソルバー。最近のQBFEVALの優勝者。^[11]
• DepQBF - 定量化されたブール式のための検索ベースのソルバー^[12]
• sKizzo - シンボリックスコレム化を使用し、充足可能性の証明書を抽出し、ハイブリッド推論エンジンを使用し、抽象分岐を実装し、限定された量指定子を扱い、有効な割り当てを列挙する最初のソルバーであり、QBFEVAL 2005、2006、2007の優勝者です。^[13]

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] [説明が必要]}

QBFEVAL 2020では、「DQBFトラック」が導入され、インスタンスにHenkin量指定子（DQDIMACS形式で表される）を持たせることができるようになりました。^[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に含まれるかどうかは、多項式時間（入力の長さに対して）で実行する必要がある関数fに対して、TQBFに含まれるかどうかをチェックすることで決定できることを意味します。記号的に言えば、 ${\displaystyle f(x)}$

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

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

そこで、L が PSPACE 言語であると仮定します。これは、L が多項式空間決定論的チューリングマシン(DTM) によって決定できることを意味します。これは、L を TQBF に縮小する上で非常に重要です。なぜなら、そのようなチューリングマシンの構成はブール式として表すことができ、ブール変数はマシンの状態とチューリングマシン テープ上の各セルの内容を表し、チューリングマシン ヘッドの位置は式の順序によって式にエンコードされるからです。特に、この縮小では、L の DTM の 2 つの可能な構成を表す変数と、自然数 t を使用して、 L の DTM が でエンコードされた構成から でエンコードされた構成にt ステップ以内で移行できる場合にのみ真となるQBF を構築します。すると、関数f は、 L の DTM から QBF を構築します。ここで、は DTM の開始構成、 はDTM の受け入れ構成、 T は DTM が 1 つの構成から別の構成に移動するために必要な最大ステップ数です。あるkに対してT = O (exp( n ^k )) であることがわかっています。ここでnは入力の長さです。これは、関連する DTM の可能な構成の総数を制限しているためです。もちろん、ループに入らない限り、DTM が到達可能な構成よりも多くのステップを実行することはできません。ループに入った場合は、いずれにしても到達することはありません。 ${\displaystyle c_{1}}$${\displaystyle c_{2}}$${\displaystyle \phi _{c_{1},c_{2},t}}$${\displaystyle c_{1}}$${\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} }}$

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

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

の場合、 の計算には再帰評価が含まれ、いわゆる「中間点」が探されます。 この場合、式を次のように書き直します。 ${\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 }).}$

これは、t ステップで到達できるかどうかという質問を、それ自体がステップで到達する中間点にステップで到達できるかどうかという質問に変換します。後者の質問の答えは、もちろん前者の質問の答えになります。 ${\displaystyle c_{1}}$${\displaystyle c_{2}}$${\displaystyle c_{1}}$${\displaystyle m_{1}}$${\displaystyle t/2}$${\displaystyle c_{2}}$${\displaystyle t/2}$

ここで、t は T によってのみ制限され、T は入力の長さに対して指数的（したがって多項式ではない）です。さらに、各再帰層は実質的に式の長さを 2 倍にします。（変数は中間点の 1 つにすぎません。t が大きいほど、いわば途中で停止する場所が増えます。）したがって、この方法で再帰的に評価するために必要な時間も指数的になる可能性があります。これは、式が指数的に大きくなる可能性があるためです。この問題は、変数と構成ペア（たとえば、 ）を使用して普遍的に量化することで解決します。これにより、再帰層によって式の長さが拡大するのを防ぎます。これにより、 は次のように解釈されます。 ${\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 }).}$

このバージョンの式は、そのインスタンスの 1 つが多項式時間で計算できるため、実際に多項式時間で計算できます。普遍的に量化された順序付きペアは、 のどちらを選択しても、 であることを示しています。 ${\displaystyle (c_{3},c_{4})}$${\displaystyle \phi _{c_{1},c_{2},t}\iff \phi _{c_{3},c_{4},\lceil t/2\rceil }}$

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

(この証明は、Sipser 2006 pp. 310–313 にすべて準拠しています。Papadimitriou 1994 にも証明が含まれています。)

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

• Fortnow & Homer (2003) は、PSPACE と TQBF の歴史的背景について説明しています。
• Zhang (2003) はブール式の歴史的背景を説明しています。
• Arora, Sanjeev. (2001). COS 522: 計算複雑性。講義ノート、プリンストン大学。2005 年 10 月 10 日閲覧。
• ランス・フォートナウ & スティーブ・ホーマー (2003 年 6 月)。計算複雑性の短い歴史。 欧州理論計算機科学協会紀要、計算複雑性コラム、80。2024 年 5 月 14 日閲覧。
• Papadimitriou, CH (1994). 計算複雑性. 参考文献: Addison-Wesley.
• Sipser, Michael. (2006). 計算理論入門. ボストン: Thomson Course Technology.
• Zhang, Lintao. (2003). 真実の探求: ブール式の充足可能性のためのテクニック。2005 年 10 月 10 日閲覧。

• クック・レビン定理、SATはNP完全であると述べる
• 一般地理

• 定量化ブール式ライブラリ (QBFLIB)
• 定量化されたブール式に関する国際ワークショップ