すぴすらのろぐ

読んだもののメモとかポエムとか

3-CNF SATからpolygraphのacyclicity判定問題への帰着

papa本 誰得 TX

このポストは、papa本で証明されている「スケジュールsが与えられとき、それがview serializableであることのテストはNP完全である」の証明の一部を構成する、3-CNF SAT問題からpolygraphのacyclicity判定問題への帰着についてのメモです。

papa本は以下の本のことです。

Theory of Database Concurrency Control

Theory of Database Concurrency Control

証明の流れ

  1. スケジュールsがview serializableである iff polygraph P(s)が非巡回である （Theorem 2.4）
  2. polygraphが非巡回であることのテストはNP完全である（Theorem 2.5）
    1. 3-CNF Fが充足可能 iff polygraph P(F)が非巡回である（本ポストの内容）
    2. 3-CNF Fからpolygraph P(F)が多項式時間で構築できる
  3. polygraph Pが与えられたとき、「Pが非巡回である iff スケジュールsがview serializableである」ようなスケジュールsをPから構築できる（Lemma 2.4）

1. 準備

1.1 polygraphとは

有向グラフ (V,A)で表現される二項関係において、ある頂点と辺のペア v \in V, (w,u) \in A, （u,v,wは互いに異なる）に対し、関係 (u,v)または関係 (v,w)のどちらか一方が排他的に成り立つとき、頂点の三つ組み (u,v,w) \in (V \times V \times V)をchoiceと呼ぶ。

two potential edges in choice

choiceによる2つの（どちらか一方の）潜在的な関係の可能性を、グラフ上ではその関係に対応する破線で描かれた2つの辺と円弧で表現する。choiceを含む有向グラフをpolygraphと呼ぶ。

representation of choice in polygraph

choiceで表現できる可能性が複数ある場合に指数的に増えていく可能な有向グラフ群を、1つのpolygraphで表現することができる。choiceで表現可能な潜在的な関係がある場合にpolygraphが有用である。

polygraph Pのそれぞれのchoiceに対して、どちらか一方の破線辺を辺として選択して得られる有向グラフDは、polygraph Pとcompatibleであるという。

polygraph Pとcompatibleな有向グラフの中に非巡回な有向グラフ（DAG）が存在する場合、そのpolygraph Pはacyclicであるという。

詳細はぱと隊長さんのポストを参照ください！polygraphに関するWeb上で貴重な（唯一の？）資料です。

1.2 CNFとは

論理式の連言標準形*1のこと。Conjunctive Normal Form の略。

CNFの例: (x_1 \lor x_2 ) \land (x_1 \lor \lnot x_2) \land (\lnot x_1 \lor \lnot x_2)

選言（論理和）によるカタマリ（カッコ内）をそれぞれ節（clause）と呼ぶ。

x_1, \lnot x_2等の変数の単体の出現およびその否定をリテラル（literal）と呼ぶ。

CNFな論理式のうち、節内のリテラルの数が高々3つであるものを3-CNFと呼ぶ。

1.3 SATとは

命題論理式の充足可能性問題（satisfiability problem）をSATと呼ぶ。 充足可能性問題とは、与えられた命題論理式に対して、式に含まれる変数に対して式全体を真とするような真理値割当てが存在するかどうかを問う問題のことである。 NP完全であることが知られている。

CNF-SATは連言標準形の論理式の充足可能性を問う問題で、こちらもNP完全。

3-SAT（3-CNF-SAT）は3-CNF 論理式の充足可能性を問う問題で、こちらもNP完全。

2 帰着の概要

3-CNF SATからpolygraphのacyclicity判定問題への帰着は以下の要素で構成されます。

  1. 3-CNF SATからsimple 3-CNF SATへの帰着
  2. 3-CNF 論理式F からpolygraph P(F)を構築する
  3. simple 3-CNF-SATからpolygraphのacyclicity判定問題への帰着

ここでpolygraphのacyclicity判定問題とは、polygraphとcompatibleな有向グラフの中で巡回がない有向グラフ（DAG）が存在するかを問う問題です。

3-CNFがsimpleであることは、最後の充足可能性と非巡回性の対応付けの際に必要になるものです。

3 3-CNF-SATからsimple 3-CNF-SATへの帰着（Lemma 2.3）

3-CNF SATをsimple 3-CNF SATに変換する手順を示します。

