2-満足可能性

コンピュータサイエンス において、2-充足可能性、2-SATまたは単に2SAT は、変数のペアに対する制約システムを満たすために、それぞれが 2 つの可能な値を持つ変数に値を割り当てる計算問題です。これは、3 つ以上の変数に対する制約を含むことができる一般的なブール充足可能性問題、および各変数の値に 3 つ以上の選択肢を許可できる制約充足問題 の特殊なケースです。しかし、 NP 完全であるこれらのより一般的な問題とは対照的に、2-充足可能性は多項式時間で解決できます。

2-充足可能性問題のインスタンスは、通常、連言正規形(2-CNF) またはKrom 式と呼ばれる特殊なタイプのブール式として表現されます。あるいは、特殊なタイプの有向グラフである含意グラフとして表現されることもあります。含意グラフは、インスタンスの変数とその否定をグラフの頂点として、変数のペアに対する制約を有向エッジとして表現します。これらの入力は両方とも、バックトラッキングに基づく方法、または含意グラフの強く連結されたコンポーネントを使用することによって、線形時間で解決できます。制約のペアを組み合わせて追加の有効な制約を作成する方法である解決 も、多項式時間で解決できます。2-充足可能性問題は、多項式時間で解決できる連言正規形式の 2 つの主要なサブクラスの 1 つを提供します。2 つのサブクラスのもう 1 つは、ホーン充足可能性です。

2 満足可能性は、オブジェクトの集合がそれぞれ 2 つの潜在的な位置を持ち、各オブジェクトが他のオブジェクトと重ならないように配置することを目指す幾何学および視覚化の問題に適用できます。その他の応用としては、クラスターの直径の合計を最小化するためのデータのクラスタリング、クラスルームやスポーツのスケジュール、断面に関する情報から形状を復元することなどがあります。

計算複雑性理論では、2-充足可能性はNL 完全問題の一例であり、対数量のストレージを使用して非決定的に解決でき、このリソース制限内で解決可能な問題の中で最も難しい問題の 1 つです。2-充足可能性インスタンスのすべてのソリューションの集合は、中央値グラフの構造で表すことができますが、これらのソリューションを数えることは#P 完全であるため、多項式時間ソリューションがあるとは予想されません。ランダム インスタンスは、制約と変数の比率が 1 を超えると、解決可能なインスタンスから解決不可能なインスタンスへと急激な相転移を起こします。これは、より複雑な形式の充足可能性問題では推測されているものの証明されていない現象です。 2-充足可能性の計算上難しいバリエーションである、満たされる制約の数を最大化する真理割り当てを見つけることには、その最適性がユニークゲーム予想に依存する近似アルゴリズムがあり、もう 1 つの難しいバリエーションである、真の変数の数を最小化する充足割り当てを見つけることは、パラメーター化された複雑性の重要なテスト ケースです。

2-充足可能性問題は、特別な制限形式を持つブール式を使用して記述できます。これは、節の論理積(ブール演算子and )であり、各節 は2 つの変数または否定変数の論理和(ブール演算子or ) です。この式に現れる変数またはその否定は、リテラルと呼ばれます。^[1]たとえば、次の式は、7 つの変数、11 の節、および 22 のリテラルを含む論理積標準形式です。 $${\displaystyle {\begin{aligned}&(x_{0}\lor x_{2})\land (x_{0}\lor \lnot x_{3})\land (x_{1}\lor \lnot x_{3})\land (x_{1}\lor \lnot x_{4})\land {}\\&(x_{2}\lor \lnot x_{4})\land {}(x_{0}\lor \lnot x_{5})\land (x_{1}\lor \lnot x_{5})\land (x_{2}\lor \lnot x_{5})\land {}\\&(x_{3}\lor x_{6})\land (x_{4}\lor x_{6})\land (x_{5}\lor x_{6}).\end{aligned}}}$$

2 満足可能性問題は、これらの変数に、式全体を真にする真理値割り当てを見つけることです。このような割り当てでは、各変数を真にするか偽にするかを選択し、各節の少なくとも 1 つのリテラルが真になるようにします。上記の式の場合、満足できる割り当ての 1 つは、7 つの変数すべてを真に設定する割り当てです。各節には少なくとも 1 つの非否定変数があるため、この割り当てはすべての節を満たします。式が真になるようにすべての変数を設定する方法は、他に 15 通りあります。したがって、この式で表される 2 満足可能性インスタンスは満足可能です。

この形式の式は 2-CNF 式として知られています。この名前の「2」は節ごとのリテラルの数を表し、「CNF」は論理積正規形(論理積の論理積の形をしたブール式の一種) を表します。^{[1]これらは、}カリフォルニア大学デービス校の数学者メルベン・R・クロムの研究にちなんでクロム式とも呼ばれます。クロムの 1967 年の論文は、2-充足問題に関する最も初期の研究の 1 つでした。^[2]

