2-SAT

論理式の形式

真を1、偽を0と表す。変数 ${\displaystyle x}$ とその否定 ${\displaystyle \neg x}$ の真偽値は互いに反対である。節を真にするには、それに含まれるリテラルの少なくとも1個が真であればよい。式全体を真にする割り当てを充足割り当てと呼び、それが存在する式を充足可能という^[8]。

2個のリテラルを持つ節を用いると、2-CNF式は

$${\displaystyle F=\bigwedge _{j=1}^{m}(a_{j}\lor b_{j})}$$

と表せる。ここで ${\displaystyle a_{j},b_{j}}$ はリテラル、${\displaystyle m}$ は節数であり、${\displaystyle \lor }$ は論理和、${\displaystyle \bigwedge }$ は論理積を表す。リテラル1個からなる節は単位節という。単位節 ${\displaystyle a}$ は ${\displaystyle a\lor a}$ と同値なので、反復を許せば2個のリテラルを持つ節として扱える^[2][8]。

リテラルを含まない節を空節という。空節を認める定義では、空節は偽を表すため、それを含む式は充足不能である。節がまったくない式は真とする^[4]。以下の含意グラフによる判定では、空節を持つ入力を先に充足不能と判定する。

禁止される組合せによる表現

異なる2変数 ${\displaystyle x,y}$ を含む節は、4通りの割り当てのうち1通りを禁止する制約として読むこともできる。各変数またはその否定を組み合わせると、禁止する割り当てを次のように指定できる。

節と禁止される割り当て

節	禁止される ${\displaystyle (x,y)}$ の値
${\displaystyle x\lor y}$	${\displaystyle (0,0)}$
${\displaystyle x\lor \neg y}$	${\displaystyle (0,1)}$
${\displaystyle \neg x\lor y}$	${\displaystyle (1,0)}$
${\displaystyle \neg x\lor \neg y}$	${\displaystyle (1,1)}$

このため、2通りの選択肢を持つ対象が複数あり、2対象の選択の組合せに禁止条件がある問題は、その条件を節に変換して2-SATで表現できる。同じ値を要求する条件 ${\displaystyle x=y}$ は ${\displaystyle (\neg x\lor y)\land (x\lor \neg y)}$、異なる値を要求する条件 ${\displaystyle x\neq y}$ は ${\displaystyle (x\lor y)\land (\neg x\lor \neg y)}$ と表せる。

具体例

例えば、

$${\displaystyle F=(x\lor y)\land (\neg x\lor y)\land (x\lor \neg y)}$$

は2-CNF式であり、${\displaystyle x=y=1}$ とすればすべての節が真になる。一方、

$${\displaystyle H=(x\lor y)\land (x\lor \neg y)\land (\neg x\lor y)\land (\neg x\lor \neg y)}$$

には充足割り当てがない。4通りの割り当てを調べると、${\displaystyle x=y=0}$ では第1節、${\displaystyle (x,y)=(0,1)}$ では第2節、${\displaystyle (x,y)=(1,0)}$ では第3節、${\displaystyle x=y=1}$ では第4節が偽になる^[9]。

7変数の例

図による説明の例として、7個の変数 ${\displaystyle x_{0},\ldots ,x_{6}}$ と11個の節からなる式

$${\displaystyle {\begin{aligned}J={}&(x_{0}\lor x_{2})\land (x_{0}\lor \neg x_{3})\land (x_{1}\lor \neg x_{3})\\&\land (x_{1}\lor \neg x_{4})\land (x_{2}\lor \neg x_{4})\\&\land (x_{0}\lor \neg x_{5})\land (x_{1}\lor \neg x_{5})\land (x_{2}\lor \neg x_{5})\\&\land (x_{3}\lor x_{6})\land (x_{4}\lor x_{6})\land (x_{5}\lor x_{6})\end{aligned}}}$$

を考える。すべての変数を1にすれば式は真になる。この式の含意グラフと充足割り当ての集合を、以下の節の図に示す。