この変換は等価な論理式への変換ではありませんが、3-CNFにおける充足可能性と変換後のsimple 3-CNFにおける充足可能性が等しくなるような変換です。 本書ではこれを帰着とは呼んでいませんが、3-CNF-SATをsimple 3-CNF-SATに帰着していると解釈できます。 またこの変換手順が多項式時間で終わることも示していませんが、論理式の長さに比例する時間で完了すると思われます。

3.1 準備

命題論理式において、否定されていない（命題）変数の出現を positive literalと呼ぶ。

同様に否定されている変数の出現をnegative literalと呼ぶ。

CNF論理式における節内にpositive/negative literalが混在していることをmixedであるという。

mixedな節がないCNF論理式をsimpleであるという。

3.2 変数の置換え

論理式内にはある変数がpositve/negativeの形で複数回出現しうる。その出現を、それぞれ別の新しい変数に置換える。元のリテラルのpositive/negativeにかかわらず変換後の変数のpositive literalとして置換えることで、元の論理式におけるすべてのリテラルをpositive表現にすることができる。

変数 xに対して、 x_1, x_2, \ldots , x_{2m}を新しい変数とし、元の論理式における変数 xの出現を以下のルールに従って新しい変数に置換する。 mは変数 x のpositve出現回数、およびnegative出現回数の大きいほうの値である（後述の制約節を作る際に便利なためである）。

  • 変数 xのpositive literalを、その出現順に x_1, x_3, x_5, \ldots と置換える
  • 変数 xのnegative literalを、その出現順に x_2, x_4, x_6, \ldots と置換える

例:

  • 変換前： (x_1 \lor x_2 ) \land (x_1 \lor \lnot x_2) \land (\lnot x_1 \lor \lnot x_2)
  • 変換後： (x_{1,1} \lor x_{2,1} ) \land (x_{1,3} \lor x_{2,2}) \land (x_{1,2} \lor x_{2,4})

3.3 制約する節の追加

置換後の論理式には置換元のある変数から置換えられた複数の変数が存在するので、これらの変数に同じ真理値を割当てることを保証したい。

例えば x_1と x_3には同じ真理値を割当てなければならないし、 x_1とx_2には逆の真理値を割当てる必要がある。これを表す節を以下の方法で作成し、変数置換え後の元の論理式に変換後の変数間の制約を表す節を（AND条件で）追加する（ここでは制約節と呼ぶことにする）。

追加される制約節：

  • すべての変数 y に対し、置換え後の変数 x_1, x_2, \ldots , x_{2m} に対し、 (x_1 \lor x_2) \land (\lnot x_1 \lor \lnot x_2) \land (x_2 \lor x_3) \land (\lnot x_2 \lor \lnot x_3) \land \ldots \land (x_{2m} \lor x_1) \land (\lnot x_{2m} \lor \lnot x_1) という節を元の論理式に追加する。

変数 xに対する制約節の1つ目の節の役割は、 x_1と x_2が同時に偽になる場合は論理式全体を偽とする（充足されない）ことで、同様に2つ目の節の役割は、 x_1と x_2が同時に真になる場合は論理式全体を偽とする（充足されない）ことである。2つ合わせて変数 xを x_1と x_2という2つの変数に逆の真理値を割当てることを保証*2している。

それ以降も同様で、隣接する添え字間で逆の真理値が割り当てられることを保証することで、同じ1つの変数 xに対する変数置換が矛盾のない真理値割当てを持つことを保証する*3*4。

変数置換によって元の論理式は非mixedになり、追加された制約節も2-CNFな非mixed論理式であるので、置換後の3-CNF論理式はsimpleである。

4 3-CNF論理式に対するpolygraphの構築手順

4.1 変換後のpolygraphの要素

入力となる3-CNF論理式Fの要素に応じて、以下の部分（poly）グラフを準備する。

Variable

3-CNF論理式に出現する各変数について、以下の図に示すようなVariableと呼ぶ1つのchoice*7を用意する。

Variable

この部分polygraphの役割は、論理式における変数の排中律（真が偽のいずれか一方の値をとること）とchoiceの二者択一性を対応付けることである。

本ポストではchoiceの二つの破線辺のうち、変数が真となるときに実線となる方を青、偽となるときに実線となる方を赤で表すことにする。

Clause

