なぜ私たち全員がSATとこれらすべてのP-NPを必要とするのか（パート1）

SATは心を整えてくれるので、すでにとても良いです

ロモノソフ（ オリジナル ）

はじめに

ハブラーでは、すでに多くの記事がP対の問題に取り組んでいます。 NPおよびSATisfiability問題。 ただし、それらのほとんどは、最も重要な質問のいくつかに答えていません。 この問題が私たちにとって本当に重要なのはなぜですか？ 決定されたらどうなりますか？ これはすべてどこに当てはまりますか？ そして、それが何であるかについて少なくとも一般的な考えを持つ必要があるのはなぜですか？







ハブ[1、2、3、4、5、6、7]で最も注目に値する作品を詳細に分析すると、一方で、計算の複雑さの分野の知識を持つ人々は根本的に新しいことを学ぶことができないことに注意してください与えられた記事。 一方、これらの記事はまだ公開されていません。 見出しの図は、問題を明確に示しています。理解していない人、それから何もはっきりしていない人、すでにそれについて聞いたことがある人はそれを必要としません。



この記事には2つの目標があります。1つ目は、問題の一般的な考え方を示して質問に答えること、1つ目はこの問題について知っておくべき理由（1つ目）、2つ目は主題に興味のある人にとって興味深い「成長のため」の資料を提供することですトピックのさらなる研究に役立つ場合があります（第2部）。

記事の構造

読みやすく、操作しやすいように、記事の内容の概要を簡単に説明します。

• 公開資料
  
  
  1. SATが私たち全員にとって重要なのはなぜですか？ アプリケーション/興味深いNPタスクとSAT
  2. SATおよびNPの完全性の歴史
  3. SAT、NPおよびPの直感的な定義
  4. どうなったら... P！= NP、P = NP
  5. 2-SATは多項式：アルゴリズムと直感
  6. 考える課題
  
  
  
• 専門資料（次のシリーズを参照）
  
  
  1. 正式な定義。 NPおよびCoNPの可​​解性問題の非対称性
  2. 2 + p-SATは多項式ですか？
  3. 複雑さの変数数への依存
  4. P対 NP、どうすればいいですか？ どこに書く？
  5. 表現できない定理：ロマノフの記事[ 3 ]が拒否を期待する理由
  6. 現代のSATソルバーについて
  7. 何を読む？
  8. 考える課題
  
  
  

免責事項

この作品は一般的な教材であり、SATの問題に精通することのみを目的としています。 計算の複雑さとSATは私の研究の主な方向ではありませんが、関連する科学分野にあるため、疑わしい場合は常に指定された情報源を参照してください。

公開資料

SATが私たち全員にとって重要なのはなぜですか？ 用途

この質問に答えるには、まず、数学的問題が私たちの知識なしに日常生活にどのような影響を与えるのか、そしてこれらの問題がどのようにSATに関係するのかを理解する必要があります。



ここに私たちの周りで発生するタスクのリストがあり、それらがSATとどのように関係するかを述べています。

• まず、RSA暗号化アルゴリズムについて説明します 。これは、銀行取引の安全性を確保し、安全な接続を作成するために使用されます。 RSAアルゴリズムは、SATを使用して「ハッキング」できます。
• 多くの推奨システム（たとえば、Netflixの一部として）は、ブール行列分解アルゴリズムを使用してコンテンツを推奨します。 このような行列の最適な分解は、SATを使用して見つけることができます。
• プロセッサ間でタスクを最適に分散するタスクは、SATを使用して解決できます。 多数の計画タスクがSATに削減されます。たとえば、 オープンショップスケジューリングでは、タスク（ジョブ）が特定の段階（特定の作業者によって完了する）を通過する必要があり、すべてのタスクの合計処理時間を最小限に抑える必要があります。
• NASAは、SATに直接リンクされたモデル検査方法を使用して、 ソフトウェア仕様とハードウェアモデルを検証します 。
• 一般的なk-meansクラスタリング法（k-means法）は、SATを使用して解決できます。
• グラフに関連する興味深いタスクのほとんど（たとえば、ソーシャルネットワークでは、グラフはユーザー間の友情の関係です）は、誰もがそれぞれの友人である最大のコミュニティの検索です。グラフ上の最長パスや他の多くのタスクの検索は、SATを使用して解決できます。 モスクワ地方の生活のタスク（だけでなく）：ごみ収集車のスケジュールをまとめて、すべてのごみ収集ポイントを最短時間で1回巡回するようにします。 ロジスティクスの多数のタスクは、SATタスクに帰着します。
• ナップザックの問題でさえ、 SATを使用して解決できます。 タスクは、固定サイズのランドセルを持ち、最大の価値のあるオブジェクトを収集することです（すべてのオブジェクトのサイズを事前に知っている）。
• 多くのビデオゲームはSAT（およびマリオも！）を使用して解決できます。 数独パズルと注意、 掃海艇はSATを使用して解決できます。
• データベースでトランザクション履歴をシリアル化するタスクは、SATを使用して解決できます。

