クールセルの定理

グラフアルゴリズムの研究において、クールセル定理は、グラフの単項二階論理で定義可能なすべてのグラフ特性は、有界木幅のグラフ上で線形時間で決定できるという定理である。^{[ 1 ] [ 2 ] [ 3 ]}この結果は、 1990 年にブルーノ・クールセルによって最初に証明され^{[ 4 ]} 、1992 年にボリー、パーカー、トビーによって独立に再発見された。^{[ 5 ]}これは、アルゴリズムのメタ定理 の原型と考えられている。^{[ 6 ] [ 7 ]}

クールセルの定理を証明する典型的な方法は、与えられたグラフの木分解に対して作用する有限ボトムアップ木オートマトンを構築することである。 ^{[ 6 ]}

より詳細には、それぞれ特定の部分集合Tの頂点（終端と呼ばれる）を持つ 2 つのグラフG ₁とG _{2は、MSO 式}Fに関して同等であると定義できます。これは、 G ₁とG ₂との交差がTの頂点のみで構成される他のすべてのグラフHについて、2 つのグラフ G ₁ ∪ HとG ₂ ∪ HがFに関して同じ挙動を示す場合です。つまり、両方ともFをモデル化するか、両方ともFをモデル化しないかのどちらかです。これは同値関係であり、 Fの長さに関する帰納法によって、 （ TとFのサイズが両方とも有界である場合）有限個の同値類を持つことが示されます。^{[ 13 ]}    

与えられたグラフGの木分解は、木と、各木ノードに対応するGの頂点のサブセットであるバッグから構成されます。これは、次の 2 つの特性を満たす必要があります。G の各頂点 v に対して、 vを含むバッグは木の連続するサブツリーに関連付けられている必要があり、Gの各エッジuvに対して、 uとv の両方を含むバッグが存在する必要があります。バッグ内の頂点は、そのバッグから派生する木分解のサブツリーで表されるGのサブグラフの終端と考えることができます。Gの木幅が有界である場合、すべてのバッグのサイズが有界である木分解が存在し、そのような分解は固定パラメータ扱いやすい時間で見つけることができます。^{[ 14 ]}さらに、この木分解を選択して、各バッグに 2 つの子サブツリーのみを持つ二分木を形成することも可能です。したがって、このツリー分解に対してボトムアップ計算を実行することが可能であり、各バッグを根とする部分木の同値類の識別子を、バッグ内で表されるエッジと、その2つの子の同値類の2つの識別子を組み合わせることによって計算します。^{[ 15 ]}

このようにして構築されたオートマトンのサイズは、入力MSO式のサイズの基本的な関数ではありません。この非基本的な複雑さは、( P = NPでない限り) パラメータに基本的な依存性を持つ固定パラメータ扱い可能な時間で木に対してMSO特性をテストすることができないという意味で必要です。^{[ 16 ]}

別のアプローチでは、モデル検査問題をブール充足可能性問題のインスタンスに変換することで機能します。これは、木分解に沿って変換を慎重に誘導して、木の幅の拡大をできるだけ小さく保つことによって実現されます。直接的な結果として、指数時間仮説の下でほぼタイトな実行時間の上限が得られます。実際、実行時間の上限の結果として得られるタワーの高さ（量化子交替の数）は最適であると予想されます。^{[ 17 ]}ブール充足可能性問題の 基となる動的計画法アルゴリズムを最大充足可能性問題または♯SATのアルゴリズムに置き換えることにより、最適化バージョンまたは計数バージョンに対応する実行時間の上限がそれぞれすぐに得られます。

クールセルの定理の証明は、より強力な結果を示しています。すなわち、有界木幅のグラフに対して、すべての（計数）単項二階性質を線形時間で認識できるだけでなく、有限状態木オートマトンによっても認識できるということです。クールセルはこれの逆を予想しました。有界木幅のグラフの性質が木オートマトンによって認識される場合、それは計数単項二階論理で定義できるということです。1998年にラポワール（1998）は、この予想の解決を主張しました。^{[ 18 ]}しかし、その証明は広く不十分であると見なされています。^{[ 19 ] [ 20 ]} 2016 年までは、いくつかの特殊なケースのみが解決されていました。具体的には、ツリー幅が最大 3 のグラフ、^{[ 21 ]}ツリー幅 k の k 連結グラフ、一定のツリー幅と弦長を持つグラフ、および k 外平面グラフについて予想が証明されていました。予想の一般版は、最終的にMikołaj Bojańczykと Michał Pilipczuk によって証明されました。^{[ 22 ]}