3-CNF論理式に出現する各節について、以下の図に示すようなClauseと呼ぶ1つの部分polygraphを用意する。

Clause

Clauseにおける破線はそれぞれ節内のリテラル（≠変数）に対応する。ある真理値割当てにおいてリテラルが偽となる場合に対応する破線が実線であると選択される。

この部分polygraphの役割は、節が偽となるような真理値割当てとグラフにおけるcycleの存在を対応付けることである*8。

Clauseの各リテラル（破線）に対して、Clauseの破線とVariable（choice）の破線をそのpositive/negative表現が合うように、Variable（choice）のコピーを以下のように付加する。

Clause with Variables

positive literalとnegative literalではVariableの付加の仕方が異なる。

具体的には、positive literalに対しては、clauseの破線とchoiceの偽の破線（赤）を重ね合わせ、negative literalに対しては、clauseの破線とchoiceの真の破線（青）を重ね合わせる。

Fan-out

上記で用意したVariableとClause（に付加したVariableのコピー）をFan-outと呼ぶ構造で接続する。

Fan-outの意図は、同じ変数に対するすべての（コピーされた）Variable、つまりchoiceが、同じ選択になるように（同じ真偽値に対応する破線辺を実線辺とすることを）強制することである。

Clauseに付加したVariableのコピーのうち外側の破線（Clauseを構成しない方の破線）を、以下のようにオリジナルのVariableの真偽が逆の破線辺と接続する。

  • Clauseに付加されたVariableの外側の破線が辺true側（青）であれば、オリジナルのVariableのfalse側（赤）と接続する
  • Clauseに付加されたVariableの外側の破線辺がfalse側（赤）であれば、オリジナルのVariableのtrue側（青）と接続する

接続する2つの辺の向きは、Clauseの外側の破辺線と、接続したオリジナルのVariableの破線辺を含み、cycleを構成しうるような向きである。つまり以下の図のように接続する：

Clauseにおける変数の出現がpositive literalの場合：

connection between positive literal and variable via fan-out

。 Clauseにおける変数の出現がnegative literalの場合：

connection between negative literal and variable via fan-out 。

4.2 3-CNFに対応するpolygraphの構築

すべての変数 x_iに対してそれぞれ、3-CNF論理式に現れるすべての（Clause内の）出現に対応するVariableのコピーを上記の方法でオリジナルのVariableと接続する。

これで3-CNF論理式Fに対応するpolygraph P(F)を構築することができる。

4.3 Fan-outの機能

オリジナルのVariableを中心に置いてpolygraphを見ると、以下の図のように左側の偽の破線辺（赤）にはpositive literalとして出現するClauseが、右側の真の破線辺（青）にはnegative literalとして出現するClauseが並ぶ。

Fan-out

ここで仮に、変数 x_iがpositive literalとして出現する節において変数の真理値割当てをtrueとしたいとする。 これは上図のpolygraphでいうと左側のClauseに付加したchoiceにおいて外側の青の破線辺を実線と選択することになる。

polygraphにcycleを作りたくないとすると、オリジナルのVariableのchoiceにおいてもtrueの破線辺（青）を選択せざるを得なくなる*9。

オリジナルのVariableのchoiceがtrueの破線辺（青）を選択すると、同様に変数 x_iがnegative literalとして出現する右側のすべてのClauseのchoiceも、trueの破線辺（青）を選択せざるを得ない*10。

同様に、変数 x_iがnegative literalとして出現する節において変数の真理値割当てをfalseとしたいとすると、上図のpolygraphにおける右側のClauseに付加したchoiceにおいて赤の破線辺を実線と選択することになる。 polygraphにcycleを作りたくないとするとオリジナルのVariableのchoiceにおいてもfalseの破線辺（赤）を選択することになる。 オリジナルのVariableのchoiceがfalseの破線辺（赤）を選択すると、同様に変数 x_iがpositive literalとして出現する左側のすべてのClauseのchoiceも、falseの破線辺（赤）を選択せざるを得ない。

Fan-outによる真理値割当ての伝播は、言うなればドミノ倒しのようなものである。このドミノは2色に塗り分けられていて、倒れたとき表に見える面が選択された辺、真理値となる。 あるClauseにおけるchoiceの真理値割り当てを押す、つまりClauseを構成しない外側の破線辺を選択する、とそれに連鎖してオリジナルのchoice、続いて反対側のすべてのClauseのchoiceに同じ選択が伝播する*11。

