論文の概要: SAT Requires Exhaustive Search

• arxiv url: http://arxiv.org/abs/2302.09512v9
• Date: Mon, 28 Oct 2024 04:18:27 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-10-29 16:00:45.275726
• Title: SAT Requires Exhaustive Search
• Title（参考訳）: SAT が Exhaustive Search を要求
• Authors: Ke Xu, Guangyan Zhou,
• Abstract要約: 本稿では,計算硬度を証明することは数学では難しくないことを示す。 非常に難しい例では、徹底的な検索が唯一の選択肢かもしれない。 これにより、SAT(長い節を持つ)と3-SATの分離は、3-SATと2-SATの分離よりもずっと簡単になります。
• 参考スコア（独自算出の注目度）: 4.959974472811339
• License:
• Abstract: In this paper, by constructing extremely hard examples of CSP (with large domains) and SAT (with long clauses), we prove that such examples cannot be solved without exhaustive search, which is stronger than P $\neq$ NP. This constructive approach for proving impossibility results is very different (and missing) from those currently used in computational complexity theory, but is similar to that used by Kurt G\"{o}del in proving his famous logical impossibility results. Just as shown by G\"{o}del's results that proving formal unprovability is feasible in mathematics, the results of this paper show that proving computational hardness is not hard in mathematics. Specifically, proving lower bounds for many problems, such as 3-SAT, can be challenging because these problems have various effective strategies available for avoiding exhaustive search. However, in cases of extremely hard examples, exhaustive search may be the only viable option, and proving its necessity becomes more straightforward. Consequently, it makes the separation between SAT (with long clauses) and 3-SAT much easier than that between 3-SAT and 2-SAT. Finally, the main results of this paper demonstrate that the fundamental difference between the syntax and the semantics revealed by G\"{o}del's results also exists in CSP and SAT.
• Abstract（参考訳）: 本稿では, CSP (大域領域) と SAT (長節) の非常に難しい例を構築することにより, P $\neq$ NP よりも強い網羅的探索なしではそのような例は解決できないことを証明した。 計算複雑性理論で現在使われているものとは全く異なる(そして欠落している)が、クルト・G・"{o}del が彼の有名な論理的不合理な結果を証明する際に用いたものと似ている。 G\"{o}del's results that proving formal unprovability is beactible in mathematics, the results of this paper show that proving compute hardness is hard in mathematics。 具体的には, 3SAT などの多くの問題に対する下位境界の証明は, 徹底的な探索を避けるために, 様々な効果的な方法が考えられるため, 困難である。 しかし、非常に難しい例では、徹底的な探索が唯一の選択肢となり、その必要性を証明することはより簡単になる。 これにより、SAT(長い節を持つ)と3-SATの分離は、3-SATと2-SATの分離よりもずっと簡単になる。 最後に、G\"{o}del の結果から明らかになった構文と意味学の基本的な違いが CSP と SAT にも存在していることを示す。

関連論文リスト

• MathGAP: Out-of-Distribution Evaluation on Problems with Arbitrarily Complex Proofs [80.96119560172224]
  大規模言語モデル(LLM)は、高い精度で算術語問題を解くことができるが、訓練された言語よりも複雑な問題にどのように一般化するかは、ほとんど分かっていない。 本研究では、任意に複雑な算術証明問題に対する LLM の評価フレームワーク、MathGAP を提案する。
  論文  参考訳（メタデータ） (2024-10-17T12:48:14Z)
• Artifical intelligence and inherent mathematical difficulty [0.0]
  まず、計算可能性と複雑性理論による制限的な結果が証明発見が本質的に難しい問題であることを示す従来の議論の更新版を提示する。 次に、人工知能にインスパイアされた最近のいくつかの応用が、数学的な証明の性質に関する新しい疑問を実際に提起する方法について説明する。
  論文  参考訳（メタデータ） (2024-08-01T20:08:31Z)
• Decomposing Hard SAT Instances with Metaheuristic Optimization [52.03315747221343]
  分解硬度(d硬度)の概念を導入する。 d-硬度が$C$ w.r.tの硬度の推定値を示すことを示す。
  論文  参考訳（メタデータ） (2023-12-16T12:44:36Z)
• Explaining SAT Solving Using Causal Reasoning [30.469229388827443]
  本稿では、因果推論を用いて、現代のSATソルバの機能に関する洞察を得るCausalSATを紹介する。 われわれはCausalSATを用いて,これまで「親指のルール」や経験的発見と考えられていた仮説を定量的に検証した。
  論文  参考訳（メタデータ） (2023-06-09T22:53:16Z)
• A hybrid Quantum proposal to deal with 3-SAT problem [75.38606213726906]
  本稿では,3SAT問題を解くためのハイブリッド量子コンピューティング戦略について述べる。 この近似の性能は、量子コンピューティングの観点から3-SATを扱う際に、一連の代表的なシナリオで検証されている。
  論文  参考訳（メタデータ） (2023-06-07T12:19:22Z)
• Amplitude amplification-inspired QAOA: Improving the success probability for solving 3SAT [55.78588835407174]
  振幅増幅アルゴリズムは、可変代入を満たすために非構造化探索に適用することができる。 Quantum Approximate Optimization Algorithm (QAOA)は、ノイズのある中間量子デバイスのための3SATを解くための有望な候補である。 振幅増幅によるQAOAの変種を導入し、3SATの成功確率を改善する。
  論文  参考訳（メタデータ） (2023-03-02T11:52:39Z)
• Estimating the hardness of SAT encodings for Logical Equivalence Checking of Boolean circuits [58.83758257568434]
  LEC インスタンスの SAT 符号化の硬さは SAT パーティショニングでは textitw.r. と推定できることを示す。 そこで本研究では, SAT符号化の難易度を精度良く推定できるパーティショニング法を提案する。
  論文  参考訳（メタデータ） (2022-10-04T09:19:13Z)
• Machine Learning Methods in Solving the Boolean Satisfiability Problem [72.21206588430645]
  本論文は, Boolean satisfiability problem (SAT) を機械学習技術で解くことに関する最近の文献をレビューする。 ML-SATソルバを手作り特徴を持つナイーブ分類器からNeuroSATのような新たなエンド・ツー・エンドSATソルバまで,進化するML-SATソルバについて検討する。
  論文  参考訳（メタデータ） (2022-03-02T05:14:12Z)
• MAJORITY-3SAT (and Related Problems) in Polynomial Time [4.035753155957698]
  与えられた$k$-CNFが有界分母を持つ少なくとも$rho in (0,1)$を持つか否かを決定するアルゴリズムを与える。 我々のアルゴリズムは、複雑性と推論の複雑さを数えることに興味深いポジティブな意味を持っている。
  論文  参考訳（メタデータ） (2021-07-06T17:24:04Z)
• On Computation Complexity of True Proof Number Search [19.376328966299322]
  任意の有向非巡回グラフにおける証明数探索のための真エンフェスト数と真エンフェスト数の計算はNPハードであることを示す。 この証明にはSATからの還元が必要であり、任意のDAGに対して真の証明/反証数を見つけることは、任意のSATインスタンスが満足できるかどうかを決定するのと同じくらい難しいことを証明している。
  論文  参考訳（メタデータ） (2021-02-08T06:06:54Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。