The Complexity of Minimizing Wire Lengths in VLSI Layouts
タイトル練り直せ
Theorem
最大次数が4の木をグリッドに埋め込めるかはNP-Complete
証明
not-all-equal 3satに帰着する。これは、3CNF式が与えられたときに、各clauseに少なくともひとつfalseになるリテラルが含まれるように充足可能か、という問題。
つまり、3CNF式が与えられたときに、それから最大次数が4の木を構成し、木がグリッドに埋め込める iff not-all-equal 3satの充足が存在する、という感じにしたい。
準備
以下のような木は向きの自由を無視して、一意な埋め込みがあります。また、これをつなげたもの（右）も一意な埋め込みになります。
3SATから木を構成
個の変数が存在するとして、横に
個、上下に長さ
の骨格をつくる。骨格の端は、これから先に追加する枝の方向を確定させるためのもの（必ず横向きになるように）。
ここから、間の列について、clauseからなる制約を付け加えていく。具体的には、
番目のclauseに
が登場しない場合、対応する箇所（下画像参照）に横棒(striker)を一つ足す。
さて、こうして構成されたグラフについて、グリッドに埋め込めるかどうかと、もとのCNF式にnot-all-equal-3sat充足が存在するかが等価になることを示す。
ポイントとしては、間の列に関して、上下を逆にしてもグラフとして同型ということである。また各骨格について、左右反転させたものも同型になるという点が重要である。結果的にある埋め込みが存在したとき、上になっている方をTrue, 下になっている方をFalseとした充足が存在することになる。
さて、各clauseについて、変数は3つある(と
があれば無視できるので、異なる変数が3つ、と考えて良い)ので、各行について、clauseに登場しない変数分として
本のstrikerが存在する。これについて、各変数がもしすべてtrueの場合、3本のstrikerが追加され、
本のstrikerになってしまう。一方、そうでない場合、strikerは
本以下である。
いま、strikerを埋め込める箇所は、free columnと呼ばれる箇所しかない。したがって、もしnot-all-equal-3satが充足可能でない場合、平面埋め込みが存在しない。
逆にnot-all-equal-3satが充足可能である場合、trueのものを上にし、falseのものを下にした場合、上述する性質を満たすような埋め込みが存在する（証明終了）
ウ ン チ ー コ ン グ
一応背景としては、木をmaximum edge length(とは?)を最小化して埋め込みたい、というものがあったっぽい。さすがに追わないと思う。 あと、complete binary treeで一意なうめこみがあるものがあるらしく(31頂点とか。ほかはしらんけどまあ似たような感じでしょ)、その場合についても本定理を拡張できるらしい。しらんけど。
ウ ン チ ー コ ン グ ！
