なぜSATとこれらすべてのP-NPが必要なのか（パート2）

前のパートでは 、SATとP-NPに関連する一般に公開されている質問が強調されました：問題の歴史、クラスとタスクの直感的な定義、SATの主な用途、P？= NPを解く場合の主な結果自習トピックについて）。

この記事では、問題の技術的な側面を検討するとともに、前の記事の資料を形式化し、詳細に提示します。



記事からの画像ブール充足可能性：理論的困難から実用的な成功まで （ACMのコミュニケーション）

記事の構造

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

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

どうなるか...

前の作業では、最も単純なソリューションシナリオのみが考慮され、多くの興味深い発言を引き起こしました（著者は、この問題に関する興味深い有用なリンクに感謝を表しています）。 この記事では、可能性のあるすべてのオプションとその結果を考慮し、コメントと以前の作業に関するコメントを考慮します。

芸術的な観点から、さまざまなソリューションに関する議論を説明することは非常に興味深いです。

P = NP

状況の開発にはいくつかのオプションがあります。

• 建設的な解決策
  
  1. 多項式には低次の係数と中程度の係数があります。詳細は、前の記事のP = NPの部分で説明されています 。 要するに：すべての暗号が崩壊する
  2. 多項式は次数が高い-実際の観点からは何も変わらないP！= NP
  
  
• 非構造的なソリューション
  
  1. この証明からアルゴリズムを取得できない場合、実用的な観点からP！= NP
  2. 可能であれば、質問P？= NPは時間の質問に変換され、証明からアルゴリズムが作成されます
  
  

P！= NP

前のケースと同様に、解決策は建設的でも非建設的でもかまいません。 建設的なケースを考慮してください（前のケースと同様の構造的に非建設的なケース）

• ソリューションの複雑さは常に指数関数的です。変更はありません。現在の世界の状況は完全に保持され、アルゴリズムは変更されません。
• 解の複雑さは常に指数関数的ではありませんが（ この記事を参照）、十分な数のケースでは多項式です。 この場合、何が起こるかを明確に予測することはほとんど不可能であり、推測することしかできません。因子分解の問題が「簡単なタスクのクラス」に該当する場合、実用的な観点から、これはRSAを攻撃するためのP = NPと同等になります
• 解の複雑さは中程度または低い（たとえば、n ^log（n） ）。この場合、実用的な観点から、これはP = NPと同等になります。

P対 NPは公理学ZFCでは解けない

詳細と興味深い点については 、「 P対NPは形式的に独立していますか？」 スコット・アーロンソン著（記事を理解するには十分な数学的文化が必要です;推定読書時間〜午後1/2）。 以下は、記事の内容の簡単な概要です。

以下の記事の主なメッセージは、仮説P = NPとP！= NPの両方が集合論と一致していることが判明する可能性があることです。 これは、P対 NPは、選択理論が集合論の他の公理から独立しているなど、集合論の公理から独立しています。 実用的な観点から、これはP！= NPを意味します。

正式な定義。 NPの可解性問題の非対称性。 CoNPクラス。

複雑性理論では、「解決可能性の問題」の形式で問題を定式化するのが慣例です。 答えが「はい」または「いいえ」のみであるタスク。 クラスPおよびNPは、言語およびチューリングマシンに関して正式に定義されています。

ここで、L _MはマシンMが受け取る言語です。
多項式のステップ数に対して言語L（p）を取る決定論的チューリングマシンがある場合、特定の問題pはクラスPに属します。

NPクラスでは、すべてが少し面白くなります。これは、解の正しさを多項式時間でチェックできる問題のクラスです。 正式には、言語LがNPに属するのは、行xがtrueであるような決定論的チューリングマシンMが存在する場合のみです。

ここで| y | -は多項式で区切られ、Mは多項式のステップ数を実行します。 「y」-証明書には特別な用語があります。 実際、定義は次のようになります。多項式解が存在する場合、問題はNPに属し、その正確性は多項式時間で検証できます。 言語がNPに属していない場合、この定義は質問に関して非対称であることに注意してください。 問題は、NPが別のクラスに属しているかどうかではありません。