SATを使用して解決されたタスクの視覚化（ ここから取られたバートセルマンによる）

「解決できる」とは何を意味し、NPはそれと何をしなければなりませんか？

簡単に言えば、SAT問題の効果的な解決策があれば、これらすべての問題を効果的に解決できます。 効率が正確に意味するものは特定のタスクに依存しますが、ここではユーザーが作業時間を受け入れられると仮定します（学期に学校をスケジュールするために、コンピューティングに数日を費やすことができ、クラスタリング方法のために、インタラクティブに結果を取得したいと思います） 上記の問題の多くについては、逆もまた真であり、それらを効果的に解決できれば、SATを効率的に解決できます（これはNP完全性と呼ばれます-この定義は非公式ですが、一般的な理解には十分です）。



これらの問題はすべてNPクラスにあります-後でクラスを詳細に説明しますが、SAT問題の効果的な解決策がわかっている場合は、NPクラスの問題を効果的に解決できることに注意してください。 言い換えれば、SATはクラスの代表的なタスクであり、そのクラスで「最も困難」であり、NPの他のすべての問題を解決することができます。

SATおよびNPの完全性の歴史

NP完全性

計算の複雑性の理論は、計算に必要な時間とメモリの量に応じて言語と関数が異なるクラスに割り当てられ、計算可能性の理論 （すなわち、ゲーデル、教会、チューリングによる30年代の仕事 ）から生まれました。 ）関数の最初のそのような分類の1つを提案しました（オリジナルの作品： こことここ ）。



NP完全性の概念は、ソビエト連邦とアメリカで1960年代と1970年代に独立して発展しました（エドモンズ、レビン、ヤブロンスキーなど）。 1971年、スティーブンクックはP対の仮説を策定しました。 NP。 SATはクラスNPの「普遍的な問題」であり、このクラスの問題（NP完全性）を解決できるという定理は、Leonid Levin（1973）とStephen Cookによって独立して証明され、Levin-Cook定理と呼ばれます。 1982年、クックはこの作品に対してチューリング賞を受賞します。



1972年に、KarpはSATがNPの唯一の興味深いタスクから遠く、膨大な数のタスクがNPにあり、SATと同等であることを示すリストである組み合わせ問題間の還元性を発表しました。 1985年、カープはこの作品に対してチューリング賞を受賞します。



1974年、FaginはNPが古典論理と密接に関連していること、つまりNPが2次の実存論理構造（ Faginの定理 ）と同等であることを示します。



1975年に、ベイカー、ジル、およびソロヴェイは、問題Pの解決不可能性に関する最初の基本的なメタ結果を得ました。 正規化されたメソッドを使用したNP これは、メソッドのクラス全体がP対対等の問題に答えることができないことを示す最初の結果です。 NP（これについては、 こちらで説明しています ）。



1979年、GaryとJohnsonは「 コンピューティングマシンと困難な問題 」を作成しました。これは、NP完全性とタスクの詳細なカタログに関する最も包括的な情報源の1つです。 いくつかの理論的結果は現在時代遅れであると考えられているという事実にもかかわらず、これは計算の複雑さの分野で最も基本的な作品の一つです。



公式言語、計算の複雑さの理論、および計算の理論間の関係の視覚化（ ここから ）：

SATソルバーの非常に短い歴史

1960年代、デイビスとプットマンは、SATを解くために、古典的な演ductive法（簡単に言えば、定理を証明する方法）を適用し始めました（ 元の作品 ）。