さらに、ハリングラフ（木幅3のグラフの特殊なケース）の場合、カウントは不要です。これらのグラフでは、木オートマトンで認識できるすべてのプロパティを単項2階述語論理でも定義できます。木分解自体をMSOLで記述できる特定のグラフクラスについても、より一般的に同じことが言えます。ただし、木幅が制限されているすべてのグラフに対しては、これは当てはまりません。一般に、カウントはカウントなしの単項2階述語論理よりも強力になるからです。たとえば、偶数個の頂点を持つグラフは、カウントを使用すれば認識できますが、カウントなしでは認識できません。^{[ 20 ]}

単項二階述語論理の式の充足可能性問題とは、その式が真となるグラフ（おそらく限定されたグラフ族内）が少なくとも１つ存在するかどうかを判定する問題である。任意のグラフ族および任意の式に対して、この問題は決定不能である。しかし、MSO ₂式の充足可能性は、木幅が制限されたグラフに対しては決定可能であり、MSO ₁式の充足可能性は、クリーク幅が制限されたグラフに対しては決定可能である。証明には、式に対する木オートマトンを構築し、そのオートマトンに受理パスが存在するかどうかをテストすることが含まれる。

部分的な逆として、Seese (1991)は、グラフの族が決定可能な MSO ₂充足可能性問題を持つ場合、その族は有界な木幅を持たなければならないことを証明した。証明は、有界でない木幅を持つグラフの族は任意の大きさのグリッドマイナーを持つというRobertsonとSeymourの定理に基づいている。^{[ 23 ]} _{Seese はまた、決定可能な MSO 1}充足可能性問題を持つグラフの族はすべて有界なクリーク幅を持たなければならないと予想した。これは証明されていないが、MSO _{1 を}CMSO ₁に置き換える予想の弱化は正しい。^{[ 24 ]}

Grohe (2001)は、Courcelle の定理を用いて、グラフGの交差数を計算することは、 Gのサイズに 2 乗依存する固定パラメータ扱い可能であり、Robertson –Seymour の定理に基づく 3 乗時間アルゴリズムを改善した。後にKawarabayashi & Reed (2007)によって線形時間に改善されたが、これも同じアプローチに従っている。与えられたグラフG の木幅が小さい場合、Courcelle の定理をこの問題に直接適用できる。一方、G の木幅が大きい場合、大きなグリッドマイナーが含まれており、その中で交差数を変更せずにグラフを単純化できる。Grohe のアルゴリズムは、残りのグラフの木幅が小さくなるまでこれらの単純化を実行し、その後、Courcelle の定理を適用して縮小された部分問題を解く。^{[ 25 ] [ 26 ]}

Gottlob & Lee (2007)は、グラフとカットペアの集合によって形成される構造が有界な木幅を持つ場合、グラフ内の最小多分岐カットを見つけるいくつかの問題に Courcelle の定理が適用されることを確認しました。その結果、彼らは、単一のパラメータである木幅によってパラメータ化された、これらの問題に対する固定パラメータ扱いやすいアルゴリズムを取得し、複数のパラメータを組み合わせた以前のソリューションを改善しました。^{[ 27 ]}

計算トポロジーにおいて、Burton & Downey (2014) は、 Courcelle の定理を MSO ₂から、任意の固定次元の単体上の量化を可能にする、有界次元の単体複体上の単項二階論理の形式に拡張しました。その結果、多様体が双対グラフのツリー幅が小さい三角分割 (退化単体を回避) を持つ場合、3-多様体の特定の量子不変量を計算する方法、および離散モース理論の特定の問題を効率的に解く方法を示しました。^{[ 28 ]}

クールセルの定理に基づく手法は、データベース理論^{[ 29 ]} 、知識表現と推論^{[ 30 ]} 、オートマトン理論^{[ 31 ]}、モデル検査^{[ 32 ]}にも適用されている。