Loading article…
論理学やコンピュータサイエンスにおいて、ブール充足可能性問題（命題充足可能性問題とも呼ばれ、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 に多項式時間アルゴリズムが存在するかどうかの問題を解決すれば、計算理論における最も重要な未解決問題の 1 つですが、P 対 NP 問題が解決されます。 [ 1 ] [ 2 ]
それにもかかわらず、ヒューリスティックSATアルゴリズムは、数万の変数と数百万の記号からなる数式を含む問題インスタンスを解くことができ、[ 3 ]これは人工知能、回路設計、[ 4 ]および自動定理証明で発生する多くの実用的なSAT問題には十分である。
命題論理式（ブール式とも呼ばれる）は、変数、演算子 AND（論理積、∧ とも表記される）、OR（論理和、∨）、NOT（否定、¬）、および括弧から構成されます。式は、その変数に適切な論理値（つまり、TRUE、FALSE）を割り当てることで TRUE にできる場合に充足可能であると言われます。ブール充足可能性問題（SAT）は、与えられた式が充足可能かどうかを判定する問題です。この決定問題は、理論計算機科学、計算複雑性理論[ 5 ] [ 6 ]、アルゴリズム、暗号[ 7 ] [ 8 ]、人工知能[ 9 ]など、コンピュータ科学の多くの分野で中心的な重要性を持っています。
リテラルは、変数（この場合、正のリテラルと呼ばれる）か、変数の否定（負のリテラルと呼ばれる）のいずれかです。節は、リテラルの選言（または単一のリテラル）です。節は、正のリテラルを最大で1つしか含まない場合、ホーン節と呼ばれます。式は、節の連言（または単一の節）である場合、連言標準形（CNF）です。
例えば、x 1は正のリテラル、¬ x 2は負のリテラル、x 1 ∨ ¬ x 2は節です。式( x 1 ∨ ¬ x 2 ) ∧ (¬ x 1 ∨ x 2 ∨ x 3 ) ∧ ¬ x 1は連言標準形です。その第 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 ) を連言標準形に変換すると、次のようになります。
前者は2つの変数のn個の連言の選言であるのに対し、後者はn個の変数の2n個の節から構成される。
しかし、ツェイティン変換を用いることで、元の命題論理式のサイズに比例する長さを持つ、等充足可能な連言標準形式を見つけることができる。
SAT は、1971 年にトロント大学のスティーブン・クック[ 10 ]と、 1973 年にロシア科学アカデミーのレオニード・レヴィン[ 11 ]によって独立に証明された、NP 完全であることが知られている最初の問題です。それまでは、NP 完全問題の概念は存在しませんでした。証明は、複雑性クラスNPのすべての決定問題が、CNF [ a ]式の SAT 問題 ( CNFSATと呼ばれることもあります) に還元できることを示しています。クックの還元の有用な特性は、受理する回答の数を保存することです。たとえば、与えられたグラフが3 色で彩色されているかどうかを判定することは、NP の別の問題です。グラフに 17 通りの有効な 3 色で彩色されている場合、クックとレヴィンの還元によって生成される SAT 式には 17 通りの満足する割り当てがあります。
NP完全性とは、最悪の場合の実行時間のみを指します。実際のアプリケーションで発生する多くのインスタンスは、はるかに高速に解決できます。詳しくは、下記の「SATを解くためのアルゴリズム」を参照してください。
任意の式の充足可能性問題と同様に、各節が最大 3 つのリテラルに制限されている連言標準形の式の充足可能性を判定することも NP 完全です。この問題は3-SAT、3CNFSAT、または3-充足可能性と呼ばれます。制限のない SAT 問題を 3-SAT に還元するには、各節l 1 ∨ ⋯ ∨ l n をn - 2個の節の連言に変換します。
ここで、x 2、⋯ 、x n −2は、他の場所には現れない新しい変数です。 2 つの式は論理的に同等ではありませんが、同等に充足可能です。 すべての節を変換して得られる式は、元の式の 3 倍以下です。つまり、長さの増加は多項式です。[ 12 ]
3-SAT は、Karp の 21 個の NP 完全問題の 1 つであり、他の問題もNP 困難であることを証明するための出発点として使用されます。[ b ]これは、3-SAT から他の問題への多項式時間還元によって行われます。この方法が使用された問題の例として、クリーク問題があります。c 個の節からなる CNF 式が与えられた場合、対応するグラフは、各リテラルに対応する頂点と、異なる節からの矛盾しない 2 つのリテラル間のエッジで構成されます。図を参照してください。グラフは、式が充足可能である場合に限り、c クリークを持ちます。 [ 13 ]
Schöning (1999) による単純なランダム化アルゴリズムがあり、実行時間は (4/3) nで、 nは 3-SAT 命題の変数の数であり、3-SAT を正しく判定する確率が高い。[ 14 ]
指数時間仮説は、3-SAT（または実際には任意のk > 2に対するk -SAT）をexp( o ( n ))時間（つまり、nに関して指数関数的に速い）で解くアルゴリズムは存在しないと主張している。
セルマン、ミッチェル、ルヴェスク（1996）は、ランダムに生成された3-SAT式の難易度を、そのサイズパラメータに応じて実証的に示しています。難易度は、DPLLアルゴリズムによって行われる再帰呼び出しの数で測定されます。彼らは、節と変数の比率が約4.26のときに、ほぼ確実に充足可能な式からほぼ確実に充足不可能な式への相転移領域を特定しました。[ 15 ]
3-充足可能性は、各節に最大k個のリテラルが含まれる CNF の式を考慮すると、 k-充足可能性( k -SAT、またはk -CNF-SAT ) に一般化できます。 [ 16 ]しかし、任意のk ≥ 3に対して、この問題は 3-SAT より簡単にも SAT より難しくもなり得ず、後者 2 つは NP 完全であるため、k -SAT でなければなりません。
一部の著者は、k -SATをちょうどk個のリテラルを持つCNF式に限定している。しかし、 k個未満のリテラルを持つ各節は、同じリテラルの繰り返しコピーで埋めることができるため、これも異なる複雑性クラスにはつながらない。[ 17 ]
ランダムに生成された節を持つk -SAT 問題の充足可能性と解空間の幾何学が統計的に調査されています。節と変数の比率 (密度とも呼ばれる) の関数として、モデルは充足可能性と解空間の幾何学に関してさまざまな相転移を示します。充足可能性については、密度がこの閾値を下回る場合に限り、高い確率で解が存在するような明確な閾値が存在します。[ 18 ]充足可能性の閾値をはるかに下回ると、解空間は幾何学的相転移も起こし、指数関数的に多くの、十分に分離されたクラスターに分裂します。この相転移の開始は既知のアルゴリズムの閾値と一致しており、幾何学とアルゴリズムの扱いにくさの間の関連性を示唆しています。[ 19 ] [ 20 ]
連言標準形（特に節ごとに3つのリテラルを含む形式）は、SAT式の標準的な表現としてよく用いられます。上記のように、一般的なSAT問題は、この形式の式の充足可能性を判定する問題である3-SATに帰着します。
3-SAT 式は、各節(リテラルの集合とみなした場合)が他の節と最大で 1 つしか交差せず、さらに、2 つの節が交差する場合、それらがちょうど 1 つのリテラルを共有する場合に、線形 SAT ( LSAT ) である。LSAT 式は、直線上の互いに素な半閉区間の集合として表現できる。LSAT 式が充足可能かどうかを判定することは NP 完全である。[ 21 ]
節内のリテラルの数が最大で 2 に制限されている場合、SAT はより簡単になります。この場合、問題は2-SATと呼ばれます。この問題は多項式時間で解くことができ、実際には複雑性クラスNLに対して完全です。さらに、リテラル内のすべての OR 演算をXOR演算に変更すると、結果は排他的 OR 2-充足可能性と呼ばれ、これは複雑性クラスSL = Lに対して完全な問題です。
与えられたホーン節の論理積の充足可能性を判定する問題は、ホーン充足可能性、またはHORN-SATと呼ばれます。これは、単位伝播アルゴリズムの1ステップで多項式時間で解くことができ、ホーン節の集合の最小モデル（TRUEに割り当てられたリテラルの集合に関して）を生成します。ホーン充足可能性はP完全です。これは、ブール充足可能性問題のP版と見なすことができます。また、量化されたホーン式の真偽判定も多項式時間で行うことができます。[ 22 ]
ホーン節は、ある変数から他の変数の集合への含意を表現できるため興味深い。実際、そのような節 ¬ 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はホーン式ではありませんが、 x 3の否定としてy 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 に属する。これは、まずこの置換を実行し、次に結果として得られるホーン式の充足可能性を確認することで解決できるからである。
SAT は、式が選言標準形、つまりリテラルの連言の選言に限定されている場合は自明です。このような式は、その連言の少なくとも 1 つが充足可能である場合に限り充足可能であり、連言は、ある変数xに対してxと NOT x の両方を含まない場合に限り充足可能です。これは線形時間でチェックできます。さらに、すべての変数がすべての連言にちょうど 1 回出現する完全な選言標準形に限定されている場合は、定数時間でチェックできます (各連言は 1 つの充足割り当てを表します)。しかし、一般的な SAT 問題を選言標準形に変換するには指数時間および空間が必要になる場合があります。例を得るには、上記の指数爆発例の「∧」と「∨」を連言標準形に置き換えます。
3-充足可能性問題の別のNP完全変種は、1/3 3-SAT（1-in-3-SAT、exactly-1 3-SATとも呼ばれる）です。節ごとに3つのリテラルを持つ連言標準形が与えられたとき、各節にちょうど1つのTRUEリテラル（したがってちょうど2つのFALSEリテラル）を持つような変数への真偽値割り当てが存在するかどうかを判定することが問題です。
別の変種として、すべて等しくない 3-充足可能性問題 ( NAE3SATとも呼ばれる) がある。節ごとに 3 つのリテラルを持つ連言標準形が与えられたとき、どの節においても 3 つのリテラルすべてが同じ真理値を持つような変数への割り当てが存在するかどうかを判定する問題である。シェーファーの二分法定理により、否定記号が許容されない場合でも、この問題は NP 完全である。[ 23 ]
もう1つの特殊なケースは、各節に（通常の）OR演算子ではなくXOR（つまり排他的論理和）が含まれる問題のクラスです。これはPに属します。なぜなら、XOR-SAT式はmod 2の線形方程式系と見なすことができ、ガウス消去法によって3次時間で解くことができるからです。[ 24 ]
上記の制約（CNF、2CNF、3CNF、Horn、XOR-SAT）は、検討対象の論理式を部分式の連言に限定します。各制約は、すべての部分式に対して特定の形式を規定します。たとえば、2CNFでは二項節のみが部分式になり得ます。
シェーファーの二分法定理は、これらの部分式を形成するために使用できるブール関数の任意の制限に対して、対応する充足可能性問題は P に属するか NP 完全であると述べている。2CNF、Horn、および XOR-SAT 式の充足可能性が P に属することは、この定理の特殊なケースである。[ 23 ]
以下の表は、SATの一般的なバリエーションをまとめたものです。
2003 年以降、非常に人気が高まっている拡張として、CNF 式に線形制約、配列、全異値制約、未解釈関数 [25] などを追加できる充足可能性法理論 (SMT)があります。このような拡張は通常 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に属するどの問題よりも厳密に難しいと広く信じられていますが、これはまだ証明されていません。
通常のSATでは、式を真にするような変数への代入が少なくとも1つ存在するかどうかを問う。そのような代入の数を扱う様々なバリエーションが存在する。
その他の一般化には、一階述語論理および二階述語論理の充足可能性、制約充足問題、0-1整数計画法などがある。
SAT は決定問題ですが、満足割り当てを見つける探索問題はSAT に帰着します。つまり、SAT のインスタンスが解けるかどうかを正しく答えるアルゴリズムは、満足割り当てを見つけるために使用できます。まず、与えられた式 Φ に対して質問します。答えが「いいえ」の場合、式は充足不可能です。そうでない場合は、部分的にインスタンス化された式 Φ { x 1 =TRUE}、つまり最初の変数x 1 をTRUE に置き換えてそれに応じて簡略化した Φ に対して質問します。答えが「はい」の場合はx 1 =TRUE、そうでない場合はx 1 =FALSE です。他の変数の値も同様の方法で後から見つけることができます。合計で、n +1 回のアルゴリズムの実行が必要です。ここでnは Φ の異なる変数の数です。
この性質は、計算複雑性理論におけるいくつかの定理で用いられている。
SAT問題はNP完全であるため、最悪ケースの計算量が指数関数的に増加するアルゴリズムしか知られていません。それにもかかわらず、2000年代にはSATの効率的でスケーラブルなアルゴリズムが開発され、数万の変数と数百万の制約（つまり節）を含む問題インスタンスを自動的に解決する能力の劇的な進歩に貢献しました。[ 3 ]電子設計自動化（EDA）におけるこのような問題の例としては、形式的等価性チェック、モデル検査、パイプライン化されたマイクロプロセッサの形式的検証、[ 25 ]自動テストパターン生成、FPGAのルーティング、[ 32 ]プランニングおよびスケジューリング問題などがあります。SATソルバーエンジンは、電子設計自動化ツールボックスの必須コンポーネントとも考えられています。
現代のSATソルバーで使用される主な手法には、Davis–Putnam–Logemann–Lovelandアルゴリズム（またはDPLL）、衝突駆動節学習（CDCL）、WalkSATなどの確率的局所探索アルゴリズムなどがあります。ほぼすべてのSATソルバーにはタイムアウトが含まれているため、解が見つからない場合でも妥当な時間内に終了します。SATソルバーによって、インスタンスの容易さや難しさが異なり、充足不能性の証明に優れているものもあれば、解の発見に優れているものもあります。最近では、深層学習技術を使用してインスタンスの充足可能性を学習する試みが行われています。[ 33 ]
SATソルバーは、SATソルビングコンテストで開発および比較されます。[ 34 ]現代のSATソルバーは、ソフトウェア検証、人工知能における制約解決、オペレーションズリサーチなどの分野にも大きな影響を与えています。
過去数十年間で、最悪実行時間の保証がますます向上した理論的アルゴリズムが提案されてきた。長さ（総リテラル数）の節セットに対するアルゴリズム[ 35 ] [ 36 ] 集合のアルゴリズム条項、[ 37 ] [ 38 ]および3-SAT のアルゴリズム変数。[ 39 ]ここで表記「「」は「多項式係数まで」を意味します。以前の実行時保証については、図に示されています。
数百万の制約と数十万の変数を持つ問題を処理できることが多い。。
（発行日時点）