choice domino

Fan-outによる伝播は、押すことでしか発生しない。例えばpositive literalとして出現するClause（左側）において真理値割当てを偽と選択した場合には、選択の強制は発生しない（ドミノを引いても伝播しない）。

またあるpositive literalとして出現するClause（左側）の真理値割当てを真と選択したからと言って、positive literalとして出現するほかの（左側の）Clauseのchoiceには影響を与えない。

5 polygraph P(F)が非巡回ならば3-CNF論理式Fは充足可能である*12

polygraph P(F)が非巡回であると仮定する。つまり、polygraph P(F)とcompatibleで非巡回な有向グラフDが存在する。

基本的な考えとして、各変数に対応するVariable（choice）における破線辺の選択をその変数の真理値割当てに対応づくと解釈する。

有向グラフDは非巡回なので、各Clauseを構成する破線辺のうち少なくとも1つは選択されていない。Clauseに閉じて考えれば、Clauseに対応する節をtrueとする真理値割当てが存在することになる。

ここで問題になるのは、各節に閉じてその節をtrueとするような真理値割当てが、論理式全体として矛盾しないかどうか（ある変数に対しては同じ真理値を割当てているか）である。 これをpolygraphの用語で言い換えると、あるVariableとそのすべてのコピーにおけるchoiceが、同じ破線辺（赤or青）を選択するかどうかということである。

このchoiceの選択の強制は、上述のFan-outの機能によって確かめられる。

今考えているのは論理式の充足可能性なので、各節においてtrueとなっているリテラル（≠変数）が重要である。

ある節においてtrueとなっているリテラルを Lとすると、 L に対応するVariableのコピー（choice）においては外側の破線辺を選択したことになる。

これによりドミノが押されるのでFan-outの機能により、リテラル L のVariableに対応するchoiceの選択はpositive/negative表現が反対のすべてのClauseに伝播する。これにより反対側のClauseでは内側の破線辺を選択していることになる。

内側の破線辺を選択することは、そのClauseにおけるローカルなcycleの可能性を増すことになるが、前提より有向グラフDは非巡回である。つまりこの変数が節の充足可能性に寄与しなくても（別のリテラルによって）その節は既にtrueである。

以上より、trueとなっているリテラルによる同じ真理値割当ての強制と、有向グラフDが非巡回であることは両立する。

各節においてfalseとなっているリテラルが存在し得るが、もしそれが他のリテラルの変数に対する真理値割当てと矛盾している場合は、そのリテラルをtrueと置換えた（polygraph P(F)とcompatibleな）別の有向グラフを考えることができる。Fan-outの機能より、同じVariableのコピーであるchoiceにおいて同じ選択をする限り、cycleができることはない。よって真理値割当てを置換えて得られる有向グラフも非巡回である*14。

よって、polygraph P(F)が非巡回ならば、論理式Fを充足する真理値割当てが存在する*15。

6 simple 3-CNF論理式Fが充足可能ならばpolygraph P(F)は非巡回である

simpleな3-CNF論理式Fを充足可能と仮定する。

simpleな3-CNF論理式Fから上記の手順でpolygraph P(F)を構成する。

各変数の真理値割当てに基づき、対応するVariableのchoice、およびそのコピーであるchoiceの破線辺を以下のように選択する。

  • 変数の真理値割当てがtrueの場合は青の破線辺を選択
  • 変数の真理値割当てがfalseの場合は赤の破線辺を選択

ある真理値割当てによって、polygraph P(F)とcompatibleな有向グラフDが得られる。 このDが非巡回であることを示す。

上記の手順で論理式から構築したpolygraphにおけるcycleの可能性は、以下の部分に現れる。

  • 各Clauseにおけるローカルなcycleの可能性
  • 各Fan-outにおけるローカルなcycleの可能性
  • VariableとFan-outを経由する、複数のClauseにまたがるグローバルなcycleの可能性*16

各Clauseのおけるローカルなcycleの存在は、元の論理式を充足する真理値割当てが存在することから否定される*17。

各Fan-outにおけるローカルなcycleの存在は、各変数のchoiceのコピーに同じ真理値割当てを適用することから否定される。

これより、cycleの可能性があるのは複数のClauseを経由するグローバルなcycleのみとなる。

