グラフの論理

グラフ理論と有限モデル理論という数学の分野では、グラフの論理は、数理論理学の文を用いてグラフの特性の形式的な仕様を扱います。これらの文で使用できる論理演算の種類には、いくつかのバリエーションがあります。グラフの第一階論理は、変数と述語がグラフの個々の頂点と辺に関係する文に関係しますが、モナドの第二階グラフ論理は、頂点または辺の集合に対する量化を可能にします。最小不動点演算子に基づく論理は、頂点の組に対するより一般的な述語を可能にしますが、これらの述語は不動点演算子を通してのみ構築できるため、その能力は制限されます。

ある文が、あるグラフに対しては真でも、他のグラフに対しては偽である場合があります。グラフがをモデル化していると言われ、 と表記される場合、の頂点と隣接関係が真となります。モデル検査のアルゴリズム上の問題は、与えられたグラフが与えられた文をモデル化しているかどうかをテストすることです。満足度のアルゴリズム上の問題は、与えられた文をモデル化するグラフが存在するかどうかをテストすることです。モデル検査と満足度は一般にどちらも困難ですが、いくつかの主要なアルゴリズム上のメタ定理は、この方法で表現された特性が重要なグラフのクラスに対して効率的にテストできることを示しています。 ${\displaystyle S}$${\displaystyle G}$ ${\displaystyle S}$${\displaystyle G\models S}$${\displaystyle S}$${\displaystyle G}$

グラフの論理に関するその他の研究テーマには、ランダム グラフが特定の種類の論理内で指定されたプロパティを持つ確率の調査や、一意のグラフによってモデル化される論理文を見つけることに基づくデータ圧縮の方法などがあります。

グラフの一階述語論理では、グラフプロパティは、グラフの頂点を表す変数と、等価性および隣接性のテストのための述語を持つ量化された論理文として表現されます。^[1]

例えば、グラフに孤立した頂点が存在しないという条件は、次の文で表現できます 。 ここで、記号は2つの頂点間の無向隣接関係を示します。この文は、すべての頂点に対して、隣接する別の頂点が存在するという意味に解釈できます。^[1]$${\displaystyle \forall u\exists v(u\sim v)}$$${\displaystyle \sim}$${\displaystyle u}$${\displaystyle v}$${\displaystyle u}$

固定された部分グラフの部分グラフ同型性問題は、 がより大きなグラフ の部分グラフとして現れるかどうかを問うものです。 これは、 の各辺について、対応する変数のペアが隣接する頂点を表し、 の残りの各頂点のペアについて、対応する変数のペアが異なる頂点を表すような頂点（ の各頂点に 1 つずつ）が存在することを述べる文で表現できます。 ^[2]図を参照してください。 特殊なケースとして、クリーク問題（クリークのサイズが固定されている場合）は、クリークのサイズに等しい数の頂点が存在し、それらはすべて隣接していることを述べる文で表現できます。^[3]${\displaystyle H}$${\displaystyle H}$${\displaystyle G}$${\displaystyle H}$${\displaystyle H}$${\displaystyle H}$

単純な無向グラフの場合、グラフの第一階理論には公理が含まれる。

${\displaystyle \forall u{\bigl (}\lnot (u\sim u){\bigr )}}$（グラフにはループを含めることはできません）、そして

${\displaystyle \forall u\forall v(u\sim v\Rightarrow v\sim u)}$（辺は無向である）。^[4]

有向グラフなどの他の種類のグラフでは、異なる公理が関係する可能性があり^{[5] 、}マルチグラフプロパティの論理的定式化では、複数のエッジ関係^[6]や頂点とエッジに別々の変数を持つなどの特別な処理が必要になります^{[7] 。}