グラフの構成

節 ${\displaystyle a\lor b}$ は含意 ${\displaystyle \neg a\Rightarrow b}$ と同値であり、${\displaystyle \neg b\Rightarrow a}$ とも同値である。この関係を使い、${\displaystyle n}$ 個の変数について、各変数とその否定に対応する ${\displaystyle 2n}$ 個の頂点を設ける。各節 ${\displaystyle a\lor b}$ に対し、

$${\displaystyle \neg a\longrightarrow b,\qquad \neg b\longrightarrow a}$$

の2本の有向辺を加える。こうして得られる有向グラフが含意グラフである。充足割り当てでは、ある頂点のリテラルが真なら、その頂点から有向路で到達できるリテラルも真になる^[2]。単位節 ${\displaystyle a}$ に対応する辺は ${\displaystyle \neg a\longrightarrow a}$ となる。

強連結成分による判定

有向グラフで、どの2頂点の間にも両方向の有向路が存在するような極大の頂点集合を強連結成分という。2-CNF式が充足可能であるための必要十分条件は、どの変数 ${\displaystyle x}$ についても、${\displaystyle x}$ と ${\displaystyle \neg x}$ が同じ強連結成分に属さないことである^[2][3.1]。

両者が同じ成分に属する場合、${\displaystyle x}$ を真にすると含意の連鎖によって ${\displaystyle \neg x}$ も真になり、${\displaystyle x}$ を偽にすると逆に ${\displaystyle x}$ が真になる。このため、どちらの値を割り当てても矛盾する^[2][3.1]。

条件が満たされている場合には、強連結成分をそれぞれ1頂点に縮約して得られる、閉路を持たない有向グラフを使って割り当てを構成できる。辺の始点が終点より先になるように成分を並べるトポロジカル順序を求め、その逆順で未割り当ての成分を真、対応する否定の成分を偽とする。含意グラフでは ${\displaystyle a\longrightarrow b}$ に対して ${\displaystyle \neg b\longrightarrow \neg a}$ も存在するため、成分内の全リテラルの否定も1個の成分にまとまる。この構造により、すべての含意を満たす割り当てが得られる^[2][3.1]。

成分のトポロジカル順序を番号で表すこともできる。成分間に辺があれば、その始点の成分の番号が終点の成分の番号より小さくなるように番号を付け、リテラル ${\displaystyle a}$ が属する成分の番号を ${\displaystyle c(a)}$ とする。上の必要十分条件を満たす場合、各変数 ${\displaystyle x}$ の値を

$${\displaystyle x=1\quad \Longleftrightarrow \quad c(x)>c(\neg x)}$$

と定めると、充足割り当てが得られる^[3.1]。

強連結成分を求める方法の一つは、深さ優先探索を2回行うものである。まず含意グラフを探索し、各頂点からの探索を終えた順を記録する。次に、すべての辺を逆向きにしたグラフで、記録した順の逆順に未訪問の頂点から探索を始める。この2回目の各探索で新たに訪れる頂点の集合が、それぞれ1個の強連結成分になる。未訪問の頂点がなくなるまで繰り返すと、成分の発見順は、元のグラフで成分を縮約した有向非巡回グラフのトポロジカル順序にもなる^[3.2]。

具体例の含意グラフ

上の充足可能な式 ${\displaystyle F}$ から得られる辺は次のとおりである。

節	対応する有向辺
${\displaystyle x\lor y}$	${\displaystyle \neg x\longrightarrow y}$、${\displaystyle \neg y\longrightarrow x}$
${\displaystyle \neg x\lor y}$	${\displaystyle x\longrightarrow y}$、${\displaystyle \neg y\longrightarrow \neg x}$
${\displaystyle x\lor \neg y}$	${\displaystyle \neg x\longrightarrow \neg y}$、${\displaystyle y\longrightarrow x}$