2-CNF 式の各節は、1 つの変数または否定変数から他の変数への含意と 論理的に同等です。たとえば、例の 2 番目の節は、次の 3 つの同等な方法のいずれかで記述できます。これらの異なる種類の操作間の同等性のため、2-充足可能性インスタンスは、連言標準形の各or節を、それが同等である 2 つの含意に 置き換えた含意標準形で記述することもできます。 ^[3]$${\displaystyle (x_{0}\lor \lnot x_{3})\;\equiv \;(\lnot x_{0}\Rightarrow \lnot x_{3})\;\equiv \;(x_{3}\Rightarrow x_{0}).}$$

2-充足可能性インスタンスを記述する3番目のよりグラフィカルな方法は、含意グラフとして記述することです。含意グラフは、変数または否定変数ごとに1つの頂点があり、対応する変数がインスタンスの含意標準形の含意によって関連付けられている場合は常に、1つの頂点を別の頂点に接続する辺がある有向グラフです。含意グラフは、各変数をその否定に取り、すべての辺の向きを反転する対称性を持つ、歪対称グラフである必要があります。 ^[4]

2-充足可能性問題を解くアルゴリズムはいくつか知られている。最も効率的なアルゴリズムは線形時間で解ける。^{[2] [4] [5]}

Krom(1967)は、2-充足可能性インスタンスを解決するための次の多項式時間決定手順を説明した。 ^[2]

2-充足可能性インスタンスに、同じ変数x を使用する 2 つの節が含まれているが、一方の節ではxが否定され、もう一方の節では否定されていないとします。この場合、2 つの節を組み合わせて、2 つの節に他の 2 つのリテラルを持つ 3 番目の節を作成できます。この 3 番目の節も、最初の 2 つの節が両方とも満たされる場合は必ず満たされます。これは 解決と呼ばれます。たとえば、節 とをこのように組み合わせて、節 を作成できます。2-CNF 式の含意形式では、この規則は 2 つの含意と を見つけ、推移性によって3 番目の含意を推論することになります。^[2]${\displaystyle (a\lor b)}$${\displaystyle (\lnot b\lor \lnot c)}$${\displaystyle (a\or \lnot c)}$${\displaystyle \lnot a\Rightarrow b}$${\displaystyle b\Rightarrow \lnot c}$${\displaystyle \lnot a\Rightarrow \lnot c}$

クロムは、この推論規則を繰り返し適用しても、任意の変数 に対して節と の両方を生成できない場合、式は一貫していると書いている。彼が証明しているように、2-CNF 式は、それが一貫している場合のみ満足可能である。というのは、式が一貫していない場合、2 つの節との両方を同時に満たすことはできないからである。そして、それが一貫している場合、式は、各ステップで一貫性を保ちながら、一度にまたはの形式の節を 1 つずつ繰り返し追加することで拡張でき、すべての変数に対してそのような節が含まれるようになるまで続く。これらの拡張ステップのそれぞれで、一貫性を保ちながら、これら 2 つの節のいずれかを常に追加できる。そうでない場合は、推論規則を使用してもう 1 つの節を生成できるからである。式内のすべての変数にこの形式の節が含まれるようになると、式に節 が含まれる場合は変数を true に設定し、式に節 が含まれる場合は変数を false に設定することで、すべての変数の満足できる割り当てを生成できる。^[2]${\displaystyle (x\lor x)}$${\displaystyle (\lnot x\lor \lnot x)}$${\displaystyle x}$${\displaystyle (x\lor x)}$${\displaystyle (\lnot x\lor \lnot x)}$${\displaystyle (x\lor x)}$${\displaystyle (\lnot x\lor \lnot x)}$${\displaystyle x}$${\displaystyle (x\lor x)}$${\displaystyle (\lnot x\lor \lnot x)}$

Krom は、アルゴリズムの効率ではなく、推論規則のシステムの完全性に主に関心がありました。しかし、彼の方法は、2 充足可能性問題を解くための多項式時間境界につながります。同じ変数を使用するすべての節をグループ化し、各節のペアに推論規則を適用することにより、与えられた 2-CNF インスタンスから可能なすべての推論を見つけて、それが一貫しているかどうかを合計時間O( n ³ )でテストすることができます。ここで、nはインスタンス内の変数の数です。この式は、変数の数に、推論規則を適用できる、与えられた変数を含む節のペアの数O( n ² )を掛けることから得られます。したがって、与えられた 2-CNF インスタンスが充足可能かどうかを時間O( n ³ )で判断することができます。Krom の方法を使用して満足できる割り当てを見つけるには、 O( n )の一貫性チェックのシーケンスが含まれるため、時間がかかりますO( n ⁴ )。 Even、Itai & Shamir (1976) は、より慎重な演算順序付けに基づいて、このアルゴリズムのより高速な時間制限O( n ² )を挙げています。しかし、このより短い時間制限でさえ、Even、Itai & Shamir (1976) および Aspvall、Plass & Tarjan (1979) による後の線形時間アルゴリズムによって大幅に改善されました。

2-充足可能性インスタンスの含意グラフの観点から、クロムの推論規則はグラフの推移閉包を構築するものとして解釈できる。クック (1971) が指摘しているように、これは解決原理を使用して充足可能性問題を解くデイビス-パトナムアルゴリズムのインスタンスと見ることもできる。その正しさは、デイビス-パトナムアルゴリズムのより一般的な正しさから導かれる。その多項式時間境界は、各解決ステップがインスタンス内の節の数を増加させ、その上限が変数の数の2次関数によって制限されるという事実から導かれる。^[6]