Fan-outによる接続を見るとわかるように、グローバルなcycleを構成しうるClause間のpathは、ある変数がpositive literalとして出現するClauseから同じ変数がnegative literalとして出現するClauseへの方向でしか存在しない。

reachable from positive literal to negative literal

negative literalとして出現するClauseからpositive literalとして出現するClauseへのpathは（choiceの破線辺は同時に有効にならないので）存在しない。

unreachable from negative literal to positive literal

また辺の向きから、positive literalからpositive literalへのpathも、negative literalからnegative literalへのpathも存在しない。

グローバルなcycleが存在するためには、あるClause Cに別のClauseから到着するpathが存在し、またそのClause Cから別のClauseへ出ていくpathが存在する必要がある。pathの方向の制約により、Clause Cには、negative literalとpositive literalの両方が存在する必要がある。

ここで論理式がsimpleであるという条件を利用すると、positive literalとnegative literalの両方を含む節Cが存在しないことになるため、グローバルなcycleは存在しない。

よって、simpleな3-CNF論理式Fが充足可能であるならば、論理式Fから構築されたpolygraph P(F)は非巡回である。

所感

  • 矛盾を積極的に偽に/cycleに倒すテクニックが出てきます。Xの存在を示す問題において矛盾を非Xに倒す、というのがきっとよく使われる方法なのだろうなと想像しました。
  • Fan-outによる接続が重要だと思いますが、ドミノ倒しによる連鎖と、negative→positive方向のpathが存在しないことが両立することをどうやって考えたのか（たまたまそうだったのか）がわかりません。
  • またFan-outでは、節の充足可能性の観点で必要なリテラルにおいてだけドミノが倒れますが、このFan-outの機能が必要十分なのが偶然なのか意図的なのか本質的なのかが気になります。
  • 帰着の手順を見る限り、入力が3-CNFでなくてもCNFでさえあればよいように思いますがどうなんでしょうか。
    • 証明できさえすればよいので、扱いが簡単な3-CNFを選択しただけかもしれません。
  • 当初、Clauseは6角形ではなく破線辺のみの3角形でもよいのではと思いましたが、Clauseの実線辺を除去すると、Clauseを構成する辺を経由しないグローバルcycleができてしまいそうな感じでした。

*1:乗法標準形、和積標準形など

*2:矛盾する真理値割当てによっては論理式全体を充足させないこと

*3:この目的であれば、最後の2mと1のペアはなくてもよさそうであるが

*4:矛盾する真理値割り当てを偽に落として問題ないのかという疑問が生じるが、元の問題が充足可能性問題で真となる真理値割当てが存在するかを問う問題であるので、偽となる真理値割当てが増えることはこの問題に影響を与えない、ということだと思われる

*5:矛盾する真理値割当てによっては論理式全体を充足させないこと

*6:この目的であれば、最後の2mと1のペアはなくてもよさそうであるが

*7:polygraphにおける用語。ぱと隊長さんの記事を参照ください

*8:CNFにおいては、一つでも偽となる節があると論理式全体が偽になる

*9:赤を選択するとFan-outにおいてローカルのcycleができてしまうため

*10:同様にFan-outにおいてローカルのcycleができてしまうため

*11:このように、片側のあるchoiceの選択が反対側のすべてのchoiceの選択に伝播する動きが、Fan-outという名前の由来と思われる

*12:帰着の観点ではこれの証明は不要？

*13:choiceにおいて外側の破線辺を選択することはClauseのローカルcycleの存在を否定します。リテラル LによってオリジナルのVariableの破線辺が選択が逆側になっているので、Fan-outにおけるローカルcycleも存在しません

*14:polygraph P(F)とcompatibleな非巡回有向グラフの中には、矛盾する真理値割当てとなるようなものが存在しうるが、そうであれば同時に必ず、矛盾しない真理値割当てに対応する有向グラフも存在する

*15:真理値割当てが存在する論理式は結果的にすべてsimpleかもしれない・・・？

*16:Fan-outによる接続を見るとわかりますが、ClauseからFan-outを経由し、Variableで折り返してくるようなcycleは（Fan-outのローカルcycleを除いて）存在しません。 つまりグローバルなcycleは必ず複数のClauseを経由します（同じ変数がpositive/negativeの両表現で出現するClauseは存在し得ます）

*17:trueと評価されるリテラルに対するVariableのコピーは外側の破線辺が選択される