🔖

2-SATを解く

2023/12/18に公開

この記事は「木 Advent Calendar 2023」の18日目です。
きのうの記事はうえきさんの「木のおもしろあるあるを書きました！」でした。
あしたの記事はまぐふらいさんの「LowLinkの紹介」です。

今日は真面目な記事なので真面目に書きます。

2-SAT とは

まずは SAT (充足可能性問題) について
説明は Wikipedia に譲ります（上のリンクをクリック！）

2-SAT (CNF-SAT のうち、節内のリテラルが高々 $2$ 個の場合）は、強連結成分分解を使うことにより、変数の数 $N$ と節の数 $M$ に対して $O(N + M)$ で解くことができます^[1]。

本記事ではこの 2-SAT について、与えられた論理式の充足可能性を判定する方法と、充足する割当を計算する方法を紹介します。
ちなみに、 2-SAT の割当の数え上げは ♯P-complete であり、効率的に解く方法は存在しないと考えられています。

2-SAT における充足可能性の判定は、論理式を有向グラフに変換することにより行います。
この有向グラフは含意グラフ (implication graph) と呼ばれ、論理式における $A \to B$ の関係を有向辺で表したものです。

論理式を含意グラフに変換するには、以下の通りの手順をたどります。

まず、それぞれの変数と、それぞれの変数の否定に対応する $2N$ 個の頂点をつくる。
- たとえば、変数が $x, y, z$ であるとき、これらの変数にくわえ、 $\bar{x}, \bar{y}, \bar{z}$ に対応する頂点も作る。
それぞれの節 $(A \vee B)$ に対して、辺 $\bar{A} \to B$ と辺 $\bar{B} \to A$ を追加する。
- たとえば、 $(x \vee y)$ なら、 $\bar{x} \to y$ と $\bar{y} \to x$ を追加する。
- $(x \vee \bar{y})$ なら、 $\bar{x} \to \bar{y}$ と $y \to x$ を追加する。
- もし節が $(A \to B)$ と表されているなら、 $A \to B$ と $\bar{B} \to \bar{A}$ を追加する。

これで含意グラフができました。

含意グラフ上で $A$ から $B$ へのパスがあるとき、 $A \to B$ が真となるべきことを意味します。（ $\bar{B} \to \bar{A}$ については別途指定する必要があることに注意）

論理式を含意グラフに変換してみましょう。

$(\bar x \vee y) \wedge (\bar y \vee z) \wedge (\bar z \vee x)$
x→y→z→x

$(\bar x \vee \bar y) \wedge (y \vee z) \wedge (\bar y \vee z)$

解答

含意グラフ上で $x$ と $\bar{x}$ を両方含むパスがあるとします。
（仮にそのようなパスがなければ、 $x$ に $0, 1$ どちらを代入しても充足可能です。）
すると、以下の3通りが考えられます。

(a) $x \to \bar x$ のパスのみある。
- この場合、 $x = 1$ かつ $\bar x = 0$ であってはならないため、 $x = 0$ とします。
(b) $\bar x \to x$ のパスのみある。
- この場合、 $\bar x = 1$ かつ $x = 0$ であってはならないため、 $x = 1$ とします。
(c) $x \to \bar x$ と $\bar x \to x$ のパスが両方ある。（つまり、 $x$ と $\bar x$ が同じ強連結成分内にある）
- この場合、充足可能な割当は存在しません。
  このように各変数について割当を行うことで、解を求めることができます。

上に示したことは、含意グラフを強連結成分分解・トポロジカルソートすることで求めることができます。
(c) についてはそのまま判定すればよいです。
ただし (a), (b) については、 DAG 上で 2 点間を結ぶパスが存在するかの判定を行うと時間がかかるため、単にトポロジカル順で判定します。

含意グラフの頂点は $O(N)$ 個、辺は $O(M)$ 本であるため、このようにして計算量 $O(N+M)$ で解くことができます。

ノーコメントとさせていただきます。

脚注