Co-NPのクラスは何ですか？ Co-NP-NPを補完します。直感的に、これはタスクがNPのタスクの否定であるクラスです。 SATが、式がtrueである変数に対してこの割り当てがtrue / falseであるかどうかを尋ねる場合、UNSATは式がすべての割り当てに対して間違っているかどうかを尋ねます つまり つまり、証明書が存在しないのは本当ですか。

または、次のように定式化できます。
NPは、簡単な所属証明書を持つ言語のコレクションです
Co-NPは、所属を拒否する簡潔な証明書を持つ言語のコレクションです（=肯定証明書は存在しません）

NP！= Co-NPの場合、NP完全問題とCo-NP完全問題のセットは交差しません（ マハニーの定理の帰結）。

言語、チューリングマシン、および複雑度クラスの定義に関する詳細については、M。Gary、D。Johnson：コンピューターと解決が難しい問題（たとえば、 こちら ）を参照してください。

現代の概念によれば、NP、Co-NP、およびPの関係は次のとおりです。

（ ここから撮影した写真）
ほとんどはオプション（d）に傾いていますが、他のオプションがありそうだと考える人もいます。たとえば、The Art of Programming 4、6A：Satisfibility -page 1、footnote（*）： "...この本の著者は、しかし、多項式アルゴリズム（SAT用-著者注）は実際に存在しますが、まだ知られていないだけです... "

2 + p-SATは多項式ですか？

前の記事で、2-SATは多項式であることが示されました。 各句を2つの変数に制限すると、問題を効率的に解決できます。 この問題の自然な一般化について考えてみましょう。3つの変数を含む文の一部しかないとしたらどうでしょうか。

pを文の総数に対する3つの変数を持つ文の数とします。 その場合、2 + p SAT問題は、3変数の文の数が事前に固定されている3-SAT問題です。 p、それぞれ（1-p）文には1つまたは2つの変数があります。

理論的な観点から、たとえpがオッシロコッシヌムの野bなカモの濃度であるとしても 。 正の数であれば、NP問題は完全ですが、実際には完全に異なって見えます。
X軸に沿って式の変数の総数を、Y軸に沿ってこの式の解の「計算コスト」とします（通常、これは最先端のSATソルバーアルゴリズムの呼び出し数と解の数です。DPLLとCDCLの簡単な説明を参照してください。前の記事）。

（グラフは、 2 + P-SAT：典型的なケースの複雑さと相転移の性質との関係から取られています）。

p <= 0.4の場合、問題は多項式であり、さらには入力データが線形です。 p> 0.4の場合、従来の3-SATと同様の動作が観察されます。 この効果を説明するために、古典的なDPLLアルゴリズム（Armin Biereのスライドから取得）を検討してください。


簡単な例を見てみましょう。

アルゴリズムにx ₂ = 1を選択させます

次に、式が単純化され、1つの変数を持つ2つの文があります-つまり、ブール制約伝搬は、そのうちの1つ、たとえばx ₃を選択し、利用可能な値のみを割り当てます

x ₃ = 1を割り当てた後、BCPは再び単一の変数x ₁を持つ文を見つけ、x ₁ = 1を割り当てます

したがって、単一のSATソルバーソリューションの後、ブール制約伝播により、式全体のソリューションを見つけることができます。 これは主に、2つの変数を持つ文の変数の決定が実際に別の変数の値を一意に決定するために発生します。これにより、割り当てのカスケード全体が発生し、BCPが式を効果的に削減します。 そのようなカスケードが式の十分な数の変数をカバーする場合、解は線形です。

複雑さの変数数への依存

別の興味深い依存関係は、いわゆる節変数比です。つまり、文の数と変数の数の比率です。 直観的には、より多くの文、より多くの制限、より多くの可能性が高い式-あまりにも多くの制限。 このような問題は、制約が厳しすぎると言われています。 提案が少ないが変数が多い場合、自由度が多く、制限が少ないことを意味します。 これにより、解決策を簡単に見つけることができ、式が実行可能である可能性があります。 彼らは彼女について、彼女が過小拘束されていると言います。