Even、Itai、Shamir (1976) は、バイナリ変数とペアワイズ制約を持つ制約充足問題を解くための限定的なバックトラッキングを含む手法について説明しています。彼らはこの手法を教室スケジュールの問題に適用しましたが、2-SATを含む他の問題にも適用できることを観察しました。^[5]

彼らのアプローチの基本的な考え方は、変数ごとに部分的な真理の割り当てを構築することです。アルゴリズムの特定のステップは「選択ポイント」であり、変数に 2 つの異なる真理値のいずれかを与えることができるポイントであり、アルゴリズムの後のステップでは、これらの選択ポイントの 1 つに戻ることがあります。ただし、戻ることができるのは最新の選択のみです。最新の選択より前に行われたすべての選択は永続的です。^[5]

最初は選択ポイントはなく、すべての変数は未割り当てです。各ステップで、アルゴリズムは次のように値を設定する変数を選択します。

• すでに両方の変数が設定されている節があり、その節が偽になるような場合、アルゴリズムは最新の選択ポイントまでバックトラックし、その選択以降に行った割り当てを取り消して、その選択で行った決定を反転します。選択ポイントがない場合、またはアルゴリズムが最新の選択ポイントまですでにバックトラックしている場合は、検索を中止し、入力された 2-CNF 式が満たされないと報告します。
• 節の 2 つの変数のうちの 1 つがすでに設定されていて、その節がまだ true または false になる可能性がある場合、もう 1 つの変数は、その節が true になるように設定されます。
• 残りのケースでは、各節は、残りの変数がどのように割り当てられても必ず真になるか、またはその 2 つの変数のどちらもまだ割り当てられていません。この場合、アルゴリズムは新しい選択ポイントを作成し、割り当てられていない変数のいずれかを任意に選択された値に設定します。

直感的に、アルゴリズムはそれぞれの選択を行った後にすべての推論の連鎖をたどります。これは矛盾とバックトラックのステップにつながるか、矛盾が導出されない場合は、選択が正しいものであり、満足のいく割り当てにつながるということになります。したがって、アルゴリズムは満足のいく割り当てを正しく見つけるか、入力が満たされないと正しく判断するかのいずれかです。^[5]

Even らは、このアルゴリズムを効率的に実装する方法については詳しく説明していません。彼らは、「あらゆる決定の影響を見つけるために適切なデータ構造を使用する」ことによって、アルゴリズムの各ステップ (バックトラック以外) を迅速に実行できるとだけ述べています。ただし、入力によっては、アルゴリズムが何度もバックトラックする可能性があり、そのたびにバックトラックの前に多くのステップが実行されるため、全体的な複雑さは非線形になる可能性があります。この問題を回避するために、彼らはアルゴリズムを変更し、各選択ポイントに到達した後、選択ポイントの変数セットの 2 つの割り当ての両方を同時にテストし、2 つの割り当てのそれぞれに同じ数のステップを費やします。これらの 2 つの割り当てのいずれかのテストによって別の選択ポイントが作成されるとすぐに、もう 1 つのテストが停止されるため、アルゴリズムのどの段階でも、バックトラック ツリーのテストがまだ行われているブランチは 2 つだけです。このように、任意の変数の 2 つのテストの実行に費やされる合計時間は、値が永続的に割り当てられている入力式の変数と節の数に比例します。その結果、アルゴリズムは合計で線形時間かかります。^[5]

Aspvall、Plass、Tarjan（1979）は、グラフ理論の強連結成分の概念に基づいて、2-充足可能性インスタンスを解決するためのより単純な線形時間手順を発見しました。^[4]

有向グラフの 2 つの頂点は、一方から他方へ、またその逆の有向パスがある場合、互いに強く接続されていると言われます。これは同値関係であり、グラフの頂点は、2 つの頂点ごとに強く接続されているサブセットである強連結成分に分割できます。グラフの強連結成分を見つけるための、深さ優先探索に基づく効率的な線形時間アルゴリズムがいくつかあります。Tarjanの強連結成分アルゴリズム^[7]とパスベースの強連結成分アルゴリズム^[8]は、それぞれ 1 回の深さ優先探索を実行します。Kosarajuのアルゴリズムは2 回の深さ優先探索を実行しますが、非常に単純です。

含意グラフの観点から言えば、2 つのリテラルは、一方のリテラルから他方のリテラルへの含意の連鎖が存在する場合、またはその逆の場合に、同じ強く連結されたコンポーネントに属します。したがって、与えられた 2 充足可能性インスタンスへの充足割り当てでは、2 つのリテラルは同じ値を持つ必要があります。特に、変数とその否定の両方が同じ強く連結されたコンポーネントに属している場合、これらのリテラルの両方に同じ値を割り当てることは不可能であるため、インスタンスは充足できません。Aspvall らが示したように、これは必要かつ十分な条件です。つまり、2-CNF 式が充足可能であるのは、その否定と同じ強く連結されたコンポーネントに属する変数が存在しないときのみです。^[4]

