ブール充足可能性問題

論理学とコンピュータサイエンスにおいて、ブール充足可能性問題（命題充足可能性問題とも呼ばれ、 SATISFIABILITY、SAT 、またはB-SATと略される）は、与えられたブール式を満たす解釈が存在するかどうかを問う問題です。言い換えれば、式の変数を一貫して TRUE または FALSE の値に置き換えて式を TRUE と評価できるかどうかを問う問題です。これが当てはまる場合、式は充足可能と呼ばれ、そうでない場合は充足不可能と呼ばれます。たとえば、式「a AND NOT b 」は、( a AND NOT b ) = TRUEとなる値a = TRUE およびb = FALSE を見つけることができるため、充足可能です。対照的に、「a AND NOT a」は充足不可能です。

SATはNP完全であることが証明された最初の問題であり、これはクック・レビン定理と呼ばれています。これは、広範囲にわたる自然な決定問題や最適化問題を含む複雑性クラスNPのすべての問題が、最大でもSATと同程度の難しさしかないことを意味します。各SAT問題を効率的に解くアルゴリズムは知られていません（ここで「効率的に」とは「多項式時間で決定論的に」という意味です）。そのようなアルゴリズムは一般的に存在しないと考えられていますが、この考えは数学的に証明または反証されていません。SATに多項式時間アルゴリズムがあるかどうかという問題を解決すれば、計算理論における最も重要な未解決問題の一つであるP対NP問題が解決されるでしょう。^{[1] [2]}

それでも、2007年現在、ヒューリスティックSATアルゴリズムは、数万の変数と数百万の記号からなる数式を含む問題のインスタンスを解くことができ、^[3]人工知能、回路設計、^[4]自動定理証明で発生する多くの実用的なSAT問題には十分です。

定義

命題論理式はブール式とも呼ばれ、変数、演算子 AND (論理積、∧ とも表記)、OR (論理和、∨)、NOT (否定、¬)、括弧から構成されます。式は、適切な論理値(TRUE、FALSE) を変数に割り当てることで TRUE にできる場合、充足可能であると言われます。ブール充足可能性問題(SAT) は、式が充足可能かどうかを判定する問題です。この判定問題は、理論計算機科学、計算量理論、^{[5] [6]}アルゴリズム、暗号^{[7] [ 8 ]、}人工知能^[9]など、計算機科学の多くの分野で中心的な重要性を持っています。^{[追加の引用が必要]}

連言標準形

リテラルは、変数（この場合、正リテラルと呼ばれる）または変数の否定（負リテラルと呼ばれる）のいずれかです。節は、リテラルの論理和（または単一のリテラル）です。節に含まれる正リテラルが最大で1つである場合、その節はホーン節と呼ばれます。式が節の論理積（または単一の節）である場合、 その式は連言標準形（CNF）です。

例えば、x ₁は肯定リテラル、¬ x ₂は否定リテラル、x ₁ ∨ ¬ x ₂は節です。式( x ₁ ∨ ¬ x ₂ ) ∧ (¬ x ₁ ∨ x ₂ ∨ x ₃ ) ∧ ¬ x ₁は連言標準形です。つまり、第1節と第3節はホーン節ですが、第2節はホーン節ではありません。この式は、 x ₁  = FALSE、x ₂  = FALSE、x ₃を任意に選択することで満足可能です。なぜなら、(FALSE ∨ ¬FALSE) ∧ (¬FALSE ∨ FALSE ∨ x ₃ ) ∧ ¬FALSE は (FALSE ∨ TRUE) ∧ (TRUE ∨ FALSE ∨ x ₃ ) ∧ TRUE と評価され、さらに TRUE ∧ TRUE ∧ TRUE (つまり TRUE) と評価されるからです。一方、1つのリテラルからなる2つの節で構成されるCNF式a ∧ ¬ aは満足できません。なぜなら、a =TRUE またはa =FALSE の場合、それぞれ TRUE ∧ ¬TRUE (つまり FALSE) または FALSE ∧ ¬FALSE (つまり FALSE) と評価されるからです。

SAT 問題のいくつかのバージョンでは、一般化連言正規形式の概念を定義すると便利です。つまり、任意の数の一般化節の連言であり、後者は、何らかのブール関数Rと（通常の）リテラルl _iに対して形式R ( l ₁ ,..., l _n )となります。許可されるブール関数のセットが異なると、問題のバージョンも異なります。例として、R (¬ x , a , b ) は一般化節であり、R (¬ x , a , b ) ∧ R ( b , y , c ) ∧ R ( c , d ,¬ z ) は一般化連言正規形です。この式は以下で使用され、Rは、その引数の 1 つが TRUE である場合にのみ TRUE となる三項演算子です。