このグラフの強連結成分は ${\displaystyle \{x,y\}}$ と ${\displaystyle \{\neg x,\neg y\}}$ であり、後者から前者への辺がある。前者のリテラルを真、後者を偽とすれば、${\displaystyle x=y=1}$ の充足割り当てが得られる。式 ${\displaystyle H}$ では、さらに ${\displaystyle x\longrightarrow \neg y}$ と ${\displaystyle y\longrightarrow \neg x}$ が加わり、4頂点が同じ強連結成分に入る。

7変数の例の含意グラフ

式 ${\displaystyle J}$ の第1節 ${\displaystyle x_{0}\lor x_{2}}$ からは ${\displaystyle \neg x_{0}\longrightarrow x_{2}}$ と ${\displaystyle \neg x_{2}\longrightarrow x_{0}}$ が得られる。第2節 ${\displaystyle x_{0}\lor \neg x_{3}}$ からは ${\displaystyle \neg x_{0}\longrightarrow \neg x_{3}}$ と ${\displaystyle x_{3}\longrightarrow x_{0}}$ が得られる。図では、残りの節についても同じ規則で辺を加えている^[2]。

この例の含意グラフには有向閉路がなく、各頂点がそれぞれ1個の強連結成分となる。したがって、変数とその否定が同じ成分に入ることはなく、式は充足可能である。

計算量

含意グラフは ${\displaystyle 2n}$ 個の頂点と高々 ${\displaystyle 2m}$ 本の辺を持つ。通常の隣接リスト表現では、グラフの構成、強連結成分の計算、各変数と否定の成分の比較、真偽値の割り当ては、合計 ${\displaystyle O(n+m)}$ 時間で実行できる。これは、変数数と節数の和に比例する線形時間という意味である^[2][3.1]。

導出原理

導出原理は、ある変数とその否定をそれぞれ含む2個の節から、残りのリテラルを含む節を導く推論規則である。例えば、${\displaystyle a\lor b}$ と ${\displaystyle \neg b\lor c}$ からは ${\displaystyle a\lor c}$ が導かれる。元の2節を満たす割り当ては導かれた節も満たすため、その節を式に加えても充足割り当ての集合は変わらない^[4]。

この操作によって得られる新しい節を、追加できなくなるまで加える。導出原理の完全性により、空節が得られる場合に限り元の式は充足不能である。2-CNF式から導かれる節も高々2個のリテラルを持ち、${\displaystyle n}$ 変数で作れる異なる節の数は ${\displaystyle O(n^{2})}$ である。このため、節の組を調べて新しい節を加える方法でも、多項式時間で判定できる^[4]。含意グラフでは、${\displaystyle \neg a\longrightarrow b\longrightarrow c}$ という2段階の含意から ${\displaystyle \neg a\longrightarrow c}$ を得る操作に対応する。

単位伝播

単位節に含まれるリテラルを真とする割り当てを行い、真になった節を取り除き、ほかの節から偽になったリテラルを取り除く。この簡約を、新しい単位節がなくなるまで繰り返す操作を単位伝播（英語版）という。空節が生じれば矛盾が検出され、節がすべてなくなれば充足割り当てが得られる^[8]。

2-CNF式では、まず既存の単位節を伝播し、未割り当ての変数 ${\displaystyle x}$ が残っていれば ${\displaystyle x=1}$ を仮定して再び伝播する。矛盾が生じた場合は、その仮定とそれに基づく割り当てを取り消し、${\displaystyle x=0}$ として伝播する。こちらでも矛盾すれば充足不能である。矛盾が生じない場合は、得られた割り当てを保持して残りの式に同じ操作を繰り返す。2-CNF式では、矛盾を生じない仮定と伝播の後の式が充足可能であることと、操作前の式が充足可能であることは同値になる。この性質により、過去の矛盾しなかった仮定へ戻って探索し直す必要がなく、多項式時間で判定できる^[8]。