これは、2-CNF 式の充足可能性をテストするための線形時間アルゴリズムにすぐにつながります。つまり、単に含意グラフに対して強力な接続分析を実行し、各変数とその否定が異なるコンポーネントに属していることを確認するだけです。ただし、Aspvall らが示したように、充足割り当てが存在する場合は、それを見つけるための線形時間アルゴリズムにもつながります。彼らのアルゴリズムは、次の手順を実行します。

• インスタンスの含意グラフを構築し、強接続性分析用の既知の線形時間アルゴリズムのいずれかを使用して、その強接続性コンポーネントを見つけます。
• 強く連結されたコンポーネントに変数とその否定の両方が含まれているかどうかを確認します。含まれている場合は、インスタンスが満たされないことを報告し、停止します。
• 含意グラフの凝縮を構築します。これは、強く連結された各コンポーネントごとに 1 つの頂点と、コンポーネントiからコンポーネントjへのエッジを持つ小さなグラフです。これは、含意グラフに、 u がコンポーネントiに属し、v がコンポーネントjに属するようなエッジuv が含まれる場合に限ります。凝縮は自動的に有向非巡回グラフになり、それが形成された含意グラフと同様に、歪対称になります。
• 凝縮の頂点を位相的に順序付けます。実際には、コサラジュのアルゴリズムによって位相的に順序付けされ、タルジャンのアルゴリズムによって逆位相的に順序付けされたコンポーネントが生成されるため、これは前のステップの副作用として効率的に達成できます。 ^[9]
• 逆位相順序の各コンポーネントについて、その変数にまだ真理値が割り当てられていない場合は、コンポーネント内のすべてのリテラルを true に設定します。これにより、補完コンポーネント内のすべてのリテラルも false に設定されます。

逆位相順序と歪対称性により、リテラルが真に設定されると、そこから含意の連鎖を介して到達できるすべてのリテラルはすでに真に設定されていることになります。対称的に、リテラルxが偽に設定されると、含意の連鎖を介してそれにつながるすべてのリテラル自体もすでに偽に設定されていることになります。したがって、この手順によって構築された真理値割り当ては、与えられた式を満たし、Aspvall らによって特定された必要十分条件の正しさの証明も完了します。^[4]

Aspvallらが示すように、含意グラフの強く連結された成分を位相的に順序付ける同様の手順は、量化される式が2-CNF式である完全に量化されたブール式を評価するためにも使用できます。^[4]

自動ラベル配置問題に対する正確なアルゴリズムと近似アルゴリズムの多くは、2 満足可能性に基づいています。この問題は、図や地図の地物にテキスト ラベルを配置する問題です。通常、各ラベルの可能な位置のセットは、地図自体 (各ラベルはラベルを付ける地物の近くにあり、他の地物を隠してはなりません) だけでなく、ラベル同士によっても非常に制約されます。つまり、2 つのラベルは互いに重ならないようにする必要があります。重なり合うと判読できなくなります。一般に、これらの制約に従うラベル配置を見つけることはNP 困難な問題です。ただし、各地物のラベルの可能な位置が 2 つしかない場合 (たとえば、地物の左と右に広がる)、ラベル配置は多項式時間で解決できます。この場合、各ラベルに変数があり、重なり合う可能性のあるラベルのペアごとに節があり、ラベルが重なり合う位置に割り当てられないようにする 2 満足可能性インスタンスを作成できます。ラベルがすべて合同な長方形である場合、対応する 2 満足可能性インスタンスには線形数の制約のみがあることが示され、ラベル付けを見つけるためのほぼ線形時間のアルゴリズムにつながります。^[10] Poon、Zhu、Chin (1998) は、各ラベルがラベルを付ける線分に対して 3 つの位置のいずれかに配置される長方形であるマップのラベル付け問題を説明しています。線分を 1 つの辺として持つか、線分を中心に置くことができます。彼らは、これらの 3 つの位置を 2 つのバイナリ変数を使用して表し、有効なラベルの存在をテストすることが 2 満足可能性問題になるようにしています。^[11]

Formann & Wagner (1991) は、与えられた点の集合に対して、最大サイズの正方形ラベルを見つける問題に対する近似アルゴリズムの一部として 2満足可能性を使用しています。このとき、各ラベルの角の 1 つは、ラベルを付ける点と重なるという制約があります。与えられたサイズのラベルを見つけるために、2 倍にすると別の点と重なる正方形と、別の点のラベルと重なり合うことのない方法でラベルを付けることのできる点を除外しています。彼らは、これらの除外規則によって、残りの点には点ごとに 2 つのラベル配置しか存在しなくなり、2 満足可能性インスタンスのソリューションとして有効なラベル配置 (存在する場合) が見つかることを示しています。解決可能な 2 満足可能性インスタンスにつながる最大ラベル サイズを検索することで、ラベルが最適ソリューションの少なくとも半分の大きさである有効なラベル配置が見つかります。つまり、彼らのアルゴリズムの近似比は最大で 2 です。^{[10] [12]}同様に、各ラベルが長方形で、ラベルを付ける点がラベルの下端のどこかに位置するように配置する必要がある場合、2-充足可能性を使用して、各ラベルの点が下隅に位置する解が存在する最大のラベルサイズを見つけると、近似比は最大2になります。^[13]