ブール代数の法則を用いると、あらゆる命題論理式は等価な連言正規形に変換できるが、その場合、指数関数的に長くなる可能性がある。例えば、式 ( x ₁ ∧ y ₁ ) ∨ ( x ₂ ∧ y ₂ ) ∨ ... ∨ ( x _n ∧ y _n ) を連言正規形に 変換すると、以下のようになる。

（x ₁  ∨  x ₂  ∨ … ∨  x _n）∧

（y ₁  ∨  x ₂  ∨ … ∨  x _n）∧

（x ₁  ∨  y ₂  ∨ … ∨  x _n）∧

( y ₁  ∨  y ₂  ∨ … ∨  x _n ) ∧ ... ∧

（x ₁  ∨  x ₂  ∨ … ∨  y _n）∧

( y ₁  ∨  x ₂  ∨ … ∨  y _n ) ∧

( x ₁  ∨  y ₂  ∨ … ∨  y _n ) ∧

( y ₁  ∨  y ₂  ∨ … ∨  y _n ) ;

前者は2 変数のn個の連言の論理和ですが、後者はn変数 の2 ^{n個の節で構成されます。}

しかし、 Tseytin変換を使用すると、元の命題論理式のサイズに線形な長さを持つ、等充足可能な連言標準形式が見つかる場合があります。

複雑

SAT はNP 完全であることが知られる最初の問題であり、 1971 年にトロント大学のStephen Cookによって証明され^[10] 、 1973 年にロシア科学アカデミーのLeonid Levinによって独立に証明されました^[11]。その時まで、NP 完全問題という概念は存在すらしていませんでした。その証明は、複雑性クラスNPのすべての決定問題が CNF ^[a]式の SAT 問題 ( CNFSATと呼ばれることもあります) に還元される方法を示しています。Cook の還元の便利な特性は、受理解の数を保存することです。たとえば、与えられたグラフに3 色があるかどうかを判断することは、NP の別の問題です。グラフに 17 個の有効な 3 色がある場合、Cook–Levin 還元によって生成される SAT 式には 17 個の満足する割り当てがあります。

NP完全性は、最悪のケースの実行時間のみを指します。実際のアプリケーションで発生する多くのケースは、はるかに高速に解決できます。以下の「SATを解くアルゴリズム」のセクションを参照してください。

3-満足度

3-SATインスタンス( x ∨ x ∨ y ) ∧ (¬ x ∨ ¬ y ∨ ¬ y ) ∧ (¬ x ∨ y ∨ y )はクリーク問題に帰着します。緑色の頂点は3クリークを形成し、 x =FALSE, y =TRUEという条件を満たします。

任意の論理式の充足可能性問題と同様に、各節が最大3つのリテラルに制限されている連言正規形の論理式の充足可能性を決定する問題もNP完全である。この問題は3-SAT、3CNFSAT、または3-充足可能性と呼ばれる。制限のないSAT問題を3-SATに縮約するには、各節l ₁ ∨ ⋯ ∨ l _{n を}n - 2個の節 の連言に変換する。

( l ₁ ∨ l ₂ ∨ x ₂ ) ∧

(¬ x ₂ ∨ l ₃ ∨ x ₃ ) ∧

(¬ x ₃ ∨ l ₄ ∨ x ₄ ) ∧ ⋯ ∧

(¬ x _{n −3} ∨ l _{n −2} ∨ x _{n −2} ) ∧

（¬ x _{n −2} ∨ l _{n −1} ∨ l _n）

ここで、x ₂ , ⋯ ,  x _{n −2}は他に現れない新しい変数である。2つの式は論理的には同値ではないが、等充足可能である。すべての節を変換した式は、元の式の最大3倍の長さになる。つまり、長さの増加は多項式である。^[12]

3-SATはカープの21のNP完全問題の一つであり、他の問題もNP困難であることを証明するための出発点として用いられます。^{[b]これは、3-SATから他の問題への}多項式時間還元によって行われます。この手法が用いられた問題の例としては、クリーク問題が挙げられます。c個の節からなるCNF式が与えられた場合、対応するグラフは各リテラルの頂点と、異なる節からの矛盾しない2つのリテラル^[c]間の辺で構成されます（図を参照）。グラフにcクリークが存在するのは、式が充足可能である場合のみです。^[13]

Schöning (1999)による単純なランダム化アルゴリズムがあり、これは(4/3) ⁿ時間で実行され、高い確率で3-SATを正しく決定することに成功します。ここでnは3-SAT命題における変数の数です。^[14]

指数時間仮説は、3-SAT（または任意のk > 2のk -SAT ）をexp( o ( n ))時間（つまり、nの指数関数よりも基本的に速い）で解くことができるアルゴリズムはないと主張しています。

セルマン、ミッチェル、レベスク（1996）は、ランダムに生成された3-SAT式の難易度について、そのサイズパラメータに応じた実証データを示しています。難易度は、DPLLアルゴリズムによる再帰呼び出し回数で測定されます。彼らは、節対変数比が約4.26のときに、ほぼ確実に満足可能な式からほぼ確実に満足不可能な式へと遷移する相転移領域を特定しました。^[15]