1976年の線形時間解法では、${\displaystyle x=1}$ と ${\displaystyle x=0}$ の両方から含意の伝播を並行して進める。片方の処理で矛盾が見つかれば他方を試し、片方が矛盾なく完了すれば他方の処理を打ち切って、その部分割り当てを確定する。原論文は、含意を調べるための適切なデータ構造を用いると、この方法を線形時間で実行できるとしている^[5][10]。

乱択アルゴリズム

任意の割り当てから始め、偽になっている節を1個選び、その節の2個のリテラルの一方を等確率で選んで、対応する変数の値を反転する方法もある。充足可能な式については、充足割り当てが得られるまでの反転回数の期待値は高々 ${\displaystyle n^{2}}$ であり、${\displaystyle 2n^{2}}$ 回の反転で見つけられる確率は少なくとも ${\displaystyle 1/2}$ となる^[11]。

この方法は、発見した割り当てが式を充足することを確認して成功を報告する。一方、打ち切りまでに発見できなかったことは、充足不能の証明にはならない。独立に繰り返すことで、充足可能な入力を見逃す確率を小さくできる^[11]。

判定問題

2-SATは、多項式時間で判定できる問題のクラスPに属する。各節を高々3個のリテラルに拡張した3-SATはNP完全であり、節の大きさの制限は計算複雑性に関わる^[8]。NPは、肯定的な答えを裏付ける解候補を多項式時間で検証できる判定問題のクラスである。NP完全な問題はNPに属し、NPのどの問題も、その問題へ多項式時間で変換して解くことができる^[13]。

対数領域での計算に着目すると、2-SATは対数領域還元の下でNL完全である。NLは、入力長に対して対数程度の作業領域を使う非決定性計算によって判定できる問題のクラスである。NL完全とは、このクラスに属し、クラス内のどの問題も、対数領域で計算できる変換によってその問題へ還元できることをいう^[6]。

NL完全性は、有向グラフにおける到達可能性との関係からも説明できる。グラフ ${\displaystyle G=(V,E)}$ と頂点 ${\displaystyle s,t}$ に対し、頂点 ${\displaystyle v}$ ごとに変数 ${\displaystyle p_{v}}$ を用意し、

$${\displaystyle \Psi =p_{s}\land \neg p_{t}\land \bigwedge _{(u,v)\in E}(\neg p_{u}\lor p_{v})}$$

を作る。${\displaystyle s}$ から ${\displaystyle t}$ への有向路があれば、${\displaystyle p_{s}=1}$ から含意をたどって ${\displaystyle p_{t}=1}$ となるため、この式は充足不能である。有向路がなければ、${\displaystyle s}$ から到達できる頂点の変数を真、残りを偽とすれば式を充足する。したがって、到達不能の判定を2-SATへ還元できる。式を生成する変換は対数領域で実行でき、NLに属する問題の答えを反転した問題もNLに属するという性質と合わせて、2-SATのNL困難性が得られる^[6]。

充足割り当ての集合

2-CNF式の充足割り当ての集合は、変数ごとの多数決に関して閉じている。すなわち、3個の充足割り当て ${\displaystyle u,v,w}$ を選び、各変数の値を、その3個の割り当てのうち少なくとも2個で採用されている値にすれば、得られる割り当ても元の式を満たす。この性質は中央値演算に関する閉性として述べられ、有限個のブール変数の割り当て集合がこの演算に関して閉じていることと、その集合をある2-CNF式の解集合として表せることは同値である^[14]。

多数決で得られた割り当てが解になることは、節ごとに確認できる。3個の解はいずれも節 ${\displaystyle a\lor b}$ を満たすので、${\displaystyle a,b}$ の少なくとも一方は2個以上の解で真になる。そのリテラルは多数決後も真になり、節は満たされる。単位節についても同様である^[14]。