2-充足可能性の同様の応用は、他の幾何学的配置問題にも行われています。グラフ描画では、頂点の位置が固定されており、各辺を 2 つの可能な位置のいずれかを持つ円弧として描画する必要がある場合 (たとえば、円弧図)、交差を避けるために各辺に使用する円弧を選択する問題は、各辺の変数と、交差につながる配置の各ペアの制約を伴う 2-充足可能性問題です。ただし、この場合、含意グラフの明示的な表現を構築してから検索するアルゴリズムと比較して、グラフを暗黙的に検索することで、解決を高速化できます。^[14] VLSI集積回路の設計 において、モジュールの集合をそれぞれ最大1回しか曲がらない配線で接続しなければならない場合、配線の経路は2つあり、どの経路を使用するか選択して、すべての配線を回路の単一層に配線できるような問題は、2-充足可能性インスタンスとして解決できる。^[15]

Boros ら (1999) は、別の VLSI 設計問題、つまり回路設計の各モジュールをミラー反転するかどうかという問題を考察しています。このミラー反転ではモジュールの動作は変わりませんが、モジュールの入力信号と出力信号がモジュールに接続するポイントの順序が変わり、モジュールが設計の残りの部分にどれだけうまく適合するかが変わる可能性があります。Borosらは、モジュールがすでに単一の線形チャネルに沿って配置されており、モジュール間の配線を配線する必要があり、チャネルの密度 (チャネルの任意の断面を通過する必要がある信号の最大数) には一定の上限があるという、問題の簡略版を考察しています。彼らは、この問題のバージョンは、制約がチャネルを挟んで互いに直接向かい合うモジュールのペアの方向を関連付ける 2 満足可能性インスタンスとして解決できることに注目しています。その結果、各ステップで 2 満足可能性インスタンスの解決が行われるバイナリ検索を実行することで、最適な密度も効率的に計算できます。^[16]

メトリック空間内のデータ ポイントのセットを 2 つのクラスターにクラスタリングする1 つの方法は、クラスターの直径の合計が最小になるようにクラスターを選択することです。ここで、単一のクラスターの直径は、そのクラスター内の任意の 2 つのポイント間の最大距離です。これは、非常に類似したポイントが異なるクラスターに割り当てられる可能性がある最大クラスター サイズを最小化するよりも望ましい方法です。2 つのクラスターのターゲット直径がわかっている場合は、2 充足可能性インスタンスを解くことで、それらのターゲットを実現するクラスタリングを見つけることができます。インスタンスにはポイントごとに 1 つの変数があり、そのポイントが最初のクラスターに属するか、2 番目のクラスターに属するかを示します。2 つのポイントが互いに離れすぎていて、両方が同じクラスターに属することができない場合は、この割り当てを防ぐ句がインスタンスに追加されます。

同じ方法は、個々のクラスターの直径が不明な場合にサブルーチンとして使用することもできます。個々のクラスターの直径を知らなくても、特定の直径の合計を達成できるかどうかをテストするには、最大で特定の合計になるターゲット直径のすべての最大ペアを試し、各直径のペアを 2 満足可能性インスタンスとして表し、2 満足可能性アルゴリズムを使用して、そのペアがクラスタリングによって実現できるかどうかを判断します。最適な直径の合計を見つけるには、各ステップがこのタイプの実行可能性テストであるバイナリ検索を実行します。同じアプローチは、クラスター直径の合計以外の組み合わせを最適化し、クラスターのサイズを測定するために任意の非類似度数 (メトリック空間での距離ではなく) を使用するクラスタリングを見つけるためにも機能します。^[17]このアルゴリズムの時間制限は、互いに密接に関連した2-充足可能性インスタンスのシーケンスを解く時間によって支配され、Ramnath（2004）は、これらの関連インスタンスを互いに独立して解く場合よりも速く解く方法を示し、直径和クラスタリング問題の合計時間制限をO（n ³）に導いた。 ^[18]

イタイとシャミール (1976) は、n 人の教師がm 人の生徒のコホートをそれぞれ教えるためにスケジュールを組まなければならないという教室スケジュールのモデルを検討しています。教師がコホートと過ごす1 週間あたりの時間数は、問題への入力として与えられた行列のエントリによって記述され、各教師にはスケジュールを組むことができる一連の時間もあります。彼らが示すように、各教師が最大で 3 時間しか利用できないときでも、この問題はNP 完全ですが、各教師が 2 時間しか利用できないときは 2 充足可能性の例として解決できます。 （1時間しか勤務できない教師は、簡単に問題から排除できる。）この問題では、各変数は教師がコホートと過ごす時間に対応し、変数への割り当てによって、その時間が教師の勤務可能時間の1時間目か2時間目かが指定され、2つのコホートが同時に1人の教師に割り当てられる、または1つのコホートが2人の教師に同時に割り当てられるという2つのタイプのいずれの衝突も防止する2充足条項がある。^[5]${\displaystyle i}$${\displaystyle j}$${\displaystyle R_{ij}}$${\displaystyle R}$${\displaystyle v_{ij}}$${\displaystyle i}$${\displaystyle j}$