CNF の式が各節に最大k個のリテラルを含むとみなされる場合、 3-充足可能性はk-充足可能性( k-SAT、k-CNF-SATとも) に一般化できます。 ^{[引用が必要]ただし、} k ≥ 3の場合、この問題は 3-SAT より簡単になることも、SAT より難しくなることもなく、後者 2 つは NP 完全であるため、k-SAT である必要があります。

著者によっては、k-SAT をちょうど k 個のリテラルを持つ CNF 式に制限している。^[要出典]これによっても、j < k個のリテラルを持つ各節l ₁ ∨ ⋯ ∨ l _jに、固定ダミー変数を追加してl ₁ ∨ ⋯ ∨ l _j ∨ d _{j +1} ∨ ⋯ ∨ d _kとすることができるため、複雑さのクラスが変わることはない。すべての節を埋め込んだ後、d ₁ = ⋯ = d _k = FALSEのみが満足できる割り当てにつながることを保証するために、2 ^k –1 個の追加の節^{[d]を追加する必要がある。k は式の長さに依存しないため、追加の節によって長さが一定に増加する。同じ理由で、} ¬ x ∨ ¬ y ∨ ¬ yのように、節で重複するリテラルが許可されるかどうかは問題ではない。

3SATの特別な例

連言標準形

連言正規形（特に節ごとに3つのリテラルを持つもの）は、SAT式の標準的な表現とよく考えられています。前述のように、一般的なSAT問題は、この形式の式の充足可能性を判定する問題である3-SATに帰着します。

リニアSAT

3-SAT 式は、各節（リテラルの集合として）が最大で1つの他の節と交差し、さらに、2つの節が交差する場合、それらの節に共通するリテラルがちょうど1つだけ存在する場合、線形 SAT (LSAT) である。LSAT 式は、直線上の互いに素な半閉区間の集合として表すことができる。LSAT 式が充足可能かどうかを判定することは NP 完全である。^[16]

2-充足可能性

SATは、節内のリテラルの数が最大2に制限されている場合、より容易になります。この場合、問題は2-SATと呼ばれます。この問題は多項式時間で解くことができ、計算量クラスNLに対して完全です。さらに、リテラル内のすべてのOR演算をXOR演算に変更すると、結果は排他的論理和2-充足可能性と呼ばれ、計算量クラスSL = Lに対して完全です。

ホーン充足可能性

ホーン節の連言の充足可能性を判定する問題は、ホーン充足可能性問題（Horn-satisfiability）またはHORN-SAT問題と呼ばれます。これは、ホーン節の集合（TRUEに割り当てられたリテラルの集合に関して）の単一の極小モデルを生成する単位伝播アルゴリズムの1ステップによって多項式時間で解くことができます。ホーン充足可能性問題はP完全です。これは、ブール充足可能性問題のP版と見ることができます。また、量化ホーン論理式の真偽判定も多項式時間で行うことができます。^[17]

ホーン節は、ある変数が他の変数の集合からどのような含意を持つかを表現できるため、興味深いものです。実際、そのような節の一つである ¬ x ₁ ∨ ... ∨ ¬ x _n ∨ yは、 x ₁ ∧ ... ∧ x _n → yと書き換えることができます。つまり、x ₁ ,..., x _nがすべて TRUE であれば、y も必ず TRUE であるということです。