空でない有限の解集合には、この中央値演算から中央値グラフと呼ばれるグラフを対応させられる。中央値グラフでは、任意の3頂点に対し、それぞれの頂点対を結ぶ最短路のいずれかに共通して含まれる頂点がただ1個存在する^[14]。図は式 ${\displaystyle J}$ の解集合を表す中央値グラフである。この例では1変数の反転が辺に対応するが、一般の2-CNF式で1変数ずつ反転してすべての解を行き来できるとは限らない。例えば ${\displaystyle (\neg x\lor y)\land (x\lor \neg y)}$ の解は ${\displaystyle (0,0)}$ と ${\displaystyle (1,1)}$ であり、両者の間を移るには2変数を同時に反転する必要がある。

計数と最大化

充足割り当ての個数を数える問題を#2-SATという。この問題は#P完全である^[1]。#Pは、多項式時間で検証でき、長さも入力長の多項式で抑えられる解候補の個数を求める関数のクラスである。ここでいう#P完全とは、そのクラスに属し、クラス内の任意の計数問題を、多項式時間の計算とその問題への問い合わせによって解けることをいう^[15]。

すべての節を満たせるかではなく、同時に満たす節数を最大化する問題はMAX-2-SATと呼ばれ、NP困難である。3-SATからの多項式時間の還元があるため、MAX-2-SATを多項式時間で厳密に解ければ、3-SATも多項式時間で解ける^[16]。判定、計数、最大化では、同じ2-CNF式を入力としても異なる計算問題が得られる。

MAX-2-SATの近似

MAX-2-SATには、最適な節数を厳密に求める方法のほか、最適値に対して一定の割合以上の節を満たす割り当てを求める近似アルゴリズムがある。各節が異なる2変数を含む場合、各変数を独立に等確率で0または1にすれば、各節が真になる確率は ${\displaystyle 3/4}$ である。節数が ${\displaystyle m}$ なら満たす節数の期待値は ${\displaystyle 3m/4}$ となり、最適値は ${\displaystyle m}$ 以下なので、最適値に対しても期待値で少なくとも ${\displaystyle 3/4}$ を保証する^[17]。

1995年には、半正定値計画法で緩和した解を乱択的に丸めることで、満たす節数の期待値が最適値の少なくとも約0.87856倍となる多項式時間アルゴリズムが示された^[18]。この研究の予備版は1994年に発表され、1995年に論文誌へ掲載された^[18]。その後の研究では丸め方の改良も検討され、2002年のアルゴリズムについて約0.9401という近似率が報告されている。2007年の研究では、各変数の肯定と否定の出現の重みが等しい場合と、偏りがある場合を区別して、近似可能性と近似困難性が調べられた^[19]。

真にする変数の個数と重み

2-CNF式を充足するという条件に加えて、真にする変数の個数を最小化する問題はNP困難である。これは頂点被覆問題を含む。無向グラフの頂点 ${\displaystyle v}$ ごとに変数 ${\displaystyle x_{v}}$ を設け、辺 ${\displaystyle uv}$ ごとに節 ${\displaystyle x_{u}\lor x_{v}}$ を加えると、真にした変数に対応する頂点の集合は、すべての辺の少なくとも一端を含む頂点被覆となる。したがって、真にする変数の個数の最小化は、この場合には頂点被覆の大きさの最小化に相当する^[20]。

変数 ${\displaystyle x_{i}}$ に実数の重み ${\displaystyle w_{i}}$ を与え、充足割り当てのうち

$${\displaystyle \sum _{i:x_{i}=1}w_{i}}$$

を最小化または最大化する問題もNP困難である。これは変数に重みを与える問題であり、MAX-2-SATで満たした節の数、または満たした節の重みの和を最大化する問題とは目的関数が異なる^[20][19]。

別の定式化として、2-CNF式と整数 ${\displaystyle k}$ を入力し、ちょうど ${\displaystyle k}$ 個の変数を真にする充足割り当てがあるかを問う重み付き2-SATがある。ここでは「重み」は真にした変数の個数を意味する。この問題は、${\displaystyle k}$ をパラメータとする計算量の分類でW[1]完全である^[21]。パラメータ化計算量では、入力長 ${\displaystyle L}$ に対し ${\displaystyle f(k)L^{c}}$ 時間で解け、定数 ${\displaystyle c}$ が ${\displaystyle k}$ に依存しない問題を固定パラメータ容易という。W[1]完全性は、この重み付き2-SATにそのようなアルゴリズムが存在すれば、W[1]に属するすべての問題も固定パラメータ容易になることを意味する^[21]。

