ブール充足可能性問題

論理学とコンピュータサイエンスにおいて、ブール充足可能性問題（命題充足可能性問題とも呼ばれ、 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 ]}

3-充足可能性は、 CNF の式において各節が最大k個のリテラルを含む場合、k-充足可能性（k-SAT、またはk-CNF-SAT ）に一般化できます。しかし、 k ≥ 3 の任意の kに対して、この問題は 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-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 の一般的なバリエーションのいくつかをまとめたものです。

名前	コード	3SATの問題？	制限	要件	クラス
3-満足度	3SAT	はい	各節には 3 つのリテラルが含まれます。	少なくとも 1 つのリテラルが true である必要があります。	NP-c
2-充足可能性	2SAT	はい	各節には 2 つのリテラルが含まれます。	少なくとも 1 つのリテラルが true である必要があります。	NL-c
正確に1 3-SAT	1-in-3-SAT	いいえ	各節には 3 つのリテラルが含まれます。	正確に 1 つのリテラルが true である必要があります。	NP-c
正確に1つの肯定的な3-SAT	1-in-3-SAT+	いいえ	各節には 3 つの肯定リテラルが含まれます。	正確に 1 つのリテラルが true である必要があります。	NP-c
すべてが等しいわけではない3つの満足度	NAE3SAT	いいえ	各節には 3 つのリテラルが含まれます。	1 つまたは 2 つのリテラルが true である必要があります。	NP-c
すべてが同じではない肯定的な3-SAT	NAE3SAT+	いいえ	各節には 3 つの肯定リテラルが含まれます。	1 つまたは 2 つのリテラルが true である必要があります。	NP-c
平面SAT	PL-SAT	はい	発生グラフ（節-変数グラフ）は平面グラフです。	少なくとも 1 つのリテラルが true である必要があります。	NP-c
リニアSAT	LSAT	はい	各節には 3 つのリテラルが含まれ、最大 1 つの他の節と交差し、交差は 1 つのリテラルになります。	少なくとも 1 つのリテラルが true である必要があります。	NP-c
ホーンの満足度	HORN-SAT	はい	ホーン節 (最大 1 つの肯定リテラル)。	少なくとも 1 つのリテラルが true である必要があります。	パソコン
XOR充足可能性	XOR-SAT	いいえ	各句には OR ではなく XOR 演算が含まれます。	すべてのリテラルの XOR は true である必要があります。	P

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つの割り当てがあるかどうかを判定する問題です。これは、ちょうど1つの非決定性受理経路が存在する場合に受理し、そうでない場合は棄却する非決定性多項式時間チューリングマシンによって解ける問題を記述する計算量クラスであるUS [ ^{23 ]}に対して完全です。
• UNAMBIGUOUS-SATは、入力式が最大でも1つの満足な割り当てを持つことが約束されている場合の充足可能性問題に付けられた名前です。この問題はUSATとも呼ばれます。^{[ 24 ]} UNAMBIGUOUS-SATを解くアルゴリズムは、複数の満足な割り当てを持つ式に対して、無限ループを含む任意の動作を示すことが許されます。この問題は簡単に思えますが、ValiantとVaziraniは[ ^{25 ] 、}これを解くための実用的な（つまりランダム化多項式時間）アルゴリズムがあれば、 NPのすべての問題も同様に簡単に解けることを示しています。
• MAX-SAT（最大充足可能性問題）は、SATのFNP一般化です。任意の割り当てによって満たされる節の最大数を求めます。効率的な近似アルゴリズムは存在しますが、厳密に解くのはNP困難です。さらに悪いことに、これはAPX完全であり、P=NPでない限り、この問題に対する多項式時間近似スキーム（PTAS）は存在しません。
• WMSATは、単調なブール式（すなわち、否定のない式）を満たす最小の重みの割り当てを求める問題である。命題変数の重みは問題の入力として与えられる。割り当ての重みは、真の変数の重みの合計である。この問題はNP完全である（^{[ 26 ]}の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で構築できるすべてのmaxterm （ただし、 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) (ロシア語)、英語に翻訳：Trakhtenbrot, BA (1984). 「ロシアのペレボル（総当たり探索）アルゴリズムへのアプローチの概観」Annals of the History of Computing . 6 (4): 384– 400. Bibcode : 1984IAHC....6d.384T . 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). 「色付き点の選択と被覆」 .離散応用数学. 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. R. E. 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). 「唯一の充足可能性問題について」情報制御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。