Miyashiro & Matsui (2005) は、2 満足可能性を、総当たり戦の組み合わせがすでに選択されており、試合をチームのスタジアムに割り当てる必要があるスポーツ スケジュールの問題に適用しています。この問題では、チームが 2 試合連続でホーム ゲームまたは 2 試合連続でアウェー ゲームをプレイする「休憩」を避け、可能な限りホーム ゲームとアウェー ゲームを交互に行うことが望ましいです。最大で 2 チームだけが、ホーム ゲームとアウェー ゲームを交互にプレイすることで、完全に休憩を回避できます。他のどのチームも、これらの 2 チームと同じホーム アウェー スケジュールを持つことはできません。同じスケジュールを持つチームと対戦できなくなるためです。したがって、最適なスケジュールには、休憩のない 2 チームと、他のすべてのチームに 1 つの休憩があります。休憩なしのチームの 1 つを選択すると、各変数が 1 つの試合における 1 つのチームのホームとアウェイの割り当てを表し、制約によって、2 つのチームが試合に対して一貫した割り当てを持つこと、各チームが休憩なしのチームとの試合前に最大 1 回の休憩を持ち、試合後に最大 1 回の休憩を持つこと、どのチームも 2 回の休憩を持たないこと、といった特性が強制される 2 満足可能性問題を設定できます。したがって、最適な休憩回数のソリューションがスケジュールに含まれるかどうかをテストするには、休憩なしのチームの選択ごとに 1 つずつ、線形数の 2 満足可能性問題を解く必要があります。同様の手法を使用して、すべてのチームが 1 回の休憩を持つスケジュールを見つけ、休憩回数を最小化するのではなく最大化することもできます (チームの総移動距離を減らすため)。^[19]

トモグラフィーとは、断面から形状を復元するプロセスです。離散トモグラフィーは頻繁に研究されている問題の簡略版であり、復元される形状はポリオミノ（ 2次元の正方格子の正方形のサブセット）であり、断面は格子の個々の行と列の正方形のセットに関する集約的な情報を提供します。たとえば、ペイントバイナンバーズやグリドラーとしても知られる人気のノノグラムパズルでは、決定する正方形のセットはバイナリイメージの暗いピクセルを表し、パズルを解く人に与えられる入力は、イメージの各行または列に含める暗いピクセルの連続ブロックの数と、それらの各ブロックの長さを示します。他の形式のデジタルトモグラフィーでは、各行または列に関する情報はさらに少なく、正方形のブロックの数と長さではなく、正方形の合計数のみが与えられます。この問題の同等のバージョンは、行列の各行と各列の値の合計のみが与えられた場合に、 与えられた0-1 行列を復元する必要があるというものです。

与えられた行と列の合計を持つ行列を見つける多項式時間アルゴリズムは存在するが^[20] 、その解は一意には程遠い可能性がある。2 × 2単位行列の形の部分行列はどれも、解の正確さに影響を与えずに補完することができる。そのため、研究者は、解の空間を制限するために使用できる、再構築する形状に対する制約を探してきた。たとえば、形状が連結していると仮定するかもしれないが、連結した解が存在するかどうかをテストすることは NP 完全である。^[21]さらに制約が厳しく、解決しやすいバージョンは、形状が直交凸である、つまり各行と列に 1 つの連続した正方形のブロックがあるというものである。いくつかの以前の解を改良して、Chrobak & Dürr (1999) は 2-SAT を使用して、連結した直交凸形状を効率的に再構築する方法を示した。^[22]彼らの解決策の考え方は、再構築する図形の左端と右端のセルを含む行のインデックスを推測し、これらの推測と指定された行と列の合計に一致する図形が存在するかどうかをテストする 2 満足可能性問題を設定することです。彼らは、指定された図形の一部である可能性のある各正方形に対して 4 つの 2 満足可能性変数を使用します。1 つは図形の 4 つの可能な「コーナー領域」のそれぞれに属するかどうかを示します。また、これらの領域が分離していること、目的の形状であること、連続した行と列を持つ全体的な図形を形成すること、および目的の行と列の合計を持つことを強制する制約を使用します。彼らのアルゴリズムにはO( m ³ n )の時間がかかります。ここで、m は入力図形の 2 つの次元のうち小さい方、n は2 つの次元のうち大きい方です。同じ方法は後に、直交接続を必要とせず、対角線のみで接続される可能性のある直交凸形状に拡張されました。^[23]

