not-all-equal-3sat系証明のテクニック

グリッドグラフの描画とか、horizontalとverticalしか使っちゃだめ系描画など、一般に「自由度が相対的に制限される」ようなセッティングにおける可能性判定の証明に使える気がする。

証明のテクは、「必ずこの配置しかありえない」ような配置を組み合わせ、これから追加できる要素の配置を一通りに制限する。

not-all-equal-3satのインスタンスを目的のアルゴリズム(NP-Completeであると証明したいもの)を使って解くことを考える。

not-all-equal-3satの本質は、各clauseについて、すべてをtrueにしてはいけないということで、上述したような、配置が固定されるオブジェクトをうまく組み合わせ、個の隙間に要素を敷き詰めるような設定を作る。これで、もし目的のアルゴリズムで敷き詰めが可能かどうか判定できるならnot-all-equal-3satが解けてしまう、という流れにする。