SAT の色んなガジェット
色んな 3 SAT について考えていく中で見つけたガジェットを書いていく 着目する構造
SAT / UnSAT 判定を難しくしている原因は「別の名前の変数が同じ値を取っており、実質的に新たな節を形成している」ような 3 変数の組が存在するためだと考えられるので、それらの組によりできた 暗節 に着目する $ =,\neで結ばれた変数は強連結になって連鎖的に解が求まるので、これも見つける
const: True False は充足不能性につながるのでこれも見つける 凡例
黒いノードが節(Closure)
黒くないノードが変数(Variable)
literal でも良いが、正 縛りにしているので、変数とする 別の黒いノードと共有する頂点は同じ変数
$ \lbrack\lbrace x_1,x_2,x_3\rbrace,\lbrace x_1,x_4,x_5\rbrace\rbrack
https://gyazo.com/8b35dbef1bc0c7467e4662aca19fd8c7
同じ色の変数は分析すると同じ値を取る事がわかる変数
頂点として重なっていないから違う変数だが、実は同じ値を取る
https://gyazo.com/253a173ef7f77e6a87f4249d4d3928b6
描画のためのさらなる縛り
節を黒三角で描いていた頃の縛りが名残として残っている
節同士が 2 変数を共有してはならない (線と塗を違う色にする必要があって面倒)
節同士が 2 変数を共有していても別に良い
exactly 3 SAT ではなくても別に良い
checker-grid 上に描いたときの辺の長さは 1 のみを認める
こうすると図を描くときの法則としてキレイ
無視して長い線を書く場合は見た目がキレイ
同じ変数を共有する節は 3 つか、4 つか
checker-grid 上に描くので多くとも 4 つ
三角形の頃の名残で 3 つに縛っても良い気もする
全部切り出した