1962年、Loveland、Logeman、Putnam、Davisは、決定論的計算（単位伝搬）の戻り値と分布を使用した検索に基づくDPLLアルゴリズムを提案しました。 簡単に言えば、アルゴリズムはある変数の値が真理に等しいと仮定し、そのような解の決定論的結果をすべて計算し、解が見つかるまで繰り返しました。 このアルゴリズムは、何十年もの間、多くのSATソルバーの基盤として機能してきました。



1992年、セルマン、レベスク、およびミッチェルは、GSAT記事でローカル検索方法を提案しました。 GSAT-ローカルの情報のみに基づいて変数の値を決定するため、Greedy SATを意味します。 アルゴリズムは、変数値の任意の割り当てから始まり、実行された文で最大の増加を与えた場合、変数の値を変更しました。 その後、さまざまなバリエーションのローカル検索方法がほとんどのSATソルバーに統合されました-1999年、Hegler Husは博士論文で確率的ローカル検索とその応用に関する広範な研究を行っています（作業はこちらで入手可能です ）。



1996年、Marques-SilvaとSakalahは、DPLLと同様に、変数の値を決定し、決定論的計算を実行するConflict-Driven-Clause-Learning（ CDCL ）アルゴリズムを提案しました;一方、アニメーションのグラフを保存し、いくつかを記憶しますソリューションにつながらず、「無駄な」ソリューションを効果的に回避し、以前に確立された競合を含むソリューションのスペースを効果的に遮断できる組み合わせ。



2001年以来、ローカリティベースの検索SATソルバーが登場し始め、 BerkMin （Berkley-Minsk）などのローカル情報に基づいて、完全検索のための部分空間を効果的に選択しています。

SAT、NPおよびPの直感的な定義

土

命題論理とは何かを定義することから始めます 。それは変数の集合{x、y、z、...}とコネクタの集合{and、or、-（not）、→}です。 各変数は「false」または「true」のいずれかです。 コネクタは標準として定義されています：

• xとyは、以下の場合にのみ（簡潔にするために、IFFを記述します-xがtrueで、yがtrueの場合のみ）、古典的な「AND」
• 変数x \ yの少なくとも1つが真である場合、xまたはyは真、古典的な「OR」
• -x true、x false、古典的な否定
• x→yがfalseの場合、xがtrueで、yがfalseの場合、例を考えます
  
  「雨が降っていたら、草は濡れている」
  
  雨が降っていて（x true）、草がまだ乾いている（y false）場合にのみ、ステートメントはfalseです。

フォーミュラFは、構文的に正しい変数とコネクタのセットです。つまり、→、および、または変数または他のフォーミュラを接続します。 例、F =（x→（yまたはz））および（z→-x）。



彼らは、その変数に値「true」\「false」を割り当てることができる場合（英語I解釈からそのような関数Iを呼び出す）、式Fは充足可能（SAT）であると言います。 簡潔にするために、 I （F）= "true"と記述します。



命題式Fは、CNF（連言標準形）の形に還元できます。つまり、

F '= c ₁およびc ₂および... c _n

ここで、c _iは（xまたはyまたはz）であり、x、y、zは変数またはその否定です。



例F =（xまたは-yまたは-z）および（-xまたは-yまたはh）および（zまたはh）。



この変換の詳細については、 ここに記述します （各文に3つ以下の変数を含めるには、追加の変数を導入する必要がありますが、これらは技術的な詳細にすぎません）。



この形式では、式が上記の形式の場合、タスクは3-SATと呼ばれ、各文c _iには3つ以下の変数またはその否定が含まれるという事実を強調します。



3-SAT問題のステートメントは次のとおりです。

指定： 3-CNFとしての命題式F

Find ::関数I 、値 "true" \ "false"をすべての変数に割り当て、 I （F）= "true"など

クラスP

P it PTIME-多項式時間で解くことができるタスク。これは、このクラスのアルゴリズムステップの数が入力データから特定の多項式以下になることを意味します。 PTIMEのさまざまなアルゴリズムと複雑さの分析に関する詳細は、Habr [9、10、11、12、13]ですでに記述されています。



説明のために、以下に簡単な例を示します。バブルソートアルゴリズム（wikiからの擬似コード ）

procedure bubbleSort( A : list of sortable items ) n = length(A) repeat swapped = false for i = 1 to n-1 inclusive do if A[i-1] > A[i] then swap(A[i-1], A[i]) swapped = true end if end for n = n - 1 until not swapped end procedure
      
      

        
        
        
      

    
        
        
        
      
      

        
        
        
      

    
     