Glebskiĭ et al. (1969) と、それとは独立に Fagin (1976) は、一階グラフ論理のゼロ-一法則を証明しました。Fagin の証明では、コンパクト性定理が使用されました。この結果によると、エルデシュ-レーニモデルにおけるランダムグラフでは、すべての一階文はほぼ常に真か、ほぼ常に偽のいずれかになります。つまり、を固定した一階文とし、ラベル付き頂点の集合上のすべてのグラフから一様にランダムにランダムな-頂点グラフを選択します。そして、が無限大に近づく極限では、モデルがゼロか1に近づく 確率は次のようになります。さらに、ラドグラフと 呼ばれる特定の無限グラフがあり、ラドグラフによってモデル化された文は、ランダムな有限グラフによってモデル化される確率が1に近づく文とまったく同じです。 各辺が他の辺から独立して一定の確率で含まれるランダムグラフの場合、同じ結果が当てはまり、同じ文がゼロか1に近づく確率を持ちます。^[8]${\displaystyle S}$${\displaystyle n}$${\displaystyle G_{n}}$${\displaystyle n}$${\displaystyle n}$${\displaystyle G_{n}}$${\displaystyle S}$$${\displaystyle \lim _{n\to \infty }\operatorname {Pr} [G_{n}\models S]\in \{0,1\}.}$$ ${\displaystyle R}$$${\displaystyle R\models S\quad \Longleftrightarrow \quad \lim _{n\to \infty }\operatorname {Pr} [G_{n}\models S]=1.}$$

与えられた文が確率が 0 に近づくのか 1 に近づくのかを判断する計算量は高く、この問題はPSPACE 完全です。^[9] 1 次グラフ特性がランダムグラフ上で確率が 1 に近づく場合、特性をモデル化するすべての - 頂点グラフを、グラフごとに多項式遅延( の関数として) でリストすることが可能です。^[4]${\displaystyle n}$${\displaystyle n}$

同様の分析は、非一様ランダムグラフに対しても実行できます。このグラフでは、辺が含まれる確率は頂点の数の関数であり、辺を含めるか除外するかの決定は、すべての辺に対して独立して同じ確率で行われます。ただし、これらのグラフの場合、状況はより複雑です。この場合、第 1 階の特性には 1 つ以上のしきい値があり、辺包含確率がしきい値から制限されている場合、特定の特性を持つ確率は 0 または 1 に近づきます。これらのしきい値は の無理数乗になることは決してないため、辺包含確率が無理数乗であるランダムグラフは、一様ランダムグラフの場合と同様の 0-1 法則に従います。同様の 0-1 法則は、 が超特殊比でない限り、の辺包含確率を持つ非常に疎なランダムグラフにも当てはまります。^[10]が超特殊である場合、特定の特性を持つ確率は 0 でも 1 でもない極限に近づきますが、この極限は効率的に計算できます。^[11]閾値が無限にある第一階の文が存在する。^[12]${\displaystyle n}$${\displaystyle n^{-c}}$${\displaystyle c>1}$${\displaystyle c}$${\displaystyle c}$

一次文に異なる変数が含まれる場合、それが記述する特性は、頂点のグラフにおいて、すべての組の頂点を調べることによってテストできます。ただし、この総当たり探索アルゴリズムは特に効率的ではなく、時間がかかります。グラフが与えられた一次文をモデル化しているかどうかを確認する問題には、特殊なケースとして、サブグラフ同型性問題(文が固定されたサブグラフを含むグラフを記述する) とクリーク問題(文が固定サイズの完全なサブグラフを含むグラフを記述する) が含まれます。クリーク問題は、パラメータ化された複雑性の観点から難しい問題の階層の最初のレベルであるW(1)に対して困難です。したがって、実行時間がおよびに依存しない関数および定数の形をとる、固定パラメータで扱いやすいアルゴリズムが存在する可能性は低いです。^[13] さらに強く言うと、指数時間仮説が正しい場合、クリーク検出と一次モデル検査には、必然的に の累乗に比例した時間がかかり、その指数は に比例します。^[14]${\displaystyle k}$${\displaystyle n}$${\displaystyle k}$${\displaystyle O(n^{k})}$${\displaystyle O(f(k)n^{c})}$${\displaystyle f}$${\displaystyle c}$${\displaystyle k}$${\displaystyle n}$${\displaystyle n}$${\displaystyle k}$

