Loading article…
論理学とコンピュータサイエンスにおいて、ブール充足可能性問題（命題充足可能性問題とも呼ばれ、 SATISFIABILITY、SAT、またはB-SATと略される）は、与えられたブール式を満たす解釈が存在するかどうかを判断する問題である。言い換えれば、与えられたブール式の変数を、式が TRUE と評価されるように一貫して TRUE または FALSE の値に置き換えることができるかどうかを問うものである。この場合、式は充足可能 であると呼ばれる。一方、そのような割り当てが存在しない場合、式によって表現される関数はすべての可能な変数割り当てに対してFALSEであり、式は 充足不可能である。たとえば、式「a AND NOT b 」は、( a AND NOT b ) = TRUE となる値a = TRUE およびb = FALSE を見つけることができるため、充足可能である。対照的に、「a AND NOT a」は充足不可能である。
SAT はNP 完全であることが証明された最初の問題です。これはCook–Levin の定理と呼ばれます。これは、広範囲の自然な決定問題と最適化問題を含む複雑性クラスNPのすべての問題が、最大でも SAT と同程度の難しさしかないことを意味します。各 SAT 問題を効率的に解くアルゴリズムは知られておらず、そのようなアルゴリズムは存在しないと一般に信じられていますが、この考えは数学的に証明されておらず、SAT に多項式時間アルゴリズムがあるかどうかという問題を解決することは、計算理論における有名な未解決問題であるP 対 NP 問題と同等です。
それにもかかわらず、2007年現在、ヒューリスティックSATアルゴリズムは、数万の変数と数百万の記号からなる数式を含む問題インスタンスを解くことができ、[1]これは、人工知能、回路設計、[2]および自動定理証明などの多くの実用的なSAT問題には十分です。
定義
命題論理式はブール式とも呼ばれ、変数、演算子 AND (論理積、∧ とも表記)、OR (論理和、∨)、NOT (否定、¬)、括弧から構成されます。式は、適切な論理値(TRUE、FALSE など) を変数に割り当てることで TRUE にできる場合、充足可能であると言われます。ブール充足可能性問題(SAT) は、式が充足可能かどうかを確認する問題です。この決定問題は、理論計算機科学、複雑性理論、[3] [4]アルゴリズム、暗号[5] [6]および人工知能[7]を含む計算機科学の多くの分野で中心的な重要性を持っています。[追加の引用が必要]
連言標準形
リテラルは、変数（この場合は正リテラルと呼ばれる）または変数の否定（負リテラルと呼ばれる）のいずれかです。節は、リテラル（または単一のリテラル）の論理和です。節に含まれる正リテラルが 1 つ以下の場合、その節はホーン節と呼ばれます。式が節の論理積（または単一の節）である場合、 その式は連言標準形（CNF）です。
たとえば、x 1は肯定リテラル、¬ x 2は否定リテラル、x 1 ∨ ¬ x 2は節です。式( x 1 ∨ ¬ x 2 ) ∧ (¬ x 1 ∨ x 2 ∨ x 3 ) ∧ ¬ x 1は連言標準形です。その最初の節と 3 番目の節はホーン節ですが、2 番目の節はホーン節ではありません。この式は、x 1 = FALSE、x 2 = FALSE、x 3 を任意に選択することで満たすことができます。これは、(FALSE ∨ ¬FALSE) ∧ (¬FALSE ∨ FALSE ∨ x 3 ) ∧ ¬FALSE が (FALSE ∨ TRUE) ∧ (TRUE ∨ FALSE ∨ x 3 ) ∧ 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 1 ,..., l n )となります。許可されるブール関数のセットが異なると、問題のバージョンも異なります。たとえば、R (¬ x , a , b ) は一般化節であり、R (¬ x , a , b ) ∧ R ( b , y , c ) ∧ R ( c , d ,¬ z ) は一般化連言正規形です。この公式は以下で使用され、R は、その引数の 1 つが TRUE である場合にのみ TRUE となる三項演算子です。
ブール代数の法則を用いると、あらゆる命題論理式は等価な連言正規形に変換できるが、その場合、指数関数的に長くなる可能性がある。例えば、式 ( x 1 ∧ y 1 ) ∨ ( x 2 ∧ y 2 ) ∨ ... ∨ ( x n ∧ y n ) を連言正規形に変換すると、次の式が得られる。
- ( x 1 ∨ x 2 ∨ … ∨ x n ) ∧
- ( y 1 ∨ x 2 ∨ … ∨ x n ) ∧
- ( x 1 ∨ y 2 ∨ … ∨ x n ) ∧
- ( y 1 ∨ y 2 ∨ … ∨ x n ) ∧ ... ∧
- ( x 1 ∨ x 2 ∨ … ∨ y n ) ∧
- ( y 1 ∨ x 2 ∨ … ∨ y n ) ∧
- ( x 1 ∨ y 2 ∨ … ∨ y n ) ∧
- ( y 1 ∨ y 2 ∨ … ∨ y n ) ;
前者は2 変数のn 個の連言の選言ですが、後者はn変数の2 n個の節で構成されます。
しかし、 Tseytin変換を使用すると、元の命題論理式のサイズに線形な長さを持つ、等充足可能な連言標準形式が見つかる場合があります。
複雑
SAT はNP 完全であることが知られる最初の問題であり、1971 年にトロント大学のStephen Cookによって証明され[8]、1973 年にロシア科学アカデミーのLeonid Levinによって独立に証明されました[9]。その時まで、NP 完全問題という概念は存在すらしていませんでした。その証明は、複雑性クラスNPのすべての決定問題が CNF [注 1]式の SAT 問題( CNFSATと呼ばれることもあります) に還元される方法を示しています。Cookの還元の便利な特性は、受理解の数を保存することです。たとえば、与えられたグラフに3 色があるかどうかを判断することは、NP の別の問題です。グラフに 17 個の有効な 3 色がある場合、Cook–Levin 還元によって生成される SAT 式には 17 個の満足する割り当てがあります。
NP 完全性は、最悪のケースの実行時間のみを指します。実際のアプリケーションで発生するインスタンスの多くは、はるかに速く解決できます。以下の §SAT を解決するためのアルゴリズムを参照してください。
3-満足可能性
任意の論理式の充足可能性問題と同様に、各節が最大3つのリテラルに制限されている連言正規形の論理式の充足可能性を決定することもNP完全です。この問題は、3-SAT、3CNFSAT、または3-充足可能性と呼ばれます。無制限のSAT問題を3-SATに縮小するには、各節l 1 ∨ ⋯ ∨ l nをn - 2個の節 の連言に変換します。
- ( l 1 ∨ l 2 ∨ x 2 ) ∧
- (¬ x 2 ∨ l 3 ∨ x 3 ) ∧
- (¬ x 3 ∨ l 4 ∨ x 4 ) ∧ ⋯ ∧
- (¬ x n −3 ∨ l n −2 ∨ x n −2 ) ∧
- (¬ x n −2 ∨ l n −1 ∨ l n )
ここで、x 2、⋯ 、 x n −2は他には現れない新しい変数である。2つの式は論理的には同値ではないが、等価である。すべての節を変換して得られる式は、最大で元の式の3倍の長さになる。つまり、長さの増加は多項式である。[10]
3-SAT はKarp の 21 個の NP 完全問題のうちの 1 つであり、他の問題もNP 困難であることを証明するための出発点として使用されます。[注 2]これは、3-SAT から他の問題への多項式時間還元によって行われます。この方法が使用されている問題の例としては、クリーク問題があります。c個の節からなる CNF 式が与えられた場合、対応するグラフは各リテラルの頂点と、異なる節からの矛盾しない 2 つのリテラル間の辺で構成されます。図を参照してください。グラフにcクリークが存在するのは、式が充足可能である場合のみです。[11]
Schöning (1999)による単純なランダム化アルゴリズムがあり、これは(4/3) n時間で実行され、3-SAT命題の変数の数nで、高い確率で3-SATを正しく決定することに成功します。[12]
指数時間仮説は、3-SAT（または任意のk > 2に対するk -SAT）をexp( o ( n ))時間（つまり、nにおける指数関数よりも基本的に速い）で解くことができるアルゴリズムは存在しないと主張しています。
セルマン、ミッチェル、レベスク（1996）は、ランダムに生成された3-SAT式の難易度について、そのサイズパラメータに応じた実証データを示しています。難易度は、DPLLアルゴリズムによる再帰呼び出しの数で測定されます。彼らは、節対変数比が約4.26のときに、ほぼ確実に満足できる式からほぼ確実に満足できない式への相転移領域を特定しました。[13]
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 1 ∨ ⋯ ∨ l jは、固定ダミー変数を使用してl 1 ∨ ⋯ ∨ l j ∨ d j +1 ∨ ⋯ ∨ d kにパディングできるためです。すべての節をパディングした後、d 1 = ⋯ = d k = FALSEのみが満足のいく割り当てにつながることを保証するために、2 k –1 個の追加節 [注 4] を追加する必要があります。k は式の長さに依存しないため、追加節によって長さが一定に増加します。同じ理由で、 ¬ x ∨ ¬ y ∨ ¬ yのように、節で重複するリテラルが許可されるかどうかは問題ではありません。
SATの特別なケース
連言標準形
連言標準形 (特に節ごとに 3 つのリテラル) は、SAT 式の標準的な表現であると考えられることがよくあります。上記のように、一般的な SAT 問題は、この形式の式の充足可能性を決定する問題である 3-SAT に簡略化されます。
選言正規形
SAT は、式が選言正規形のものに制限されている場合、つまり、リテラルの連言の選言である場合に、自明です。そのような式が実際に満足可能であるのは、少なくとも 1 つの連言が満足可能である場合であり、連言が満足可能であるのは、ある変数xについてxと NOT x の両方を含まない場合です。これは線形時間で確認できます。さらに、式が完全な選言正規形に制限されている場合(すべての変数がすべての連言に 1 回だけ出現する)、定数時間で確認できます (各連言は 1 つの満足する割り当てを表します)。ただし、一般的な SAT 問題を選言正規形に変換するには、指数的な時間とスペースがかかります。例を取得するには、上記の指数関数的な爆発例の "∧" と "∨" を連言正規形に置き換えます。
正確に1 3 の充足可能性
3-充足可能性問題の変形として、3 分の 1 の 3-SAT ( 1-in-3-SATやexact-1 3-SATとも呼ばれる) があります。節ごとに 3 つのリテラルを含む連言正規形が与えられた場合、問題は、各節にちょうど1 つの TRUE リテラル (したがってちょうど 2 つの FALSE リテラル) が含まれるように変数に真理値を割り当てる方法が存在するかどうかを判断することです。対照的に、通常の 3-SAT では、すべての節に少なくとも1 つの TRUE リテラルが必要です。正式には、3 分の 1 の 3-SAT 問題は、引数のちょうど 1 つが TRUE の場合にだけ TRUE となる三項演算子R を使用するすべての一般化節を含む一般化連言正規形として与えられます。3 分の 1 の 3-SAT 式のすべてのリテラルが正の場合、充足可能性問題は3 分の 1 の正の 3-SATと呼ばれます。
3分の1の3-SATは、その肯定的なケースとともに、マイケル・R・ギャリーとデビッド・S・ジョンソンによる標準参考文献「コンピュータと扱いにくさ：NP完全性理論のガイド」にNP完全問題「LO4」として記載されています。3分の1の3-SATは、トーマス・ジェローム・シェーファーによってシェーファーの二分法定理の特別なケースとしてNP完全であることが証明されました。シェーファーの二分法定理は、ブール充足可能性を特定の方法で一般化する問題はクラスPにあるか、NP完全であるかのいずれかであると主張しています。[14]
Schaefer は、3-SAT から 3 分の 1 の 3-SAT への簡単な多項式時間削減を可能にする構成を示しています。"( xまたはyまたはz )" を 3CNF 式の節とします。この節のみをシミュレートするために使用する 6 つの新しいブール変数a、b、c、d、e、およびf を追加します。すると、式R ( x、a、d ) ∧ R ( y、b、d ) ∧ R ( a、b、e ) ∧ R ( c、d、f ) ∧ R ( z、c 、 FALSE) は、 x、y、またはzの少なくとも 1 つが TRUE である場合に限り、新しい変数の設定によって満たされます(図 (左) を参照)。したがって、 m個の節とn個の変数を持つ3-SATインスタンスは、5m個の節とn + 6m個の変数を持つ、3分の1が等価な3-SATインスタンスに変換できます。[15]もう1つの削減では、4つの新しい変数と3つの節のみが含まれます。R (¬ x、a、b ) ∧ R ( b、y、c ) ∧ R( c、d、¬ z )、図（右）を参照してください。
すべてが等しくない 3 満足可能性
もう一つの変種は、全てが等しくない3-充足可能性問題（ NAE3SATとも呼ばれる）である。節ごとに3つのリテラルを持つ連言正規形が与えられた場合、どの節でも3つのリテラルすべてが同じ真理値を持たないような変数への割り当てが存在するかどうかを判断するという問題である。この問題も、シェーファーの二分法定理により、否定記号が認められない場合でもNP完全である。[14]
リニアSAT
3-SAT 式は、各節（リテラルの集合として）が最大で 1 つの他の節と交差し、さらに、2 つの節が交差する場合、それらの節にはちょうど 1 つのリテラルが共通している場合、線形 SAT (LSAT) です。LSAT 式は、直線上の互いに素な半閉区間の集合として表すことができます。LSAT 式が充足可能かどうかを判断することは NP 完全です。[16]
2-満足可能性
節内のリテラルの数が最大 2 に制限されている場合、 SAT はより簡単になります。この場合、問題は2-SATと呼ばれます。この問題は多項式時間で解決でき、実際、複雑性クラスNLに対して完全です。さらに、リテラル内のすべての OR 演算がXOR演算に変更された場合、結果は排他的論理和 2-充足可能性と呼ばれ、複雑性クラスSL = Lに対して完全な問題です。
ホーンの満足度
与えられたホーン節の論理積の充足可能性を決定する問題は、ホーン充足可能性、またはHORN-SATと呼ばれる。これは、ホーン節の集合（TRUEに割り当てられたリテラルの集合に関して）の単一の最小モデルを生成する単位伝播アルゴリズムの1つのステップによって多項式時間で解決できる。ホーン充足可能性はP完全である。これはブール充足可能性問題のPバージョンと見なすことができる。また、量化ホーン式の真偽の決定は多項式時間で行うことができる。[17]
ホーン節は、1 つの変数が他の一連の変数からどのような含意を持つかを表現できるため、興味深いものです。実際、そのような節の 1 つである ¬ x 1 ∨ ... ∨ ¬ x n ∨ y は、 x 1 ∧ ... ∧ x n → yと書き換えることができます。つまり、x 1、...、x nがすべて TRUE の場合、y もTRUE である必要があります。
ホーン論理式のクラスの一般化は、名前変更可能なホーン論理式です。これは、いくつかの変数をそれぞれの否定に置き換えることでホーン形式にすることができる論理式の集合です。たとえば、 ( x 1 ∨ ¬ x 2 ) ∧ (¬ x 1 ∨ x 2 ∨ x 3 ) ∧ ¬ x 1はホーン論理式ではありませんが、y 3 をx 3の否定として導入することで、ホーン論理式 ( x 1 ∨ ¬ x 2 ) ∧ (¬ x 1 ∨ x 2 ∨ ¬ y 3 ) ∧ ¬ x 1に名前変更できます。対照的に、( x 1 ∨ ¬ x 2 ∨ ¬ x 3 ) ∧ (¬ x 1 ∨ x 2 ∨ x 3 ) ∧ ¬ x 1の名前変更はホーン公式につながります。このような置換の存在の確認は線形時間で行うことができます。したがって、このような公式の充足可能性は、最初にこの置換を実行し、次に結果のホーン公式の充足可能性をチェックすることで解決できるため、P に含まれます。
XOR 充足可能性
もう 1 つの特殊なケースは、各節に(単純な) OR 演算子ではなくXOR (つまり排他的論理和) が含まれる問題のクラスです。 [注 5]これはPに属します。XOR-SAT 式は 2 を法とする線型方程式のシステムと見なすこともできるため、ガウスの消去法によって 3 次時間で解くことができます。[18]例についてはボックスを参照してください。この書き直しは、ブール代数とブール環 の親族関係と、2 を法とする算術が有限体 を形成するという事実に基づいています。a XOR b XOR c が TRUE と評価されるのは、{a、b、c} の要素のうち 1 つまたは 3 つが TRUE である場合のみであるため、特定のCNF式の1 - in - 3 -SAT 問題の各解は XOR-3-SAT 問題の解でもあり、XOR-3-SAT の各解は 3-SAT の解です。図を参照してください。その結果、各 CNF 式について、式で定義された XOR-3-SAT 問題を解決し、その結果に基づいて 3-SAT 問題が解決可能であるか、1-in-3-SAT 問題が解決不可能であるかを推論することが可能になります。
複雑性クラス P と NP が等しくない場合、SAT とは異なり、2 充足可能性、ホーン充足可能性、XOR 充足可能性のいずれも NP 完全ではありません。
シェーファーの二分法定理
上記の制約 (CNF、2CNF、3CNF、Horn、XOR-SAT) は、検討対象の式をサブ式の連言として制限します。各制約は、すべてのサブ式の特定の形式を指定します。たとえば、2CNF では、2 項節のみがサブ式になることができます。
シェーファーの二分法定理は、これらの部分式を形成するために使用できるブール関数の任意の制限に対して、対応する充足可能性問題はPまたはNP完全であると述べています。2CNF、ホーン、およびXOR-SAT式の充足可能性のPへの帰属は、この定理の特別なケースです。[14]
次の表は、SAT の一般的なバリエーションのいくつかをまとめたものです。
SATの拡張
2003年以降、大きな人気を集めている拡張は、CNF式に線形制約、配列、すべて異なる制約、解釈されない関数などを追加できる、充足可能性法理論（SMT）です。[ 19 ]このような拡張は通常NP完全のままですが、現在では多くの種類の制約を処理できる非常に効率的なソルバーが利用可能です。
ブール変数をバインドするために「すべてに対して」( ∀ ) と「存在する」( ∃ )の両方の量指定子が許可されている場合、充足可能性問題はより困難になります。そのような式の例は、 ∀ x ∀ y ∃ z ( x ∨ y ∨ z ) ∧ (¬ x ∨ ¬ y ∨ ¬ z )です。これは有効です。なぜなら、xとyのすべての値に対して、 zの適切な値を見つけることができるからです。つまり、 xとyの両方が FALSE の場合はz =TRUE 、それ以外の場合はz =FALSE です。SAT 自体は (暗黙的に) ∃ 量指定子のみを使用します。代わりに ∀ 量指定子のみが許可されている場合、いわゆるトートロジー問題が得られ、これはco-NP 完全です。両方の量指定子が許可されている場合、問題は量指定ブール式問題（QBF ）と呼ばれ、 PSPACE完全であることが示されます。PSPACE完全問題はNPのどの問題よりも厳密に難しいと広く信じられていますが、これはまだ証明されていません。高度に並列化されたPシステムを使用すると、QBF-SAT問題は線形時間で解くことができます。[20]
通常の SAT では、式が成り立つような変数割り当てが少なくとも 1 つあるかどうかを尋ねます。さまざまなバリエーションで、そのような割り当ての数を扱います。
- MAJ-SAT では、すべての割り当ての大多数が式を TRUE にするかどうかを尋ねます。確率クラスであるPPでは完全であることがわかっています。
- #SAT、つまり式を満たす変数割り当ての数を数える問題は、決定問題ではなく計数問題であり、 #P 完全です。
- UNIQUE SAT [21]は、式にちょうど1つの割り当てがあるかどうかを判断する問題です。これは、ちょうど1つの非決定性受理パスがある場合に受理し、そうでない場合は拒否する非決定性多項式時間チューリングマシンによって解決可能な問題を記述する複雑性クラスであるUS [22]に対して完全です。
- UNAMBIGUOUS-SATは、入力が最大で1つの満足する割り当てを持つ式に制限されている場合の満足度問題に付けられた名前です。この問題はUSATとも呼ばれます。[23] UNAMBIGUOUS-SATを解くアルゴリズムは、複数の満足する割り当てを持つ式に対して、無限ループを含む任意の動作を示すことが許可されています。この問題は簡単に思えますが、ValiantとVaziraniは[ 24]、これを解くための実用的な（つまり、ランダム化多項式時間）アルゴリズムがあれば、 NPのすべての問題が同じように簡単に解けることを示しています。
- MAX-SAT、つまり最大充足問題とは、 SAT のFNP一般化です。これは、任意の割り当てによって満たすことができる節の最大数を要求します。効率的な近似アルゴリズムがありますが、正確に解くのは NP 困難です。さらに悪いことに、これはAPX完全であり、つまり、P=NP でない限り、この問題に対する多項式時間近似スキーム(PTAS)は存在しません。
- WMSATは、単調なブール式（つまり、否定のない式）を満たす最小の重みの割り当てを見つける問題です。命題変数の重みは、問題の入力で与えられます。割り当ての重みは、真の変数の重みの合計です。この問題はNP完全です（ [25]のTh.1を参照）。
その他の一般化には、第一および第二階論理の充足可能性、制約充足問題、0-1 整数計画法などがあります。
満足のいく仕事を見つける
SAT は決定問題ですが、満足できる割り当てを見つける検索問題は SAT に帰着します。つまり、SAT のインスタンスが解決可能かどうかを正しく答える各アルゴリズムは、満足できる割り当てを見つけるために使用できます。まず、与えられた式 Φ について質問されます。答えが「いいえ」の場合、式は満たされません。それ以外の場合は、部分的にインスタンス化された式 Φ { x 1 =TRUE}、つまり最初の変数x 1がTRUE に置き換えられ、それに応じて簡略化された Φ について質問されます。答えが「はい」の場合、x 1 =TRUE になり、それ以外の場合はx 1 =FALSE になります。他の変数の値は、同じ方法で後で見つけることができます。合計で、アルゴリズムのn +1 回の実行が必要です。ここで、 nは Φ 内の異なる変数の数です。
この特性は複雑性理論のいくつかの定理で使用されています。
SATを解くアルゴリズム
SAT問題はNP完全であるため、指数関数的な最悪ケースの複雑性を持つアルゴリズムのみが知られています。それにもかかわらず、SATの効率的でスケーラブルなアルゴリズムは2000年代に開発され、数万の変数と数百万の制約（つまり節）を含む問題インスタンスを自動的に解決する能力の劇的な進歩に貢献しました。[1]電子設計自動化（EDA）におけるそのような問題の例としては、形式的等価性チェック、モデルチェック、パイプライン化されたマイクロプロセッサの形式的検証、[19]自動テストパターン生成、FPGAの配線、[26]計画およびスケジューリングの問題などがあります。SAT解決エンジンは、電子設計自動化ツールボックスに不可欠なコンポーネントとも考えられています。
現代のSATソルバーが使用する主な手法には、デイビス・パトナム・ローゲマン・ラブランドアルゴリズム（DPLL）、衝突駆動節学習（CDCL）、およびWalkSATなどの確率的 局所探索アルゴリズムがあります。ほぼすべてのSATソルバーにはタイムアウトが含まれているため、解が見つからない場合でも妥当な時間で終了します。SATソルバーによって、簡単または難しいインスタンスが異なり、不満足性の証明に優れているものもあれば、解を見つけることに優れているものもあります。最近[いつ? ]、ディープラーニング技術を使用してインスタンスの満足可能性を学習する試みが行われています。[27]
SATソルバーはSATソルバーコンテストで開発され、比較されています。[28]現代のSATソルバーは、ソフトウェア検証、人工知能における制約解決、オペレーションズリサーチなどの分野にも大きな影響を与えています。
参照
注記
- ^ 任意の式の SAT 問題も NP 完全です。NP であることが簡単に示されるため、CNF 式の SAT よりも簡単になることはあり得ません。
- ^ つまり、少なくとも NP の他のすべての問題と同じくらい難しい。決定問題は、NP に属し、NP 困難である場合にのみ NP 完全です。
- ^ つまり、一方のリテラルが他方のリテラルの否定ではない
- ^ すなわち、d 1 ,⋯, d kで構築できるすべての最大項（ただし、d 1 ∨⋯∨ d kを除く）
- ^正式には、3 項ブール関数 Rを持つ一般化された連言正規形が採用されており、これは引数の 1 つまたは 3 つが TRUE の場合にのみ TRUE になります。3 つ以上のリテラルを持つ入力節は、上記と同様に 3 つのリテラルを持つ節の等充足可能な連言に変換できます。つまり、XOR-SAT は XOR-3-SAT に縮小できます。
外部リンク
ウィキメディア・コモンズには、ブール充足問題に関連するメディアがあります。
- SAT ゲーム: ブール充足可能性問題を自分で解いてみよう
- 国際SATコンテストウェブサイト
- 満足度テストの理論と応用に関する国際会議
- 満足度、ブールモデリング、計算に関するジャーナル
- SAT Live、充足可能性問題に関する研究の総合ウェブサイト
- MaxSATソルバーの年次評価
参考文献
- ^ ab 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ソルバーは、
数百万の制約と数十万の変数を持つ問題を扱うことができることが多い。
。 - ^ Hong, Ted; Li, Yanjing; Park, Sung-Boem; Mui, Diana; Lin, David; Kaleq, Ziyad Abdel; Hakim, Nagib; Naeimi, Helia; Gardner, Donald S.; Mitra, Subhasish (2010 年 11 月)。「QED: 効果的なポストシリコン検証のためのクイック エラー検出テスト」。2010 IEEE 国際テスト会議。pp. 1–10。doi : 10.1109 / TEST.2010.5699215。ISBN 978-1-4244-7206-2. S2CID 7909084。
- ^ Karp, Richard M. (1972)。「組み合わせ問題における縮約可能性」(PDF)。Raymond E. Miller、James W. Thatcher (編)。『コンピュータ計算の複雑性』。ニューヨーク: Plenum。pp. 85–103。ISBN 0-306-30707-3. 2011年6月29日時点のオリジナル（PDF）からアーカイブ。2020年5月7日閲覧。こちら: p.86
- ^ Aho, Alfred V.; Hopcroft, John E.; Ullman, Jeffrey D. (1974).コンピュータアルゴリズムの設計と分析. Addison-Wesley. p. 403. ISBN 0-201-00029-6。
- ^ Massacci, Fabio; Marraro, Laura (2000-02-01). 「SAT 問題としての論理暗号解析」. Journal of Automated Reasoning . 24 (1): 165–203. doi :10.1023/A:1006326723002. S2CID 3114247.
- ^ Mironov, Ilya; Zhang, Lintao (2006)。「ハッシュ関数の暗号解析への SAT ソルバーの応用」。Biere, Armin; Gomes, Carla P. (編)。充足可能性テストの理論と応用 - SAT 2006。コンピュータサイエンスの講義ノート。第 4121 巻。Springer。pp. 102–115。doi :10.1007/ 11814948_13。ISBN 978-3-540-37207-3。
- ^ Vizel, Y .; Weissenbacher, G.; Malik, S. ( 2015). 「ブール充足可能性ソルバーとモデル検査におけるその応用」。IEEE紀要。103 (11): 2021–2035。doi :10.1109/JPROC.2015.2455034。S2CID 10190144 。
- ^ 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-09 にオリジナルからアーカイブ(PDF)されました。
- ^ レビン、レオニード(1973)。 「ユニバーサル検索問題 (ロシア語: Универсальные задачи перебора, Universal'nye perebornye zadachi)」。情報伝達の問題 (ロシア語: Проблемы передачи информа́ции、問題のあるペレダチ情報ii)。9 (3): 115–116。(pdf) (ロシア語)、英語に翻訳、 Trakhtenbrot, BA (1984)。 「ロシアのペレボル(総当たり検索) アルゴリズムへのアプローチの調査」 Annals of the History of Computing。6 (4): 384–400。doi :10.1109/MAHC.1984.10036。S2CID 950581。
- ^ Aho、Hopcroft、Ullman（1974）、定理10.4。
- ^ Aho、Hopcroft、Ullman（1974）、定理10.5。
- ^ 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）されました。
- ^ セルマン、バート、ミッチェル、ヘクター・レベスク (1996)。「困難な満足可能性問題の生成」。人工知能。81 ( 1–2 ): 17–29。CiteSeerX 10.1.1.37.7362。doi :10.1016/ 0004-3702 (95)00045-3。
- ^ abc Schaefer, Thomas J. (1978). 「充足可能性問題の複雑さ」(PDF) .第 10 回 ACM コンピューティング理論シンポジウム議事録. サンディエゴ、カリフォルニア州 . pp. 216–226. CiteSeerX 10.1.1.393.8951 . doi :10.1145/800133.804350.
- ^ Schaefer (1978)、p.222、補題3.5。
- ^ 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.
- ^ Buning, HK; Karpinski, Marek; Flogel, A. (1995). 「定量化されたブール式の解像度」.情報と計算. 117 (1). エルゼビア: 12–18. doi : 10.1006/inco.1995.1025 .
- ^ ムーア、クリストファー、メルテンス、ステファン（2011）、計算の性質、オックスフォード大学出版局、p. 366、ISBN 9780199233212。
- ^ ab RE Bryant、SM German、MN Velev、「解釈されていない関数を持つ等価性ロジックの効率的な決定手順を使用したマイクロプロセッサ検証」、Analytic Tableaux and Related Methods、pp. 1–13、1999年。
- ^ Alhazov, Artiom; Martín-Vide, Carlos; Pan, Linqiang (2003). 「制限されたアクティブ膜を持つPシステムを認識してPSPACE完全問題を解決する」Fundamenta Informaticae . 58 : 67–77.ここでは: セクション3、Thm.3.1
- ^ 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.
- ^ 「Complexity Zoo:U - Complexity Zoo」. complexityzoo.uwaterloo.ca . 2019年7月9日時点のオリジナルよりアーカイブ。2019年12月5日閲覧。
- ^ Kozen, Dexter C. (2006). 「補足講義 F: 一意の充足可能性」.計算理論. コンピュータサイエンスのテキスト. Springer. p. 180. ISBN 9781846282973。
- ^ Valiant, L.; Vazirani, V. ( 1986). 「NPは一意の解を検出するのと同じくらい簡単です」（PDF）。理論計算機科学。47 :85–93。doi : 10.1016 /0304-3975(86)90135-0。
- ^ Buldas, Ahto; Lenin, Aleksandr; Willemson, Jan; Charnamord, Anton (2017). 「攻撃ツリーのシンプルな実行不可能性証明書」。Obana, Satoshi、Chida, Koji (編著)。情報とコンピューターセキュリティの進歩。コンピューターサイエンスの講義ノート。Vol. 10418。Springer International Publishing。pp. 39–55。doi :10.1007/978-3-319-64200-0_3。ISBN 9783319642000。
- ^ Gi-Joon Nam; Sakallah, KA; Rutenbar, RA (2002). 「検索ベースのブール充足可能性による新しい FPGA 詳細ルーティング アプローチ」(PDF) . IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems . 21 (6): 674. doi :10.1109/TCAD.2002.1004311. 2016 年 3 月 15 日のオリジナル(PDF)からアーカイブ。2015年 9 月 4 日に取得。
- ^ Selsam, Daniel; Lamm, Matthew; Bünz, Benedikt; Liang, Percy; de Moura, Leonardo; Dill, David L. (2019年3月11日). 「シングルビット監視からのSATソルバーの学習」. arXiv : 1802.03685 [cs.AI].
- ^ 「国際SATコンペティションのウェブページ」。2007年11月15日閲覧。
出典
- この記事には、 Karem A. Sakallah教授による https://web.archive.org/web/20070708233347/http://www.sigda.org/newsletter/2006/eNews_061201.html の資料が含まれています。
さらに読む
（発行日順）
- ゲイリー、マイケル R. ;ジョンソン、デビッド S. (1979)。コンピュータと扱いにくさ: NP 完全性理論のガイド。WH フリーマン。pp. A9.1: LO1–LO7、pp. 259–260。ISBN 0-7167-1045-5。
- Marques-Silva, J.; Glass, T. (1999)。「充足可能性と再帰学習を使用した組み合わせ同値性チェック」。Design, Automation and Test in Europe Conference and Exhibition、1999。議事録 (カタログ番号 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. doi :10.1109/TC.2006.175. S2CID 14819050.
- 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)。「Satisfiability Solvers」。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). 「ブール充足可能性ソルバーとモデル検査におけるその応用」。IEEE論文集。103 (11): 2021–2035。doi : 10.1109 /JPROC.2015.2455034。S2CID 10190144 。
- Knuth, Donald E. (2022)。「第 7.2.2.2 章: 充足可能性」。コンピュータプログラミングの芸術。第 4B 巻: 組み合わせアルゴリズム、パート 2。Addison-Wesley Professional。pp. 185–369。ISBN 978-0-201-03806-4。