すでに2 + p SATを検討しているため、この依存関係のパラメーターpを考慮することも興味深いでしょう。問題の「線形性」の程度、pが大きいほど、ブール制約の伝播が効果的でなく、解決策を見つけるのが難しくなるためです。

2 + p SATのSAT / UNSAT移行

自然からのグラフ：Remi Monasson、Riccardo Zecchina、Scott Kirkpatrick、Bart Selman、Lidlor Troyanskykによる特徴的な「相転移」から計算の複雑さを決定する

実際、このグラフは私たちが考えている以上のものを提供します。「複雑な」ランダムな数式を生成することができます。 数式がSATとUNSATの中間にある場合、そのモデルを見つけることは困難であり、実行不可能性の証明を生成することは困難であることを意味します。
DPLL呼び出しの数のSAT / UNSAT移行の位置への依存性は次のとおりです。

Satis能力問題のハードインスタンスの検索： S. Cook、 D。Mitchellによる調査の記事のグラフ

現代のSATソルバーについて

基本原理、アルゴリズム、およびヒューリスティックの説明でも100ページ以上かかるため、最も一般的で主要なSATアルゴリズムの1つであるCDCL-Conflict Driven Clause Learningの説明に限定します。 名前が示すように、このアルゴリズムの主な特徴の1つは、解決につながらない決定を記憶する機能です。つまり、アルゴリズムはそれらを文の形で記憶します。 x ₁ = 1、x ₂ = 2、x ₃ = 1を決定し、これが競合につながる場合、CDCLは競合の組み合わせの否定を記憶します。

De Morganのルールに従って、CNFの形式を与えます

それを式に追加します


したがって、CDCLの2つの重要なコンポーネント：決定グラフと含意グラフ、および競合する組み合わせでの動作。 原則として、決定を下した後、アルゴリズムはすべての可能な決定論的計算を実行し、競合します。 含意グラフと決定スタックは、どの段階でどの組み合わせと解決策が競合を引き起こしたかを示し、競合提案の生成に基づいています-したがって、競合駆動句学習という名前は、アルゴリズムが競合の組み合わせを効果的に見つけ、それらを学習し、競合の組み合わせを考慮して決定を下します。

CDCLアルゴリズムの例を詳しく見てみましょう。

酒井正弘より

CDCLの詳細は、次の著作物に記載されています。
Satis能力のハンドブック： 第4章ジョアンマルケスシルバ、イネスリンチ、シャラドマリクによる競合駆動型節学習SATソルバー
CDCLによるSAT / SMTサマースクール2013のスライド： CDCL SATソルバーとSATベースの問題解決
アルゴリズムおよび内部構造の詳細かつ十分な技術的説明： 実用的なSATソルビング：Con ict-driven SATソルバー

P対 NP、どうすればいいですか？ どこに書く？

まず、解決策の常識への適合に関する多くの質問に答える必要があります。

1. 問題を解決する他の試みが失敗した理由を説明できますが、私たちの仕事はそうではありません
2. この作業がどのように非効率性の定理、すなわち これらの定理（例：Baker-Gill-Solovayの定理）がこの仕事に当てはまらないことを明確に示す
3. P = NPで、証明が建設的である場合、プロトタイプが必要です。そうでなければ、誰も解決策を信じません。
4. 仕事は自給自足であり、専門家が理解するために利用可能です。 すべての必要な定義、拡張された形式の証拠が含まれています（ヒエログリフとアクセスできない言語で3ページに書かれたミレニアムタスクにより、検査官はバスケットで彼女を毒する疑いと欲求を引き起こします）
5. 著者は複雑性理論をよく理解しています。つまり、彼らはすべての主要な作品や作品に精通しており、近年この科学分野で何が起こったかを知っています。