入力パラメーターは、ソートする数値の配列です。 配列の長さの増加に応じた時間の増加に興味があります。 TIME時間のnへの依存。 繰り返しループの各反復は、3 * n以下のステップを実行し、配列の少なくとも1つの要素を目的の位置に設定することに注意してください。 これは、繰り返しループがn回以下実行されることを意味します。 これは、操作の数（別名TIME）が配列の長さ（および「n =長さ（A）」からの線形項）の特定の2乗として増加することを意味します。



時間（n）= a * n ² + b * n + C



言い換えると、アルゴリズムの実行時間はnの多項式によって制限されます。この場合、アルゴリズムの実行時間は要素数の2乗よりも速く増加せず、 Big-Oレコードを使用して書き込みます。

クラスNP

NPは非決定的多項式時間を表します。 非常に多くの場合、誤って非多項式時間と呼ばれ、これについてジョークが生まれました。

アルゴリズムを多項式と非多項式に分割することは、宇宙をバナナと非バナナに分割することとほぼ同じです。

この記事では、NPの正式な定義には興味がありません（これは専門資料に含まれます）が、クラスNPの直感的な表現を検討します。 NPの本質と内部メカニズムは、いわゆる推測とチェックの方法に従います。 つまり ソリューションの検索スペースは指数関数的（ブルートフォースを排除するのに十分な大きさ）であり、ソリューションのチェックは簡単なタスクです。 NPは、多数のオプションの中から解決策（「推測」-推測部分）を見つけ、その正しさを確認する（部分を確認する）必要がある問題のクラスと見なすことができます。



SATの観点から、解空間はすべての種類の変数値のセットです。式にk個の異なる変数がある場合、式の2 ^k個の 「解釈」、つまり サーチスペースIは指数関数的に。 ただし、 Iを「推測」した場合、多項式時間で式の真理を検証できます。

P！= NPの場合はどうなりますか

何もありません、誰かだけが百万ドルを受け取ります。

P = NPの場合はどうなりますか

良い点と悪い点の2つのニュースがあります。



良いもの。 多数の最適化問題を迅速に解決し、タスクをグラフ化し、スケジュールを組み、パズルを組み立て、さまざまなデータベースプロパティをチェックし、NASA仕様のパフォーマンスを効果的にテストします。



悪いもの。 現代の暗号化はすべて崩壊しており、それによって銀行システムが打撃を受けています。 人々はマリオのボットを書き始めます。

Pの2-SAT

SATの興味深いバリエーションを考えてみましょう。各句は2つの変数に制限されています。 以下、著者は、素材の認識を容易にするためにすべてを大幅に簡素化します。



与えられた ：Fはc ₁およびc ₂およびc ₃ ...およびc _nの形式の式であり、

c _iの形式は（xまたはy）で、x、yは変数またはその否定です。つまり、xは変数vまたは-vです。

Find ：関数I 、値 "true" \ "false"をすべての変数に割り当て、 I （F）= "true"となる

ステートメント ：関数Iが存在する場合はP（F）= I 、そうでない場合はP（F）= {}となるような多項式アルゴリズムPがあります。



（*）関数Iが存在し、Pが関数Iを返す場合、関数Iは一意ではありません（アルゴリズムと複雑性に関する書籍では、すべてが形式言語で記述されますが、これらの詳細は、2-SATが多項式である理由の一般的な考えを理解するために不可欠ではありません）

証拠のスケッチ：

最初に、次の等式を使用して元の式を変換します。



真理値表を使用して確認できます。 このルールの背後にある直感は次のとおりです。

「雨が降っていた場合、草は濡れています」（x→y、x-雨が降っていた、y-草は濡れています）

これは、草が乾いている（濡れていない：yが偽）場合、雨が降らない（xが偽）ことを意味します。

草が濡れている場合、直感的なレベルで、雨が降った（xはある意味で、xはyが真である理由を「説明」する）か、雨がなかった（xは偽である）か、別の理由があることを意味するtrue（z-隣人が草を注いだため、草が濡れています）。



（*）を使用してFをc ' ₁およびc' ₂ ...およびc ' _nの形式に変換します。c' _iの形式は（x→y）です。x、yは変数またはその否定です。 その結果、Fは含意グラフです。 以下の同様のグラフの例：

s ₁ =雨が降っていた場合、草は濡れています。