グラフの制限されたクラスでは、一階文のモデル検査ははるかに効率的になります。特に、一階文として表現できるすべてのグラフ特性は、有界拡張のグラフに対して線形時間でテストできます。これらは、すべての浅いマイナーがスパースグラフであり、辺と頂点の比率がマイナーの深さの関数によって制限されるグラフです。さらに一般的には、一階モデル検査は、どこにも密でないグラフ、つまり、各可能な深さで少なくとも 1 つの禁止された浅いマイナーがあるグラフのクラスに対して、ほぼ線形時間で実行できます。逆に、モデル検査が任意の単調なグラフの族に対して固定パラメータで処理可能である場合、その族はどこにも密でないに違いありません。^[15]

グラフの論理における一階述語文は、が をモデル化する唯一のグラフである場合にグラフを定義すると言われる。すべてのグラフは少なくとも 1 つの文によって定義される。たとえば、任意の-頂点グラフは、グラフの各頂点に 1 つずつ変数を持ち、さらにグラフの頂点以外の頂点が存在しないという条件を述べる変数を持つ文によって定義できる。文の追加節を使用して、2 つの頂点変数が等しくないこと、 の各辺が存在すること、 の隣接していない頂点のペア間に辺が存在しないことを保証できる。ただし、一部のグラフでは、グラフを定義する大幅に短い文が存在する。^[16]${\displaystyle S}$${\displaystyle G}$${\displaystyle G}$${\displaystyle S}$${\displaystyle n}$${\displaystyle G}$${\displaystyle n+1}$${\displaystyle n}$${\displaystyle G}$${\displaystyle G}$

与えられたグラフを定義する最も単純な文（単純さの尺度は異なる）から、いくつかの異なるグラフ不変量を定義できます。特に、グラフの論理的深さは、グラフを定義する文における量指定子のネスト（量指定子のランク）の最小レベルとして定義されます。 ^[17]上記の文は、そのすべての変数の量指定子をネストしているため、論理的深さ を持ちます。グラフの論理的幅は、グラフを定義する文の変数の最小数です。^[17]上記の文では、この変数の数は です。論理的深さと論理的幅は、どちらも与えられたグラフのツリー幅によって制限できます。 ^[18]同様に、論理的長さは、グラフを説明する最短の文の長さとして定義されます。上記の文の長さは頂点の数の 2 乗に比例しますが、長さが辺の数に比例する文で任意のグラフを定義することができます。^[17]${\displaystyle n+1}$${\displaystyle n+1}$

すべての木とほとんどのグラフは、2つの変数のみを持つ一階の文で記述できますが、述語を数えることで拡張されます。この論理で固定定数の変数を持つ文で記述できるグラフの場合、多項式時間でグラフの正規化を見つけることができます（多項式の指数は変数の数に等しい）。正規化を比較することで、これらのグラフのグラフ同型問題を多項式時間で解決できます。 ^[19]

トラクテンブロートの定理の特別なケースとして、与えられた一階述語文が有限無向グラフで実現できるかどうかは決定不可能である。つまり、すべての文に対してこの質問に正しく答えられるアルゴリズムは存在しない。^[20]

1 階の文の中には、無限グラフではモデル化できるが、有限グラフではモデル化できないものがある。例えば、 1次数の頂点がちょうど 1 つあり、他のすべての頂点の次数がちょうど 2 であるという性質は、1 階の文で表現できる。これは無限光線でモデル化できるが、有限グラフに対するオイラーの握手補題に違反する。しかし、1930 年代にアロンゾ・チャーチとアラン・チューリングが提唱したEntscheidungsproblemの否定解から、有限に制約されていないグラフに対する 1 階の文の充足可能性は決定不可能なままであることがわかる。また、すべてのグラフに対して真である 1 階の文と、有限グラフに対して真だが一部の無限グラフに対して偽である 1 階の文を区別することも決定不可能である。^[21]