これらすべての条件が満たされていると仮定し、次に2番目に、認識された決定と見なされるものは何ですか？ ジャーナル「Automation and Mechanics」に掲載されていますか？ P対NPの問題に適した会議がいくつかあります。
STOC、コンピューティング理論に関する年次ACMシンポジウム
TAGL、アルゴリズムに関するACMトランザクション
FOCS、コンピューター科学の基礎に関するIEEE年次シンポジウム

彼ら（これらの会議のいずれか）があなたの決定を認めれば、あなたは何百万人も安全に数えることができます-その瞬間まで、その決定は多くの間違った決定P vs NP。

P vs.のチェックの問題に関する興味深いロードマップ（より正確には、質問のインタラクティブなリストですら）。 ここで NPソリューションを紹介します 。

ロマノフの記事が拒否を期待する理由

あなたが短い答えをした場合、その記事は「常識」のリストからの質問のいずれにも答えないので：

1. この記事には「関連する作業」はまったくありません。40年間、複雑性理論の進歩はなかったようです（著者は3回しか言及していません）。たとえば、 NP完全性コラム：近似の多くの制限を見ることができますデイビッド・S・ジョンソンは 、この事例について簡単に簡潔に説明し、関連するすべての作業、TAGLの通常の高品質の作業について述べています
2. この作業では、代数表現（変数からのタブレット、これらのタブレットのグラフ、およびプロパティをチェックするためのほとんどの連言クエリ）が認められます-決定可能性P vs. 代数的手法を使用したNP。 ところで、レビュアーがあなたがそのような結果を意図的に無視すると疑う場合、これは提出された作品に対して解釈されます
3. プロトタイプが漸近線で指数関数的に実行されないのはどこですか？
4. アルゴリズムの擬似コードはどこにありますか？ 本格的な実用例はどこにありますか：入力はよく知られた複雑な例ですが、アルゴリズムと出力データの操作は段階的に行われていますか？ 正式化はどこですか？ 17ページの記事では、2つの形式の式（a => b）と精神の非公式フレーズ：「Fの行を3つの空でない列の同じ数でグループ化する」
5. 例えば、レビンクックの作品への重要な参照はありません。

さらに、作業が修正されたとしても、誰にも公開書簡を書くことはまだ意味をなさないと仮定します。現代科学はそのように機能しません。正しい決定を国民に納得させるのはあなたの仕事です。 これは専門家の意見のプリズムを通してのみ行うことができます。上記の会議を参照してください。

何を読む？

通常、SAT / SMTサマースクールではすべてがうまく説明されています。
教材2013
教材2012

すぐにSATについての新鮮なKnutがあります-ドラフトが利用可能です： The Art of Programming 4、6A：Satisfibility

以前の投稿には多数のリンクがありますが、 なぜ私たち全員がSATとこれらすべてのP-NP（パート1）を必要とするのですか？
主なものは次のとおりです。
SAT-solver'ahについて：
SAT Solvers：凝縮された歴史
モダンSATソルバーの理解は、おそらく世界で最も有名なSATソルバー開発者であるArmin Biereの著者です。 現在、コンピュータープログラミングのアート：第4巻、プレファシクル6A充足可能性を書いているドナルドクヌースは、多くの問題について彼と相談していると言います。
SATソルバーの新しい時代に向けて

NPの歴史について：
Michael SipserによるP対NP質問の歴史と状況
Elvira MayordomoによるP対NP

複雑さの理論に関する最も有名で尊敬される作品の一つ：
Gary M.、Johnson D.-計算機と困難な問題[1982]

考える課題

SAT、リレーショナル代数、ブレークポイントの問題の矛盾。
次の3つのステートメントが提供されます。
1. 1次論理と関係代数の「計算の複雑さ」は同じです。つまり、ある形式でタスクが複雑Xを持っている場合、同じ複雑さで別の形式で表現されます（ link ）。
2.関係代数は推移的閉包を表現できない-クラスPのタスク（ 関係代数：推移的閉包 ）
3. 1次論理のSATは停止問題に相当し、アルゴリズム的に解決できません（ link ）。
質問：これはどのようにできますか？