論文の概要: SAT Requires Exhaustive Search
- arxiv url: http://arxiv.org/abs/2302.09512v7
- Date: Mon, 18 Sep 2023 04:41:39 GMT
- ステータス: 処理完了
- システム内更新日: 2023-09-20 00:38:55.604812
- Title: SAT Requires Exhaustive Search
- Title（参考訳）: SATは排他的検索を必要とする
- Authors: Ke Xu, Guangyan Zhou
- Abstract要約: 本稿では,計算硬度を証明することは数学では難しくないことを示す。
非常に難しい例では、徹底的な検索が唯一の選択肢かもしれない。
これにより、SAT(長い節を持つ)と3-SATの分離は、3-SATと2-SATの分離よりもずっと簡単になります。
- 参考スコア（独自算出の注目度）: 5.859552783895773
- License: http://creativecommons.org/licenses/by/4.0/
- 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の数学における形式的証明不可能性を証明するという結果が示すように、この論文の結果は計算の困難さを証明することは数学では難しくないことを示している。
具体的には, 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。