量化された式

変数に存在量化子 ${\displaystyle \exists }$ または全称量化子 ${\displaystyle \forall }$ を付けた式の真偽を判定する問題も考えられる。存在量化は式を真にする値が存在すること、全称量化は両方の真偽値について式が真であることを表す。通常の2-SATは、すべての変数を存在量化した場合に相当する。量化子を式の先頭に置き、その後に2-CNF式を置いた形では、存在量化と全称量化が混在していても、強連結成分を用いる方法を拡張して線形時間で真偽を判定できる^[2]。

ラベル配置

2-SATは、候補の選択と、候補同士の両立しない組合せの禁止を論理式で表すために用いられる。例えば地下鉄路線図のラベル配置では、各駅について2個のラベル位置候補を残し、各駅からちょうど1個を選び、選んだラベルが重ならない配置を求める部分問題を2-SATとして表せる^[23]。

候補ごとに「採用するなら真」となる変数を設ける。2候補を ${\displaystyle p,q}$ とすると、ちょうど1個を選ぶ条件は

$${\displaystyle (p\lor q)\land (\neg p\lor \neg q)}$$

で表せる。また、候補 ${\displaystyle p}$ と ${\displaystyle r}$ が重なるなら ${\displaystyle \neg p\lor \neg r}$ を加え、路線と交差する候補 ${\displaystyle p}$ を禁止するなら単位節 ${\displaystyle \neg p}$ を加える。これらはいずれも2-CNFの節であり、同時に満たす配置の有無を判定できる^[23]。

生成した論理式の判定は変数数と節数に対して線形時間であるが、候補のすべての組の重なりを制約にすると、駅数を ${\displaystyle N}$ として節数は ${\displaystyle O(N^{2})}$ になり得る。したがって、制約の生成を含む配置判定の時間は、駅数に対して線形とは限らない^[23]。

グラフの描画と集積回路の配線

グラフの頂点の位置を固定し、各辺を2通りの円弧のいずれかで描くとき、交差のない描画を選べるかという問題は2-SATに還元できる。各辺に1個の変数を対応させ、交差を生じる円弧の組合せを節で禁止する。平面グラフの頂点数を ${\displaystyle N}$ とすると、この直接的な方法は ${\displaystyle O(N^{2})}$ 時間で判定する。幾何的な探索構造を用い、含意関係をすべて列挙せずに探索することで、計算時間を短縮する方法も示されている^[24]。

集積回路の配線にも同じ考え方を適用できる。端点の組を水平・垂直の線分で結び、曲がる回数を高々1回とする場合、各配線には通常2通りの経路がある。1層にすべての配線を交差なく収められるかどうかは、経路の選択を変数にし、配線間の干渉を高々2リテラルの節で表して判定できる。1986年の研究では、この方法による ${\displaystyle O(N^{2})}$ 時間のアルゴリズムが示された。ここで ${\displaystyle N}$ は配線の本数である^[25]。

改名可能ホーン式の判定

ホーン節は、否定されていない変数を高々1個含む節である。各節がホーン節であるCNF式をホーン式という。各節の長さに上限はない。一部の変数について、その変数と否定の出現を式全体で入れ替えることでホーン式になるCNF式は、改名可能ホーン式と呼ばれる^[26]。

この変換が可能かどうかは、補助的な2-SATを使って判定できる。原変数 ${\displaystyle x}$ ごとに「${\displaystyle x}$ の肯定と否定を入れ替えるなら1」となる変数 ${\displaystyle s_{x}}$ を設ける。同じ原節に現れる任意の2リテラルが、変換後に同時に肯定形にならないことを条件にする。例えば原節 ${\displaystyle x\lor y\lor \neg z}$ に対しては、