Batenburg と Kosters (2008、2009) は、完全なノノグラム パズルのソルバーの一部として、2 満足度を使用して、他のいくつかのヒューリスティックから取得した情報を組み合わせました。パズルの部分的な解が与えられた場合、彼らは各行または列内で動的計画法を使用して、その行または列の制約によっていずれかのマスが白または黒に強制されるかどうか、および同じ行または列内の任意の 2 つのマスが含意関係によって接続できるかどうかを判断します。また、彼らは、各行と列のブロック長のシーケンスをその合計で置き換えることによってノノグラムをデジタル断層撮影問題に変換し、最大フロー定式化を使用して、すべての行と列を組み合わせたこのデジタル断層撮影問題に、状態を決定できるマス目または含意関係によって接続できるマス目のペアがあるかどうかを判断します。これら 2 つのヒューリスティックのいずれかがマス目の 1 つの値を決定する場合、それは部分的な解に含まれ、同じ計算が繰り返されます。しかし、両方のヒューリスティックで正方形を設定できなかった場合、両方で見つかった含意が 2 満足可能性問題に結合され、2 満足可能性ソルバーを使用して、問題によって値が固定されている正方形が検索され、その後、手順が再度繰り返されます。この手順は、解の発見に成功するかどうかはわかりませんが、多項式時間で実行されることが保証されています。Batenburg と Kosters は、ほとんどの新聞パズルではその完全なパワーを必要としないが、この手順と、この 2 満足可能性アプローチと Even、Itai、Shamir (1976) ^[5]の限定的なバックトラッキングを組み合わせた、より強力だが遅い手順の両​​方が、より困難なランダムに生成されたノノグラムに適用された場合、2 満足可能性のない動的計画法とフロー ヒューリスティックよりも大幅に効果的であると報告しています。^[24]

2-充足可能性の次に、多項式時間で解決できる充足可能性問題のもう 1 つの主要なサブクラスは、ホーン充足可能性です。このクラスの充足可能性問題では、入力はやはり連言正規形の式です。節ごとに任意の数のリテラルを含めることができますが、正のリテラルは最大で 1 つだけです。 Lewis (1978) は、このクラスの一般化である名前変更可能なホーン充足可能性を発見しました。これは、補助的な 2-充足可能性インスタンスによって多項式時間で解決できます。式が名前変更可能なホーンであるのは、いくつかの変数をその否定に置き換えることでホーン形式にできる場合です。これを行うために、Lewis は、名前変更可能なホーン インスタンスの各変数に対して 1 つの変数を持つ 2-充足可能性インスタンスを設定します。ここで、2-充足可能性変数は、対応する名前変更可能なホーン変数を否定するかどうかを示します。 Hornインスタンスを生成するには、名前変更可能なHornインスタンスの同じ節に現れる2つの変数がその節に正に現れてはならない。変数のペアに対するこの制約は2-充足可能性制約である。結果として得られる2-充足可能性インスタンスへの充足割り当てを見つけることで、ルイスは、名前変更可能なHornインスタンスを多項式時間でHornインスタンスに変換する方法を示している。^[25]長い節を複数の小さな節に分割し、線形時間の2-充足可能性アルゴリズムを適用することで、これを線形時間に短縮することができる。^[26]

2-充足可能性は、独立集合と少数の完全な二部グラフに分割できる無向グラフの認識問題^[27]、インターネットの自律サブシステム間のビジネス関係の推論^[28]、進化木の再構築^[29]などの問題にも応用されている。

対数量の書き込み可能メモリのみを使用して、 2-充足可能性インスタンスが充足可能でないかどうかを判断するための非決定性アルゴリズムは、簡単に記述できます。つまり、変数v を(非決定的に) 選択し、 vからその否定に至り、その後vに戻る含意の連鎖を (非決定的に) 検索するだけです。このような連鎖が見つかった場合、インスタンスは充足可能ではありません。Immerman –Szelepcsényi の定理により、非決定性ログスペースで、充足可能な 2-充足可能性インスタンスが充足可能であることを確認することもできます。

2-充足可能性は NL 完全であり[ 30 ^]、これは対数空間で非決定的に解ける問題の複雑性クラス NLにおける「最も難しい」または「最も表現力豊かな」問題の 1 つであることを意味します。ここでの完全性とは、対数空間のみを使用する決定性チューリング マシンが、 NL内の他のあらゆる問題を同等の 2-充足可能性問題に変換できることを意味します。よりよく知られている複雑性クラスNPの同様の結果と同様に、この変換と Immerman–Szelepcsényi 定理を組み合わせると、NL 内のあらゆる問題を、長さが 2 に制限された節を持つ単一の存在量化された述語を持つ2 階論理式として表すことができます。このような式は SO-Krom として知られています。^{[31]同様に、含意正規形は、}推移閉包の演算子を追加することで1 階論理 で表現できます。^[31]

2-充足可能性インスタンスに対するすべての解の集合は、中央値グラフの構造を持ち、そのグラフの辺は、すべてが互いに等しいか等しくないという制約のある変数の集合の値を反転する操作に対応する。特に、このように辺をたどることで、任意の解から他の任意の解に到達できる。逆に、任意の中央値グラフは、このようにして2-充足可能性インスタンスに対する解の集合として表すことができる。任意の3つの解の中央値は、各変数を3つの解の過半数で保持される値に設定することによって形成される。この中央値は常に、インスタンスに対する別の解を形成する。^[32]

フェダー（1994）は、与えられた2-充足可能性インスタンスに対するすべての解を効率的にリストし、いくつかの関連する問題を解決するためのアルゴリズムを説明しています。^[33]また、互いに最大のハミング距離 を持つ2つの満足な割り当てを見つけるアルゴリズムも存在します。 ^[34]

