2-SAT

2-SAT問題の概要

2-SAT（ツーサット）は、論理式が特定の形式、つまり各節が最大で2つのリテラルで構成されるときに成立するかどうかを判断する問題です。具体的には、リテラルとは変数またはその否定を指し、節はリテラルが「または」で結ばれたもので、全体が「かつ」で結合された形式を連言標準形（2-CNF）と呼びます。この2-SAT問題は、命題論理における満足可能性問題（SAT）の特別なケースです。

問題の背景

2-SATは、SAT問題の一つの制限された形態であり、変数の数や節の数に対して多項式時間で解決可能です。主に用いられる解法は、論理式を含意グラフという有向グラフに変換し、強連結成分を調べる方法です。このプロセスを通じて、与えられた式を真にするための変数の割り当ても効率的に導出可能です。

2-SATの解法においては、充足可能な場合、どのように式を真にするかの具体的な解を同じプロセス内で得られますが、充足割り当ての個数を数える問題である#2-SATは#P完全、満たす節の数を最大化するMAX-2-SATはNP困難であるとされています。2-SATは、例えばラベル配置やクラスタリング、選択肢の組合せにおける制約を表現するのに役立ちます。

具体的な形式と例

2-SAT問題は、下記のような形式で表されます。\[ F = (a_1 \lor b_1) \land (a_2 \lor b_2) \land ... \land (a_m \lor b_m) \] ここで、\(a_j\)と\(b_j\)はリテラルであり、\(m\)は節の数です。単なるリテラルからなる節は単位節と呼ばれ、リテラルを含まない節は空節と呼ばれます。空節は充足不能な式を意味し、すべてのリテラルの割り当てについての条件が強い制約を設けるものです。

具体例を挙げると、\[ F = (x \lor y) \land (
eg x \lor y) \land (x \lor
eg y) \] という2-CNF式は、\(x = y = 1\)という割り当てを設定するとすべての節を満たすため充足可能です。

一方で、\[ H = (x \lor y) \land (x \lor
eg y) \land (
eg x \lor y) \land (
eg x \lor
eg y) \] という式は、充足可能な割り当てが存在しません。これは、いかなる割り当てをしても常に偽になる節を含んでいるためです。

含意グラフの観点

含意グラフを用いた解法は、節を有向辺で表現する有力な手段です。例えば、\(a \lor b\) という節は、\(
eg a \Rightarrow b\) および \(
eg b \Rightarrow a\) という2つの有向辺からなるグラフとして表せます。全てのリテラルを考慮した上で、強連結成分を確認し、それぞれの変数とその否定が同じ成分に属しないことが充足条件となります。

強連結成分の判定は、深さ優先探索を基にして行われ、効率的な多項式時間計算が可能です。この結果、2-SATはNL完全であり、特定の条件下であれば効率的に解を得られます。

応用案例

2-SATは多くの現実世界の問題に応用されています。特に、ラベルの配置や集積回路の一部としての選択肢の管理に利用されます。例えば、地下鉄の駅においては、各駅のラベルを適切に配置するための条件を2-SATで表現することができ、候補となるラベルが互いに重ならないように選ばれることは、適切な制約の表現によって実現可能です。

このような2-SATの理論と技術は、お絵かきロジックや日程調整の問題など、様々な分野において役立っています。さらなる研究や実用的な応用が期待されます。

もう一度検索