ホーン論理式の一般化として、名前変更可能なホーン論理式があります。これは、いくつかの変数をそれぞれの否定に置き換えることでホーン形式にすることができる論理式の集合です。例えば、 ( x ₁ ∨ ¬ x ₂ ) ∧ (¬ x ₁ ∨ x ₂ ∨ x ₃ ) ∧ ¬ x ₁はホーン論理式ではありませんが、 x 3 の否定として y 3 を導入することで、ホーン論理式 ( x ₁ ∨ ¬ _x 2 ₎ ∧ ( _¬ x 1 _∨ x 2 _∨ ¬ y ₃ ) ∧ ¬ x ₁に名前変更することができます。対照的に、( x ₁ ∨ ¬ x ₂ ∨ ¬ x ₃ ) ∧ (¬ x ₁ ∨ x ₂ ∨ x ₃ ) ∧ ¬ x ₁は名前を変更しないとホーン論理式となる。このような置換の存在確認は線形時間で実行できるため、このような論理式の充足可能性はPに含まれる。なぜなら、まずこの置換を行い、次に結果として得られるホーン論理式の充足可能性を確認することで解けるからである。

3SATの問題ではない

選言正規形

SATは、式が選言正規形に限定されている場合、つまり、リテラルの連言の選言である場合に限り、自明です。このような式が実際に満足可能であるのは、少なくとも1つの連言が満足可能である場合であり、連言が満足可能であるのは、ある変数xに対してxと NOT x の両方を含まない場合です。これは線形時間で検証できます。さらに、式が完全な選言正規形に限定されている場合、つまり、すべての変数がすべての連言に1回だけ出現する場合、定数時間で検証できます（各連言は1つの満足する割り当てを表します）。しかし、一般的なSAT問題を選言正規形に変換するには、指数関数的な時間と空間が必要になる場合があります。例として、上記の指数関数的な爆発の例の「∧」と「∨」を連言正規形に置き換えてください。

正確に1 3の充足可能性

3-充足可能性問題のNP完全変種として、1/3 3-SAT （ 1-in-3-SAT、exactly-1 3-SATとも呼ばれる）があります。この問題は、節ごとに3つのリテラルを持つ連言正規形が与えられたとき、各節にちょうど1つのTRUEリテラル（つまりちょうど2つのFALSEリテラル）が含まれるような変数への真理値割り当てが存在するかどうかを判定することです。

すべてが等しいわけではない3つの満足度

もう一つの変種は、全てが等しいわけではない3-充足可能性問題（NAE3SATとも呼ばれる）である。節ごとに3つのリテラルを持つ連言正規形が与えられたとき、どの節においても3つのリテラルすべてが同じ真理値を持つような変数への代入が存在するかどうかを判定する問題である。この問題は、シェーファーの二分定理により、否定記号が認められない場合でもNP完全である。^[18]

XOR充足可能性

もう一つの特殊なケースは、各節に（単純な）OR演算子ではなくXOR（すなわち排他的論理和）演算子が含まれる問題群である。これはPに属する。なぜなら、XOR-SAT式は2を法とする線型方程式の連立と見なすこともできるため、ガウス消去法によって3乗時間で解くことができるからである。^[19]

シェーファーの二分定理

上記の制約 (CNF、2CNF、3CNF、Horn、XOR-SAT) により、検討対象の式は部分式の連言となるように制限されています。各制約は、すべての部分式に対して特定の形式を指定します。たとえば、2CNF では、2 項節のみが部分式になることができます。

シェーファーの二分定理は、これらの部分式を形成するために使用できるブール関数への任意の制約に対して、対応する充足可能性問題はPまたはNP完全に属することを述べている。2CNF、ホーン、およびXOR-SAT式がPに属することは、この定理の特別な場合である。^[18]

次の表は、SAT の一般的なバリエーションのいくつかをまとめたものです。

SATの拡張

2003年以降、大きな人気を博している拡張は、線形制約、配列、すべて異なる制約、解釈されない関数などを用いてCNF式を強化できる、満足可能性法理論（SMT）である。 [ 20 ^]このような拡張は通常NP完全のままであるが、現在では多くの種類の制約を処理できる非常に効率的なソルバーが利用可能である。

ブール変数を束縛するために「すべてに対して」（∀）と「存在する」（∃）の両方の量指定子が許される場合、充足可能性問題はより困難になります。そのような式の例としては、 ∀ x ∀ y ∃ z ( x ∨ y ∨ z ) ∧ (¬ x ∨ ¬ y ∨ ¬ z )が挙げられます。これは、 xとyのすべての値に対して、適切なzの値、すなわちxとy の両方が FALSE の場合はz =TRUE 、それ以外の場合はz =FALSE が成り立つため、有効です。SA​​T 自体は（暗黙的に） ∃ 量指定子のみを使用します。代わりに ڼ 量指定子のみを許すと、いわゆるトートロジー問題が生じますが、これは共NP完全です。両方の量指定子が任意の数だけ許容される場合、この問題は量指定ブール式問題（QBF ）と呼ばれ、 PSPACE完全であることが示されます。PSPACE完全問題はNPのどの問題よりも厳密に困難であると広く信じられていますが、これはまだ証明されていません。

通常のSATでは、式が成り立つような変数代入が少なくとも1つあるかどうかを問われます。様々なバリエーションがあり、そのような代入の数を問うことができます。

• MAJ-SATは、すべての割り当ての少なくとも半分が式を真とするかどうかを問う。これは確率クラスPPに対して完全であることが知られている。驚くべきことに、 MAJ-kSATは任意の有限整数kに対してPに属することが証明されている。^[21]
• #SAT、つまり式を満たす変数割り当ての数を数える問題は、決定問題ではなく計数問題であり、 #P 完全です。
• UNIQUE SAT ^[22]は、式にちょうど1つの割り当てがあるかどうかを判定する問題です。これは、非決定性多項式時間チューリングマシンによって解ける問題を記述する計算量クラスであるUS ^[23]に対して完全です。USは、非決定性受理経路がちょうど1つ存在する場合に受理し、そうでない場合は棄却します。
• UNAMBIGUOUS-SATは、入力式が最大でも1つの満足な割り当てを持つことが約束されている場合の充足可能性問題に付けられた名前です。この問題はUSATとも呼ばれます。^[24] UNAMBIGUOUS-SATを解くアルゴリズムは、複数の満足な割り当てを持つ式に対して、無限ループを含む任意の動作を示すことが許されます。この問題は一見簡単に思えますが、ValiantとVaziraniは[ ^{25] 、これを解くための実用的な（すなわち}ランダム化多項式時間）アルゴリズムがあれば、 NPのすべての問題も同様に簡単に解けることを示しています。
• MAX-SAT（最大充足可能性問題）は、SATのFNP一般化です。任意の割り当てによって満たされる節の最大数を求めます。効率的な近似アルゴリズムは存在しますが、厳密に解くのはNP困難です。さらに悪いことに、これはAPX完全であり、P=NPでない限り、この問題に対する多項式時間近似スキーム（PTAS）は存在しません。
• WMSATは、単調なブール式（すなわち、否定のない式）を満たす最小の重みの割り当てを求める問題である。命題変数の重みは問題の入力として与えられる。割り当ての重みは、真の変数の重みの合計である。この問題はNP完全である（ ^[26]のTh.1を参照）。

その他の一般化には、第1 階および第 2 階論理の満足度、制約充足問題、0-1 整数計画法の充足可能性が含まれます。

満足のいく仕事を見つける

SATは決定問題ですが、満足な割り当てを見つける探索問題はSATに帰着します。つまり、SATのインスタンスが解けるかどうかを正しく答える各アルゴリズムは、満足な割り当てを見つけるために使用できます。まず、与えられた式Φについて質問します。答えが「いいえ」の場合、式は満足できません。それ以外の場合は、部分的にインスタンス化された式Φ { x ₁ =TRUE}、つまり最初の変数x ₁をTRUEに置き換え、それに応じて簡略化した式Φについて質問します。答えが「はい」の場合、x ₁ =TRUE、それ以外の場合はx ₁ =FALSEです。他の変数の値も同様の方法で見つけることができます。合計でn +1回のアルゴリズム実行が必要です。ここで、nはΦ内の異なる変数の数です。

この特性は複雑性理論のいくつかの定理で使用されています。

• NP ⊆ P/poly ⇒ PH = Σ ₂（カープ・リプトンの定理）
• NP ⊆ BPP ⇒ NP = RP
• P = NP ⇒ FP = FNP

SATを解くアルゴリズム

SAT 解答の指数関数的複雑さと変数数、節数、式の長さ

SAT問題はNP完全であるため、この問題に対しては、最悪ケースの複雑度が指数関数的になるアルゴリズムしか知られていない。それにもかかわらず、SATの効率的でスケーラブルなアルゴリズムは2000年代に開発され、数万の変数と数百万の制約（つまり節）を含む問題インスタンスを自動的に解く能力の劇的な進歩に貢献した。^[3]電子設計自動化（EDA）におけるそのような問題の例としては、形式的同値性検査、モデル検査、パイプライン化されたマイクロプロセッサの形式的検証、^[20]自動テストパターン生成、FPGAの配線、^[27]プランニング、スケジューリング問題などがあげられる。SAT解決エンジンは、電子設計自動化ツールボックスに不可欠なコンポーネントでもあると考えられている。

現代のSATソルバーで用いられる主要な手法には、デイビス・パトナム・ローゲマン・ラブランドアルゴリズム（DPLL）、衝突駆動節学習（CDCL）、そしてWalkSATのような確率的 局所探索アルゴリズムなどがある。ほぼすべてのSATソルバーはタイムアウト機能を備えているため、解が見つからない場合でも妥当な時間で終了する。SATソルバーによって、容易に判断できる問題や困難に判断できる問題は異なり、充足不可能性の証明に優れているものもあれば、解の発見に優れているものもある。最近では、深層学習技術を用いて問題の充足可能性を学習する試みがなされている。^[28]

SATソルバーはSAT解答コンテストで開発され、比較されています。^{[29]現代のSATソルバーは、ソフトウェア検証、人工知能における制約解決、}オペレーションズ・リサーチなどの分野にも大きな影響を与えています。

過去数十年間で、最悪ケースの実行時間保証が改善された理論的なアルゴリズムが提示されてきました。これには、長さ（総リテラル数）の節集合に対するアルゴリズム、^{[30] [31]} 、節集合に対するアルゴリズム 、[ ^{32] [33]}、変数付き3-SATアルゴリズム^[34]が含まれます。ここで、「 」という表記は「多項式因数まで」、つまり を意味します。以前の実行時間保証は図に示されています。 ${\displaystyle O^{*}(1.0638^{L})}$ ${\displaystyle L}$ ${\displaystyle O^{*}(1.2226^{m})}$ ${\displaystyle m}$ ${\displaystyle O^{*}(1.32793^{n})}$ ${\displaystyle n}$ ${\displaystyle O^{*}(.)}$ ${\displaystyle O^{*}(f(n))=O(f(n)n^{O(1)})}$

参照

• 満たされないコア
• 理論による充足可能性
• SATを数える
• 平面SAT
• カーロフ・ツウィックアルゴリズム
• 回路の充足可能性

注記

1. 任意の式の SAT 問題も NP 完全です。NP であることが簡単に示されるため、CNF 式の SAT よりも簡単になることはあり得ません。
2. つまり、NPに属する他のすべての問題と少なくとも同程度に難しい。意思決定問題がNP完全であるためには、NPに属し、かつNP困難でなければならない。
3. つまり、一方のリテラルがもう一方のリテラルの否定ではない
4. すなわち、 d ₁ ,⋯, d _kで構築できるすべての最大項（ただし、 d ₁ ∨⋯∨ d _kを除く）

外部リンク

• SATゲーム：ブール充足可能性問題を自分で解いてみよう
• 国際SATコンテストウェブサイト
• 満足度テストの理論と応用に関する国際会議
• 充足可能性、ブールモデリング、計算に関するジャーナル
• SAT Live、満足度問題に関する研究の総合ウェブサイト
• MaxSATソルバーの年次評価

参考文献

1. Fortnow, L. (2009). 「P対NP問題の現状」(PDF) . Communications of the ACM . 52 (9): 78– 86. doi :10.1145/1562164.1562186. S2CID  5969255.
2. Fortnow, L. (2021). 「P対NPの50年と不可能の可能性」(PDF) . ACMカンファレンス議事録 (カンファレンス'17) .
3. Ohrimenko, Olga; Stuckey, Peter J.; Codish, Michael (2007)、「Propagation = Lazy Clause Generation」、Principles and Practice of Constraint Programming – CP 2007、Lecture Notes in Computer Science、vol. 4741、pp.  544– 558、CiteSeerX 10.1.1.70.5471、doi :10.1007/978-3-540-74970-7_39、ISBN  978-3-540-74969-1現代のSATソルバーは、数百万の制約と数十万の変数を持つ問題を扱うことができる。。
4. ホン・テッド、リー・ヤンジン、パーク・ソンボエム、ムイ・ダイアナ、リン・デイビッド、カレク・ジヤド・アブデル、ハキム・ナギブ、ナエイミ・ヘリア、ガードナー・ドナルド・S、ミトラ・スバシッシュ（2010年11月）。「QED：効果的なポストシリコン検証のためのクイックエラー検出テスト」2010 IEEE国際テスト会議、pp.  1– 10. doi :10.1109/TEST.2010.5699215. ISBN 978-1-4244-7206-2. S2CID  7909084。
5. カープ、リチャード・M. (1972). 「組合せ問題における還元可能性」(PDF) . レイモンド・E・ミラー、ジェームズ・W・サッチャー編. 『コンピュータ計算の複雑性』 ニューヨーク: プレナム. pp.  85– 103. ISBN 0-306-30707-3. 2011年6月29日時点のオリジナル（PDF）からアーカイブ。2020年5月7日閲覧。こちら：p.86
6. Aho, Alfred V.; Hopcroft, John E.; Ullman, Jeffrey D. (1974). 『コンピュータアルゴリズムの設計と分析』 Addison-Wesley. p. 403. ISBN 0-201-00029-6。
7. Massacci, Fabio; Marraro, Laura (2000-02-01). 「SAT問題としての論理暗号解析」. Journal of Automated Reasoning . 24 (1): 165– 203. doi :10.1023/A:1006326723002. S2CID  3114247.
8. ミロノフ, イリヤ; 張, リンタオ (2006). 「SATソルバーのハッシュ関数暗号解読への応用」. ビエール, アーミン; ゴメス, カーラ P. (編).充足可能性テストの理論と応用 - SAT 2006.コンピュータサイエンス講義ノート. 第4121巻. シュプリンガー. pp.  102– 115. doi :10.1007/11814948_13. ISBN 978-3-540-37207-3。
9. Vizel, Y.; Weissenbacher, G.; Malik, S. (2015). 「ブール充足可能性ソルバーとモデル検査への応用」. Proceedings of the IEEE . 103 (11): 2021– 2035. doi :10.1109/JPROC.2015.2455034. S2CID  10190144.
10. Cook, Stephen A. (1971). 「定理証明手順の複雑さ」(PDF) . Proceedings of the third annual ACM symposium on Theory of computing - STOC '71 . pp.  151– 158. CiteSeerX 10.1.1.406.395 . doi :10.1145/800157.805047. S2CID 7573663. 2022年10月9日時点のオリジナルより アーカイブ(PDF) 。 
11. レビン、レオニード(1973)。 「ユニバーサル検索問題 (ロシア語: Универсальные задачи перебора, Universal'nye perebornye zadachi)」。情報伝達の問題 (ロシア語: Проблемы передачи информа́ции、問題のあるペレダチ情報ii)。9 (3): 115–116 .(pdf) (ロシア語)、英語に翻訳：トラクテンブロート, BA (1984). 「ロシアにおけるペレボル（総当たり探索）アルゴリズムへのアプローチの概観」 Annals of the History of Computing . 6 (4): 384– 400. doi :10.1109/MAHC.1984.10036. S2CID  950581.
12. Aho、Hopcroft、Ullman（1974）、定理10.4。
13. Aho、Hopcroft、Ullman（1974）、定理10.5。
14. Schöning, Uwe (1999年10月). 「k-SATと制約充足問題のための確率的アルゴリズム」(PDF) .第40回コンピュータサイエンス基礎シンポジウム (カタログ番号99CB37039) . pp.  410– 414. doi :10.1109/SFFCS.1999.814612. ISBN 0-7695-0409-4. S2CID  123177576。2022年10月9日にオリジナルからアーカイブ（PDF）されました。
15. セルマン, バート; ミッチェル, デイビッド; レベスク, ヘクター (1996). 「困難な充足可能性問題の生成」.人工知能. 81 ( 1–2 ): 17–29 . CiteSeerX 10.1.1.37.7362 . doi :10.1016/0004-3702(95)00045-3. 
16. Arkin, Esther M.; Banik, Aritra; Carmi, Paz; Citovsky, Gui; Katz, Matthew J.; Mitchell, Joseph SB; Simakov, Marina (2018-12-11). 「色付き点の選択と被覆」. Discrete Applied Mathematics . 250 : 75– 86. doi : 10.1016/j.dam.2018.05.011 . ISSN  0166-218X.
17. Buning, HK; Karpinski, Marek; Flogel, A. (1995). 「定量化されたブール式の解像度」.情報と計算. 117 (1). エルゼビア: 12–18 . doi : 10.1006/inco.1995.1025 .
18. Schaefer, Thomas J. (1978). 「充足可能性問題の複雑性」(PDF) .第10回ACMコンピューティング理論シンポジウム議事録. サンディエゴ、カリフォルニア州. pp.  216– 226. CiteSeerX 10.1.1.393.8951 . doi :10.1145/800133.804350. 
19. ムーア、クリストファー、メルテンス、ステファン（2011年）、計算の性質、オックスフォード大学出版局、p.366、ISBN 9780199233212。
20. RE Bryant、SM German、MN Velev、「解釈されていない関数の等価性ロジックに対する効率的な決定手順を使用したマイクロプロセッサ検証」、Analytic Tableaux and Related Methods、pp. 1–13、1999年。
21. Akmal, Shyan; Williams, Ryan (2022). MAJORITY-3SAT（および関連問題）の多項式時間解法. pp.  1033– 1043. arXiv : 2107.02748 . doi :10.1109/FOCS52979.2021.00103. ISBN 978-1-6654-2055-6。
22. Blass, Andreas; Gurevich, Yuri (1982-10-01). 「一意な充足可能性問題について」. Information and Control . 55 (1): 80– 88. doi : 10.1016/S0019-9958(82)90439-9 . hdl : 2027.42/23842 . ISSN  0019-9958.
23. “Complexity Zoo:U - Complexity Zoo”. complexityzoo.uwaterloo.ca . 2019年7月9日時点のオリジナルよりアーカイブ。2019年12月5日閲覧。
24. Kozen, Dexter C. (2006). 「補足講義F：一意な充足可能性」.計算理論. コンピュータサイエンステキスト. Springer. p. 180. ISBN 9781846282973。
25. Valiant, L.; Vazirani, V. (1986). 「NPは一意解の検出と同じくらい簡単だ」(PDF) .理論計算機科学. 47 : 85–93 . doi : 10.1016/0304-3975(86)90135-0 .
26. Buldas, Ahto; Lenin, Aleksandr; Willemson, Jan; Charnamord, Anton (2017). 「攻撃木のためのシンプルな実行不可能証明書」. 尾花聡; 千田浩二 (編).情報とコンピュータセキュリティの進歩. コンピュータサイエンス講義ノート. 第10418巻. Springer International Publishing. pp.  39– 55. doi :10.1007/978-3-319-64200-0_3. ISBN 9783319642000。
27. Gi-Joon Nam; Sakallah, KA; Rutenbar, RA (2002). 「探索ベースのブール充足可能性によるFPGA詳細配線手法の新規化」(PDF) . IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems . 21 (6): 674. Bibcode :2002ITCAD..21..674N. doi :10.1109/TCAD.2002.1004311. オリジナル(PDF)から2016年3月15日にアーカイブ。 2015年9月4日閲覧。
28. Selsam, Daniel; Lamm, Matthew; Bünz, Benedikt; Liang, Percy; de Moura, Leonardo; Dill, David L. (2019年3月11日). 「シングルビット監視によるSATソルバーの学習」. arXiv : 1802.03685 [cs.AI].
29. 「国際SATコンペティションのウェブページ」 。 2007年11月15日閲覧。
30. Junqiang PengとMingyu Xiao (2022年8月). 数式の長さに関するSATのさらなる改善（技術レポート）. arXiv : 2105.06131 .
31. Junqiang PengとMingyu Xiao (2023年10月). 「数式の長さに関するSATのさらなる改善」. Information and Computation . 294 105085: 論文番号105085. doi :10.1016/j.ic.2023.105085.
32. Huairui Chu、Mingyu Xiao、Zhe Zhang (2020年7月). SATの改良された上限値（技術レポート）. arxiv. arXiv : 2007.03829 .
33. Huairui Chu、Mingyu Xiao、Zhe Zhang (2021年10月). 「SATの改良された上限値」.理論計算機科学. 887 : 51–62 . doi :10.1016/j.tcs.2021.06.045.
34. S. Liu (2018年7月). I. Chatzigiannakis、C. Kaklamanis、D. Marx、D. Sannella (編). Chain、被覆コードの一般化、およびk -SATの決定論的アルゴリズム. Proc. ICALP. LIPIcs. Vol. 107. Schloss Dagstuhl. pp. 88:1–13. doi : 10.4230/LIPIcs.ICALP.2018.88 .

出典

• この記事には、Karem A. Sakallah教授による https://web.archive.org/web/20070708233347/http://www.sigda.org/newsletter/2006/eNews_061201.html の資料が含まれています。

さらに読む

（発行日順）

• ゲイリー, マイケル・R. ;ジョンソン, デイビッド・S. (1979). 『コンピュータとイントラクタビリティ：NP完全性理論へのガイド』WHフリーマン. A9.1: LO1–LO7, 259–260. ISBN 0-7167-1045-5。
• Marques-Silva, J.; Glass, T. (1999). 「充足可能性と再帰学習を用いた組み合わせ同値性検証」. Design, Automation and Test in Europe Conference and Exhibition, 1999. Proceedings (Cat. No. PR00078) (PDF) . p. 145. doi :10.1109/DATE.1999.761110. ISBN 0-7695-0078-12022年10月9日時点のオリジナルよりアーカイブ（PDF）されています。
• Clarke, E.; Biere, A.; Raimi, R.; Zhu, Y. (2001). 「充足可能性解法を用いた有界モデル検査」.システム設計における形式手法. 19 : 7–34 . doi :10.1023/A:1011276507260. S2CID  2484208.
• ジュンキリア、E.タッチェラ、A. (2004)。ジュンキリア、エンリコ。タッケラ、アルマンド (編)。満足性テストの理論と応用。コンピューターサイエンスの講義ノート。 Vol. 2919.土井：10.1007/b95238。ISBN 978-3-540-20851-8. S2CID  31129008。
• Babic, D.; Bingham, J.; Hu, AJ (2006). 「B-Cubing: 効率的なSAT解法の新たな可能性」(PDF) . IEEE Transactions on Computers . 55 (11): 1315. Bibcode :2006ITCmp..55.1315B. doi :10.1109/TC.2006.175. S2CID  14819050. 2016年10月23日時点のオリジナルよりアーカイブ。
• Rodriguez, C.; Villagra, M.; Baran, B. (2007). 「ブール充足可能性のための非同期チームアルゴリズム」(PDF) . 2007 第2回バイオインスパイアード・モデルズ・オブ・ネットワーク、情報、コンピューティングシステム. pp.  66– 69. doi :10.1109/BIMNICS.2007.4610083. S2CID  15185219.
• Gomes, Carla P. ; Kautz, Henry; Sabharwal, Ashish; Selman, Bart (2008). 「充足可能性ソルバー」 Harmelen, Frank Van; Lifschitz, Vladimir; Porter, Bruce (編).知識表現ハンドブック. 人工知能の基礎. 第3巻. Elsevier. pp.  89– 134. doi :10.1016/S1574-6526(07)03002-7. ISBN 978-0-444-52211-5。
• Vizel, Y.; Weissenbacher, G.; Malik, S. (2015). 「ブール充足可能性ソルバーとモデル検査への応用」. Proceedings of the IEEE . 103 (11): 2021– 2035. doi :10.1109/JPROC.2015.2455034. S2CID  10190144.
• Knuth, Donald E. (2022). 「第7章 2.2.2 充足可能性」. 『コンピュータプログラミングの技法』 第4巻B 組合せアルゴリズム パート2. Addison-Wesley Professional. pp.  185– 369. ISBN 978-0-201-03806-4。