#2SAT は、与えられた 2-CNF 式に対する充足割り当ての数を数える問題です。この数え上げ問題は#P 完全であり、^[35] P = NPでない限り多項式時間で解くことはできません。さらに、 NP = RPでない限り、#2SAT の完全多項式ランダム近似スキームは存在せず、これは入力が単調な 2-CNF 式、つまり各リテラルが変数の正の出現である 2-CNF 式に制限されている場合でも当てはまります。^[36]

2SAT式を満たす割り当ての正確な数を計算する最も速い既知のアルゴリズムは、時間で実行されます。^{[37] [38] [39]}${\displaystyle O(1.2377^{n})}$

与えられた変数数nと節数mに対して、2 変数節の集合から各節を一様にランダムに選択することで、2 変数の充足可能性インスタンスをランダムに形成できる。mがnに対して小さい場合、そのようなインスタンスは充足可能である可能性が高いが、mの値が大きいほど充足可能性の確率は低くなる。より正確には、m / n が定数 α ≠ 1 として固定されている場合、充足可能性の確率はn が無限大に近づくにつれて限界に近づく。α < 1 の場合、限界は 1 であるが、α > 1 の場合、限界は 0 である。したがって、この問題はα = 1 で相転移を示す。^[40]

最大2充足問題（MAX-2-SAT）では、入力は2つのリテラルを含む連言正規形の式であり、割り当てによって同時に充足できる節の最大数を決定することが課題である。より一般的な最大充足問題と同様に、MAX-2-SATはNP困難である。証明は3SATからの還元によって行われる。^[41]

MAX-2-SAT を、含意グラフに関連するグラフにおいて、1 つの端点が最初の部分集合にあり、もう 1 つの端点が 2 番目の部分集合にあるエッジの数を最大化するカット (つまり、頂点を 2 つの部分集合に分割する) を見つける問題として定式化し、このカット問題に半正定値計画法を適用すると、少なくとも 0.940... 倍の最適節数を満たす近似解を多項式時間で見つけることができる。^[42]バランスのとれたMAX 2-SATインスタンスは、すべての変数が等しい重みで正と負に現れる MAX 2-SAT のインスタンスである。この問題に対して、Austrin は近似比を に改善した。^[43]${\displaystyle \min \left\{(3-\cos \theta )^{-1}(2+(2/\pi )\theta )\,:\,\pi /2\leq \theta \leq \pi \right\}=0.943...}$

もしユニークゲーム予想が正しいとすれば、バランスが取れているかどうかに関わらず、 0.943...より良い近似定数でMAX 2-SATを多項式時間で近似することは不可能である。 ^[44] P≠NPというより弱い仮定の下では、この問題は21/22 = 0.95454...より良い定数内でのみ近似不可能であることが知られている。^[45]

様々な著者がMAX-2-SATインスタンスの正確な解に対する指数関数的な最悪ケースの時間境界を調査した。^[46]

重み付き2-充足可能性問題（W2SAT）では、入力は-変数2SATインスタンスと整数kであり、問​​題はちょうどk個の変数が真となる充足割り当てが存在するかどうかを判断することです。^[47]${\displaystyle n}$

W2SAT 問題には、特殊なケースとして、与えられた無向グラフのすべての辺に接するk個の頂点の集合を見つける頂点カバー問題が含まれます。頂点カバー問題の任意のインスタンスに対して、グラフの各頂点に変数を持つ同等の W2SAT 問題を構築できます。グラフの各辺uv は、ソリューションの真の変数にuまたはv のいずれかを含めることによってのみ満たされる2SAT 節u ∨ vで表すことができます。その結果得られる 2SAT 式の満足するインスタンスは、頂点カバー問題のソリューションをエンコードし、 k個の頂点を持つ頂点カバーがある場合に限り、k 個の真の変数を持つ満足する割り当てが存在します 。したがって、頂点カバーと同様に、W2SAT はNP 完全です。

さらに、パラメータ化された複雑性において、 W2SATは自然なW[1]完全問題を提供する。^{[47]これは、} W[1]のすべての問題に当てはまらない限り、 W2SATは固定パラメータでは扱いにくいことを意味する。つまり、実行時間がf ( k )· nO ^(1)の形をとるW2SATアルゴリズムは存在しない可能性が高い。さらに強いことは、指数時間仮説が成り立たない限り、W2SATは時間no ^{( k )で}解くことはできないということである。^[48]

2-充足可能性に対する最初の多項式時間アルゴリズムを発見しただけでなく、Krom (1967) は、量化される式が 2-CNF 式である、完全に量化されたブール式を評価する問題も定式化しました。2-充足可能性問題は、すべての量化子が存在的である、この量化された 2-CNF 問題の特殊なケースです。Krom は、これらの式に対する効果的な決定手順も開発しました。Aspvall、Plass、Tarjan (1979) は、強く連結されたコンポーネントと位相的順序付けの手法を拡張することで、線形時間で解決できることを示しました。^{[2] [4]}

2-充足可能性問題は、命題多値論理に対しても問われることがある。アルゴリズムは通常線形ではなく、いくつかの論理では問題はNP完全である。概要についてはHähnle (2001, 2003)を参照のこと。^[49]