理論計算機科学 において、非決定性制約論理は、一定の制約の下で重み付き無向グラフの辺に方向が与えられる組み合わせシステムである。同じ制約の下で、単一の辺を反転するステップによってこの方向を変えることができる。これは、辺の方向変更の各シーケンスを元に戻せるという点で 、可逆論理の一種である。
特定の状態を接続する、すべての状態を接続する、または指定されたエッジを反転する一連の動きを求める制約論理の再構成問題は、 PSPACE 完全であることが証明されています。これらの困難性の結果は、さまざまなゲームやパズルが PSPACE 困難または PSPACE 完全であることの証明の基礎となります。
制約グラフ


非決定性制約論理の最も単純なバージョンでは、無向グラフの各辺の重みは 1 または 2 です。(重みは、重み 1 の辺を赤で、重み 2 の辺を青で描画することでグラフィカルに表現することもできます。) グラフは立方体グラフである必要があります。つまり、各頂点は 3 つの辺に接続し、さらに各頂点は偶数個の赤い辺に接続する必要があります。[2]
辺は、少なくとも2単位の重みが各頂点に向くように向けられている必要があります。つまり、少なくとも1つの青い辺、または少なくとも2つの赤い辺が入らなければなりません。これらの制約を遵守しながら、1つの辺を反転させるステップによって向きを変えることができます。[2]
より一般的な非決定性制約ロジックでは、より多様なエッジウェイト、頂点あたりのエッジ数の増加、各頂点の入力ウェイトのしきい値の変更が可能になります。エッジウェイトと頂点しきい値のシステムを持つグラフは、制約グラフと呼ばれます。エッジウェイトがすべて 1 または 2 で、頂点の入力ウェイトが 2 単位必要で、すべての頂点に赤エッジが偶数個ある 3 つの入力エッジがあるという制限されたケースは、制約グラフと呼ばれます。[2]
and/or制約グラフという名前が付けられた理由は、and/or制約グラフの2種類の頂点が、ブール論理のANDゲートとORゲートのように動作するからです。2つの赤いエッジと1つの青いエッジを持つ頂点は、青いエッジを外向きにする前に両方の赤いエッジが内側を向く必要があるという点で、ANDゲートのように動作します。3つの青いエッジを持つ頂点は、2つのエッジが入力として指定され、3つ目が出力として指定されるORゲートのように動作します。出力エッジを外向きにする前に少なくとも1つの入力エッジが内側を向く必要があるという点で。[2]
通常、制約ロジックの問題は、制約グラフの有効な構成を見つけることを中心に定義されます。制約グラフは、次の 2 種類のエッジを持つ無向グラフです。
- 重みのある赤い縁
- 重みのある青い縁
制約グラフを計算モデルとして使用し、グラフ全体をマシンとして考えます。マシンの構成は、グラフとそのエッジの特定の方向で構成されます。構成が流入制約を満たす場合、その構成は有効であると呼ばれます。つまり、各頂点には少なくとも の入ってくる重みが必要です。言い換えると、特定の頂点に入るエッジの重みの合計は、頂点から出るエッジの重みの合計よりも少なくとも大きくなければなりません。
また、制約グラフ内の移動は、結果として得られる構成が依然として有効であるように、エッジの方向を反転するアクションであると定義します。
制約論理問題の正式な定義
制約グラフ、開始構成、終了構成が与えられているとします。この問題は、開始構成から終了構成に移動する有効な移動のシーケンスが存在するかどうかを尋ねます。この問題は、3 正則グラフまたは最大次数 3 グラフに対して PSPACE 完全です。[3]この削減はQSATに従っており、以下に概説します。
バリエーション
平面非決定性制約ロジック
上記の問題は、制約グラフが平面であっても、つまり、2 つのエッジが互いに交差しないようにグラフを描くことができない場合でも、PSPACE 完全です。この削減は、平面 QSATに従います。
エッジ反転
この問題は、前の問題の特殊なケースです。制約グラフが与えられた場合、有効な一連の動きによって指定されたエッジを反転できるかどうかを尋ねます。最後の有効な動きが目的のエッジを反転する限り、有効な一連の動きによってこれを行うことができます。この問題は、3 正則グラフまたは最大次数 3 グラフに対して PSPACE 完全であることも証明されています。[3]
制約グラフの満足度
この問題は、無向グラフが与えられたときに流入制約を満たす辺の向きが存在するかどうかを問うものです。この問題はNP完全であることが証明されています。[3]
難しい問題
制約グラフとその向きに関する以下の問題はPSPACE完全である: [2]
- 方向と指定されたエッジe が与えられた場合、指定された方向から最終的にエッジe を反転する一連のステップが存在するかどうかをテストします 。
- 一連の手順によって、ある方向を別の方向に変更できるかどうかをテストします。
- 指定された方向を持つ 2 つのエッジeとfが与えられ、グラフ全体に 2 つの方向 (1 つはe上で指定された方向を持ち、もう 1 つはf上で指定された方向を持つ) があり、一連の手順によって相互に変換できるかどうかをテストします。
これらの問題が困難であることの証明には、and/or制約グラフの論理的解釈に基づいた、量化されたブール式の還元が含まれます。量化子をシミュレートし、赤いエッジで運ばれる信号を青いエッジで運ばれる信号に変換する(またはその逆)ための追加のガジェットが必要ですが、これらはすべてand頂点とor頂点の組み合わせによって実現できます。[2]
これらの問題は、平面グラフ を形成する および/または制約グラフに対しても PSPACE 完全のままです。これの証明には、2 つの独立した信号が互いに交差できるようにするクロスオーバー ガジェットの構築が含まれます。また、これらの問題の困難性を維持しながら、追加の制約を課すこともできます。3 つの青い辺を持つ各頂点は、赤い辺を持つ三角形の一部である必要があります。このような頂点は保護された または と呼ばれ、(グラフ全体の有効な方向に関係なく) 三角形の青い辺の両方が内側を向くことができないという特性があります。この制約により、他の問題の困難性削減でこれらの頂点をシミュレートすることが容易になります。[2]さらに、制約グラフに有界帯域幅を要求することもでき、その場合の問題は依然として PSPACE 完全のままです。[4]
PSPACE困難性の証明
この削減は QSAT に従います。QSAT 式を埋め込むには、制約グラフに AND、OR、NOT、UNIVERSAL、EXISTENTIAL、および Converter (色を変更する) ガジェットを作成する必要があります。考え方は次のとおりです。
- AND 頂点は、2 つの赤い入射エッジ (入力) と 1 つの青い入射エッジ (出力) を持つ頂点です。
- OR 頂点は、3 つの青い入射エッジ (2 つの入力、1 つの出力) を持つ頂点です。
他のガジェットもこの方法で作成できます。完全な構造はErik Demaineのウェブサイトで公開されています。[5]完全な構造はインタラクティブな方法でも説明されています。[6]
アプリケーション
非決定性制約論理の元々の応用では、ラッシュアワーや倉庫番などのスライディングブロックパズルのPSPACE完全性を証明するために使用されました。そのためには、これらのパズルでエッジとエッジの向き、頂点、保護された頂点をシミュレートする方法を示すだけで済みます。[2]
非決定性制約論理は、制限された帯域幅の平面グラフ上の独立集合、頂点カバー、支配集合などの古典的なグラフ最適化問題の再構成バージョンの困難さを証明するためにも使用されています。これらの問題では、残りの頂点が常に解を形成するという特性を維持しながら、一度に1つの頂点を解集合内または解集合外に移動することにより、与えられた問題に対する1つの解を別の解に変更する必要があります。[4]
再構成3SAT
この問題は、 3-CNF式と 2 つの満足な割り当てが与えられた場合、各ステップで変数の値を反転できる状態で、1 つの割り当てから他の割り当てへと進む一連のステップを見つけることができるかどうかを問うものです。この問題は、非決定性制約論理問題からの還元によって PSPACE 完全であることが示されます。[3]
スライディングブロックパズル
この問題は、ブロックの初期配置が与えられた場合、スライディングブロックパズルで目的の配置に到達できるかどうかを問うものです。この問題は、長方形がドミノであってもPSPACE完全です。 [2]
ラッシュアワー
この問題は、初期設定が与えられた場合にラッシュアワーパズルの勝利条件に到達できるかどうかを問うものです。この問題は、ブロックのサイズが であっても PSPACE 完全です。[3]
ダイナミックマップラベル
この問題は、静的マップが与えられたときに、滑らかな動的ラベル付けが存在するかどうかを問うものである。この問題もPSPACE完全である。[7]
参考文献
- ^ 「制約グラフ」、people.irisa.fr 、2020年2月13日閲覧
- ^ abcdefghi Hearn, Robert A. ; Demaine, Erik D. (2005)、「非決定論的制約論理計算モデルによるスライディングブロックパズルおよびその他の問題の PSPACE 完全性」、理論計算機科学、343 (1–2): 72–96、arXiv : cs/0205005、doi :10.1016/j.tcs.2005.05.008、MR 2168845、S2CID 656067。
- ^ abcde Demaine, Erik、「非決定論的制約論理」(PDF)
- ^ ab van der Zanden, Tom C. (2015)、「グラフ制約ロジックのパラメータ化された複雑さ」、第 10 回パラメータ化および正確な計算に関する国際シンポジウム、LIPIcs. Leibniz Int. Proc. Inform.、vol. 43、Schloss Dagstuhl. Leibniz-Zent. Inform.、Wadern、pp. 282–293、arXiv : 1509.02683、doi : 10.4230/LIPIcs.IPEC.2015.282、ISBN 9783939897927、MR 3452428、S2CID 15959029。
- ^ Gurram, Neil、「非決定論的制約論理」(PDF)、Erik Demaine
- ^ 「制約グラフ(制約グラフとQBFからの削減を説明するインタラクティブなウェブサイト)。著者:François Schwarzentruber。」、people.irisa.fr 、 2020年2月20日取得
- ^ Buchin, Kevin; Gerrits, Dirk HP (2013)、「Dynamic Point Labeling is Strongly PSPACE-Complete」、Cai, Leizhen、Cheng, Siu-Wing、Lam, Tak-Wah (編)、『Algorithms and Computation』、Lecture Notes in Computer Science、vol. 8283、Springer Berlin Heidelberg、pp. 262–272、doi :10.1007/978-3-642-45030-3_25、ISBN 9783642450303