最小固定点に基づくグラフの論理は、特別な固定点演算子によって定義された述語（頂点または頂点の組のプロパティ）を許可することで、グラフの第一階論理を拡張します。この種の定義は、述語の特定の値が真である場合に他の値も真であることを示す式である含意から始まります。「固定点」とは、これが有効な含意である述語です。常に真である述語を含め、固定点は多数存在する可能性があります。「最小固定点」は、可能な限り真の値が少ない固定点です。より正確には、その真の値は他の固定点の真の値のサブセットである必要があります。^[22]

例えば、与えられたグラフにおいて 2 つの頂点と がパスで接続されている場合は を真と定義し、そうでない場合は を偽と定義します。すると、すべての頂点は自分自身と接続され、が の隣接頂点と接続されている場合は、もう 1 ステップで にも接続されます。この推論を論理的に表現すると、は式の最小不動点 となります 。ここで、不動点であるということは、逆の含意矢印が示唆するように、式の右側が真であれば左側が真であることを意味します。この場合、最小不動点であるということは、この含意を繰り返し使用することで接続性が示されない限り、2 つの頂点が接続されていると定義されないことを意味します。^[22]${\displaystyle C(u,v)}$${\displaystyle u}$${\displaystyle v}$${\displaystyle u}$${\displaystyle v}$${\displaystyle v}$${\displaystyle C}$$${\displaystyle C(u,v)\leftarrow {\Bigl (}(u=v)\vee \exists w{\bigl (}C(u,w)\wedge w\sim v{\bigr )}{\Bigr )}.}$$

不動点論理のいくつかのバリエーションが研究されている。最小不動点論理では、最小不動点を明確に定義するために、定義式の演算子の右側の項は述語を肯定的にのみ使用する必要がある（つまり、各出現は偶数の否定内にネストされている必要がある）。同等の論理力を持つ別のバリエーションであるインフレーション不動点論理では、式は単調である必要はないが、結果として得られる不動点は、すべて偽の述語から始めて定義式から得られる含意を繰り返し適用することによって得られるものとして定義される。否定的な含意や複数の述語を同時に定義できる他のバリエーションも可能であるが、追加の定義力は提供されない。これらの方法のいずれかで定義された述語は、より大きな論理文の一部として頂点の組に適用できる。^[22]${\displaystyle \leftarrow }$

固定小数点論理、および値が 0 から頂点の数までの範囲にある整数カウント変数も許可するこれらの論理の拡張は、記述的複雑性において、多項式時間で決定できるグラフ理論の決定問題の論理的記述を提供する試みとして使用されている。論理式の固定点は、述語が真となる値の集合にタプルを繰り返し追加して固定点に到達するアルゴリズムによって多項式時間で構築できるため、この論理ではグラフが文をモデル化しているかどうかの決定は常に多項式時間で決定できる。多項式時間のグラフ特性のすべてが、固定小数点とカウントのみを使用する論理の文でモデル化できるわけではない。^{[23] [24]}ただし、一部の特殊なグラフクラスでは、多項式時間特性はカウント付きの固定小数点論理で表現可能な特性と同じである。これらには、ランダムグラフ^{[23] [25]}区間グラフ[ ^{23] [26]および（}グラフ構造定理の論理的表現を通じて）禁制マイナーグラフによって特徴付けられるあらゆるクラスのグラフ^[23]が含まれる。