$${\displaystyle (s_{x}\lor s_{y})\land (s_{x}\lor \neg s_{z})\land (s_{y}\lor \neg s_{z})}$$

を加える。この条件を全節のリテラルの組について作れば2-CNF式が得られ、その充足割り当てが、ホーン式に変換するための入れ替え方を与える^[26]。

2クラスタの直径制約

点集合を高々2個のクラスタに分け、各クラスタの直径を指定された非負の上限以下にする問題も2-SATで表せる。クラスタの直径は、その中にある2点間の距離の最大値であり、1点だけのクラスタでは0とする。点 ${\displaystyle i}$ の変数を ${\displaystyle p_{i}}$ とし、第1クラスタに属するなら真、第2クラスタに属するなら偽とする^[27]。

直径の上限がそれぞれ ${\displaystyle D_{1},D_{2}}$ のとき、距離 ${\displaystyle d(i,j)}$ が ${\displaystyle D_{1}}$ を超える点の組には ${\displaystyle \neg p_{i}\lor \neg p_{j}}$ を加え、両方が第1クラスタに入ることを禁止する。同様に、${\displaystyle d(i,j)>D_{2}}$ なら ${\displaystyle p_{i}\lor p_{j}}$ を加える。得られた式を満たす割り当ては、指定された直径制約を満たす振り分けに対応する。空になった集合はクラスタとして数えない。点数を ${\displaystyle N}$ とすると、調べる点対と生成する節の数は ${\displaystyle O(N^{2})}$ なので、この可否判定は ${\displaystyle O(N^{2})}$ 時間で行える^[28]。

このような可否判定は、クラスタの直径の和を最小化する手法にも用いられる^[27]。1987年の研究では、2個の非空クラスタの直径の和を最小化する ${\displaystyle O(N^{3}\log N)}$ 時間のアルゴリズムが示された。この方法は、直径の候補をグラフの構造から絞り込み、上限の組に対する可否判定を繰り返すものである^[28]。

2通りの時間帯の選択

日程調整でも、各予定に2通りの時間帯があり、選んだ時間帯が互いに重ならないようにする問題は2-SATで表せる。例えば、開始時刻 ${\displaystyle S_{i}}$、終了時刻 ${\displaystyle T_{i}}$ の結婚式ごとに、所要時間 ${\displaystyle D_{i}}$ の式典を最初か最後に置き、同じ担当者がすべての式典に出席する問題がある。候補となる時間帯は ${\displaystyle [S_{i},S_{i}+D_{i})}$ と ${\displaystyle [T_{i}-D_{i},T_{i})}$ であり、ある式典の終了時刻と別の式典の開始時刻が等しい場合は、両方に出席できるものとする。また、会場間の移動時間は考慮しない^[3.3]。

変数 ${\displaystyle x_{i}}$ を、式典を最初に置くなら真、最後に置くなら偽とする。結婚式 ${\displaystyle i,j}$ の最初の時間帯どうしが重なる場合には、節 ${\displaystyle \neg x_{i}\lor \neg x_{j}}$ を加え、両方で最初を選ぶことを禁止する。最初と最後、最後と最初、最後どうしについても同様に、時間帯が重なる選択の組を節で禁止する。これらの節をすべて満たす割り当てがあれば、それに対応する時間帯を選ぶことで日程を組める^[3.3]。

具体例として、1組目の結婚式が8時から9時までで式典に30分、2組目が8時15分から9時までで式典に20分かかる場合を考える。時間帯の重なりから得られる式は

$${\displaystyle (\neg x_{1}\lor \neg x_{2})\land (x_{1}\lor \neg x_{2})\land (x_{1}\lor x_{2})}$$

であり、充足割り当ては ${\displaystyle x_{1}=1,x_{2}=0}$ となる。したがって、1組目の式典を8時から8時30分、2組目を8時40分から9時に置けば、担当者は両方に出席できる^[3.3]。