c ₂ =隣人が芝生に水をやった場合、草は濡れています。

c ₃ =草が濡れている場合、雑草はよく成長します。





含意のグラフで特定の頂点v（雨が降っていたなど）から離れた場合、ピーク-v（雨が降っていなかった）に到達することができない場合、含意のシステムは一貫していることがわかります。 直感は次のとおりです。たとえば雨が降っていたなどの仮定を立てると、草が濡れていて雑草が成長しているとすぐに結論し（隣人が芝生に水をまくかどうかを選択するだけです）、矛盾がない場合は 、特に機能Iの一部があります雨が降っていると判断したので、「草が濡れている」と「雑草がよく育つ」という意味がわかりました。「隣人が芝生に水をやった」という意味について決定するだけです。



そのような決定を何回行う必要がありますか？ 文の数はn以下です。 1つの決定を下す場合、いくつの操作を行う必要がありますか？ ソリューションごとに、グラフの端を1回だけ移動する必要があります。つまり、1つのソリューションでn回以下の操作を実行する必要があります。 これは、 Iを見つけるためにn ²回以下の操作を実行する必要がないことを意味します。 ■

「考える」タスク

このタスクでは、追加の研究と文献の検索が必要になる場合があります。

簡単なSATソリューション

状態

各命題式F = c ₁およびc ₂およびc ₃およびc _nは、選言標準形（DNF）、つまり、F '= c' ₁またはc ' ₂ ...またはc' _kの形式にすることができます。ここで、c ' _iの形式は（xおよびyおよびz）です。x、y、zは変数またはその否定です。 たとえば、De Morganルールの一貫した適用（リンク）と括弧の開示を使用します。

F 'には、関数Iの単純な検索アルゴリズムが存在します。c' _iの少なくとも1つが真であることが必要です。 問題を解決する簡単な擬似コードを書きましょう。

 #Input: F — propositional formula in disjunctive normal form (DNF) #Output: {SAT, UNSAT} for each c in F do if c is SAT: return SAT return UNSAT
      
      

        
        
        
      

    
        
        
        
      
      

        
        
        
      

    
     

各文（節）c _{iに対して} 、検索アルゴリズムIも重要です。文c _iに変数vとその否定が同時に含まれていない場合、c _iは充足可能（SAT）です。

合計 ：充足可能性の式をチェックするための簡単なアルゴリズムを取得します

見つける ：間違いはどこですか？

参照とソース

序文の写真は

計算の複雑さと人類の原理Scott Aaronson



スライド

SATがスケールする理由：相転移現象と複雑さへの裏口スライドは、バートセルマンコーネル大学の好意によるものです。

スライドは記事に基づいています：

2 + P-SAT：典型的なケースの複雑さと相転移の性質との関係 （Monasson、Remi; Zecchina、Riccardo; Kirkpatrick、Scott; Selman、Bart;およびTroyansky、Lidror）

他の記事はこちらにあります。



NPの歴史について詳しくはこちらをご覧ください。

Michael SipserによるP対NP質問の歴史と状況

Elvira MayordomoによるP対NP



SAT-solver'ahの詳細：

SAT Solvers：凝縮された歴史

モダンSATソルバーの理解は、おそらく世界で最も有名なSATソルバー開発者であるArmin Biereの著者です。 現在、コンピュータープログラミングのアート：第4巻、プレファシクル6A充足可能性を書いているドナルドクヌースは、多くの問題について彼と相談していると言います。

SATソルバーの新しい時代に向けて



Habraの素材：

[1] NP完全問題の単純なアルゴリズムを信じない理由

[2] PとNPについてもう少し

[3] 科学者への公開書簡と、NP完全3-VYP問題に対するロマノフアルゴリズムの参照実装

[4] 公開された証明P≠NP？

[5] P = NP？ 理論計算機科学の最も重要な未解決の問題。

[6] アカデミック大学の理論的コンピューターサイエンス

[7] 2012年のアルゴリズム分野のトップ10の結果

[8] スーパーマリオはNP完全であることが証明されました。

[9] アルゴリズムの複雑さ分析の概要（パート1）

[10] アルゴリズムの複雑さ分析の概要（パート2）

[11] アルゴリズムの複雑さ分析の概要（パート3）

[12] アルゴリズムの複雑さの分析の概要（パート4）

[13] アルゴリズムの複雑さを知る