グラフのモナド二階論理では、変数は頂点、辺、頂点の集合、辺の集合の最大 4 種類のオブジェクトを表します。モナド二階グラフ論理には、主に 2 つのバリエーションがあります。頂点と頂点集合の変数のみが許可される MSO ₁と、4 種類の変数すべてが許可される MSO ₂です。これらの変数の述語には、等価性テスト、メンバーシップ テスト、頂点と辺の関連性 (頂点と辺の両方の変数が許可されている場合) または頂点のペア間の隣接性 (頂点の変数のみが許可されている場合) が含まれます。定義のその他のバリエーションでは、モジュラー カウント述語などの追加の述語が許可されます。^[27]

一例として、無向グラフの接続性は、頂点を 2 つの空でない部分集合に分割するたびに、一方の部分集合からもう一方の部分集合への辺が存在するというステートメントとしてMSO ₁で表現できます。頂点の分割は、分割の片側にある頂点の部分集合によって記述でき、そのような各部分集合は、自明な分割 (一方または他方の側が空である分割) を記述するか、辺が交差するかのいずれかである必要があります。つまり、グラフが接続されているのは、MSO ₁文 をモデル化する場合です。 ただし、接続性は、第 1 階グラフ論理では表現できず、存在 MSO ₁ (すべての集合量指定子が存在的で文の先頭に出現するMSO _1のフラグメント) や存在 MSO ₂でも表現できません。^[28]${\displaystyle S}$$${\displaystyle \forall S{\Bigl (}\forall x(x\in S)\vee \forall y{\bigl (}\lnot (y\in S){\bigr )}\vee \exists x\exists y{\bigl (}x\in S\wedge \lnot (y\in S)\wedge x\sim y{\bigr )}{\Bigr )}.}$$

MSO _2では、ハミルトン性は、すべての頂点で接続された 2 正則グラフを形成する辺の集合の存在によって表現できます。接続性は上記のように表現され、2 正則性は各頂点で 3 つの異なる辺ではなく 2 つの辺の発生として表現されます。ただし、MSO 1 ではハミルトン性は表現できません。_なぜなら、MSO _{1 は、2 分割の各側に等しい数の頂点を持つ}完全 2 部グラフ(ハミルトングラフである) と不均衡な完全 2 部グラフ (そうではない) を区別できないためです。^[29]

_MSO2の定義には含まれていないが、無向グラフの向きはトレモー木を使った手法で表現することができる。これにより向きに関する他のグラフ特性も表現できる。^[30]

クールセルの定理によれば、木幅が制限されたグラフでは、すべての固定された MSO ₂プロパティを線形時間でテストでき、クリーク幅が制限されたグラフでは、すべての固定された MSO ₁プロパティを線形時間でテストできます。^{[31]木幅が制限されたグラフに対するこの結果のバージョンは、}対数空間でも実装できます。^[32]この結果の応用には、グラフの交差数を計算するための固定パラメータの扱いやすいアルゴリズムが含まれます。 ^[33]

モナド的二階述語論理の文の充足可能性問題は、その文が真となるグラフが少なくとも 1 つ (場合によっては制限されたグラフ族内) 存在するかどうかを判断する問題である。任意のグラフ族および任意の文について、この問題は決定不可能である。しかし、木幅が制限されたグラフについてはMSO _{2文の充足可能性は決定可能であり、クリーク幅が制限されたグラフについては MSO 1}文の充足可能性は決定可能である。証明には、クールセルの定理を使用して、その特性をテストできるオートマトンを構築し、次にそのオートマトンを調べて受け入れ可能なグラフがあるかどうかを判断することが含まれる。部分的な逆として、^{[34] Seese (1991) は、グラフ族に決定可能な MSO} ₂充足可能性問題がある場合は常に、その族には木幅が制限されている必要があることを証明した。証明は、無制限の木幅を持つグラフの族は任意に大きなグリッド マイナーを持つというロバートソンとシーモアの定理に基づいています。また、決定可能なMSO ₁充足問題を持つグラフの族はすべて、クリーク幅が制限されている必要があると予想しました。 ^{[35]これは証明されていませんが、モジュラーカウンティング述語でMSO} ₁を拡張する予想の弱化は正しいです。^[34]