学校の時間割

学校の時間割を組む問題では、教師 ${\displaystyle i}$ とクラス ${\displaystyle j}$ の組ごとに必要な授業数 ${\displaystyle R_{ij}}$ が与えられ、双方が利用できる時間帯に授業を割り当てる。教師が同時に複数のクラスを教えたり、クラスが同時に複数の授業を受けたりすることは禁止される。各教師が利用できる時間帯を高々2個に制限した場合、この時間割問題は多項式時間で解ける^[5]。

1976年の論文は、この場合を分岐を限定したバックトラック法で解いている。すでに決めた時間割によって選択が1通りに定まる教師を順に割り当て、そのような教師がいなくなったら、未割り当ての教師について一方の時間割を仮定する。そこから矛盾が生じれば、その仮定からの割り当てを取り消して他方を試す。両方で矛盾が生じれば実行不能と判定でき、それ以前に確定した選択まで戻る必要はない。同論文は、この分岐を限定する手法が2-SATにも適用できると述べている^[5]。一方、利用可能時間が3個の教師を含めると、全体の時間帯が3個でクラスが常に利用可能という制限の下でも、時間割問題はNP完全となる^[5]。

スポーツの日程

総当たり戦では、対戦相手と試合日が決まっていても、どちらのチームのホームで試合を行うかを選ぶ必要がある。連続する2試合がともにホーム、またはともにアウェーとなることをブレークという。${\displaystyle 2n}$ チームが ${\displaystyle 2n-1}$ 回の試合日に毎回1試合ずつ行い、ほかの全チームと1回ずつ対戦する場合、ブレークの総数を理論的下限の ${\displaystyle 2n-2}$ とする割り当ての存在と、各チームのブレークをちょうど1回とする割り当ての存在は、いずれも2-SATを用いて判定できる^[29]。

2005年に示された方法では、ホームとアウェーの選択をブール変数で表す補助問題を作る。対戦する両チームに異なる値を要求する条件などは、2リテラルの節で表せる。${\displaystyle O(n)}$ 個の補助問題を、それぞれ ${\displaystyle O(n^{2})}$ 個の変数と節からなる2-SATに変換するため、全体で ${\displaystyle O(n^{3})}$ 時間となる。この結果が扱うのは、指定したブレーク数や分布を実現できるかという問題である^[29]。

離散トモグラフィーとパズル

離散トモグラフィー（英語版）は、行や列などの方向ごとの投影から離散的な図形を復元する問題を扱う。例えば、0と1からなる行列の各行・各列について、1の個数が与えられたとき、それに一致する図形を求める問題がある。各行と各列で図形を構成するマスが連続し、さらに図形全体が辺を共有するマスで連結するポリオミノに限ると、復元問題を2-SATに還元する方法がある。図形の左右端の位置の候補を調べ、各候補に対して図形の外側の4領域をブール変数で表し、凸性や投影の条件を節にする^[30]。

お絵かきロジックでは、各行・各列の黒いマスの総数だけでなく、連続する黒いマスの長さと順序が指定される。これを解く手法の一つは、各行・各列の条件を動的計画法で調べる方法と、マスの総数に関する投影の条件から推論する方法を組み合わせ、得られたマス間の含意を2-CNF式にまとめるものである。含意グラフに ${\displaystyle x\longrightarrow \neg x}$ の有向路があれば、充足可能な式のどの解でも ${\displaystyle x=0}$ となり、逆向きの有向路があれば ${\displaystyle x=1}$ となる。この性質を使って値の確定したマスを増やし、推論を繰り返す^[31]。

この推論は多項式時間で行えるが、得られる2-SAT制約はパズルのすべての条件を表すとは限らない。そのため、各マスの値がすべて確定すればパズルは解けるものの、未確定のマスが残る場合もあり、一般のお絵かきロジックを多項式時間で必ず解く方法ではない^[31]。