論文の概要: Are Hitting Formulas Hard for Resolution?

• arxiv url: http://arxiv.org/abs/2206.15225v1
• Date: Thu, 30 Jun 2022 12:13:26 GMT
• ステータス: 処理完了
• システム内更新日: 2022-07-01 15:17:27.556872
• Title: Are Hitting Formulas Hard for Resolution?
• Title（参考訳）: フォーミュラの雇用は解決が難しいか?
• Authors: Tom\'a\v{s} Peitl and Stefan Szeider
• Abstract要約: 打球公式の解の複雑さは、いわゆる既約打球公式に支配されていることを示す。 最大14節のヒット式を列挙する効率的なアルゴリズムを実装した。
• 参考スコア（独自算出の注目度）: 26.575053800551633
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: Hitting formulas, introduced by Iwama, are an unusual class of propositional CNF formulas. Not only is their satisfiability decidable in polynomial time, but even their models can be counted in closed form. This stands in stark contrast with other polynomial-time decidable classes, which usually have algorithms based on backtracking and resolution and for which model counting remains hard, like 2-SAT and Horn-SAT. However, those resolution-based algorithms usually easily imply an upper bound on resolution complexity, which is missing for hitting formulas. Are hitting formulas hard for resolution? In this paper we take the first steps towards answering this question. We show that the resolution complexity of hitting formulas is dominated by so-called irreducible hitting formulas, first studied by Kullmann and Zhao, that cannot be composed of smaller hitting formulas. However, by definition, large irreducible unsatisfiable hitting formulas are difficult to construct; it is not even known whether infinitely many exist. Building upon our theoretical results, we implement an efficient algorithm on top of the Nauty software package to enumerate all irreducible unsatisfiable hitting formulas with up to 14 clauses. We also determine the exact resolution complexity of the generated hitting formulas with up to 13 clauses by extending a known SAT encoding for our purposes. Our experimental results suggest that hitting formulas are indeed hard for resolution.
• Abstract（参考訳）: 岩間によって導入されたハッティング公式は、命題CNF公式の珍しいクラスである。 多項式時間で満足度が決定可能であるだけでなく、それらのモデルでさえ閉形式で数えられる。 これは、バックトラックと解像度に基づくアルゴリズムを持ち、2-SAT や Horn-SAT のようなモデルカウントが難しい他の多項式時間決定可能なクラスとは対照的である。 しかし、これらの解法に基づくアルゴリズムは、通常、解法を打つために欠落している解法複雑性の上限を示唆する。 フィギュアリングは難しいのか? 本稿では,この質問に答える第一歩を踏み出す。 打球公式の解複雑性は、Kulmann と Zhao が最初に研究したいわゆる既約打球公式に支配されるが、これはより小さな打球公式では成り立たない。 しかし、定義上、大きな既約な打撃公式は構成が困難であり、無限に多数存在するかどうかは分かっていない。 理論的な結果に基づいて,nautyソフトウェアパッケージ上に効率的なアルゴリズムを実装し,最大14節の既約ヒット数を列挙する。 また、既知のSATエンコーディングを我々の目的のために拡張することにより、最大13節のヒット公式の正確な解複雑性も決定する。 実験結果から,打抜き式は解決が難しいことが示唆された。

関連論文リスト

• Unsupervised Discovery of Formulas for Mathematical Constants [0.0]
  本稿では,これらの公式の分類,特徴化,パターン同定のための体系的手法を提案する。 我々の方法論の鍵となるのは、公式の数値ではなく、公式の収束力学に基づくメトリクスの導入である。 我々は1,768,900のそのような公式の集合上で我々の方法論を検証し、数学定数の既知の多くの公式を同定し、以前は知られていなかった$pi$, $ln(2)$, Gaus', Lemniscateの定数を発見した。
  論文  参考訳（メタデータ） (2024-12-22T01:43:56Z)
• Simple and Provable Scaling Laws for the Test-Time Compute of Large Language Models [70.07661254213181]
  大規模言語モデルのテスト時間計算のための2つの原理的アルゴリズムを提案する。 理論的には、1つのアルゴリズムの故障確率は、そのテスト時間計算が大きくなるにつれて指数関数的に減衰する。
  論文  参考訳（メタデータ） (2024-11-29T05:29:47Z)
• General Boolean Formula Minimization with QBF Solvers [4.264192013842096]
  我々は任意の形式で同等の式を得るという問題に興味を持っている。 我々は、最小化アルゴリズムを適用して、元の公式の自然言語翻訳を生成する動機付けをしている。 我々はその問題を解決するための3つの可能な(実践的な)アプローチを分析する。
  論文  参考訳（メタデータ） (2023-03-12T12:08:58Z)
• Arbitrarily Large Labelled Random Satisfiability Formulas for Machine Learning Training [5.414308305392762]
  決定問題を解くことなく、任意の大きさのランダムな式を正しくラベル付けする方法を示す。 我々は1万変数の式で満足度を予測するタスクのために、既存の最先端モデルを訓練する。 同じデータセットで99%をランダムに推測するのに勝るものは見当たらない。
  論文  参考訳（メタデータ） (2022-11-21T17:52:13Z)
• Superredundancy: A tool for Boolean formula minimization complexity analysis [0.0]
  超冗長節 (superredundant clause) は、公式の解法閉鎖において冗長な節である。 逆の超冗長性の概念は、与えられたものと同値であるすべての最小のCNF式における節のメンバシップを保証する。
  論文  参考訳（メタデータ） (2022-05-02T09:17:52Z)
• A Scalable Combinatorial Solver for Elastic Geometrically Consistent 3D Shape Matching [69.14632473279651]
  本稿では,3次元形状間の幾何学的一貫したマッピング空間をグローバルに最適化するスケーラブルなアルゴリズムを提案する。 従来の解法よりも数桁高速なラグランジュ双対問題と結合した新しい原始問題を提案する。
  論文  参考訳（メタデータ） (2022-04-27T09:47:47Z)
• A Closed-Form Solution to Local Non-Rigid Structure-from-Motion [107.60023055615302]
  広く適用可能な仮定の下では、曲面正規化の観点から新しい方程式系を導出できることが示される。 2つ以上のビューから得られた再構成は、最先端の手法よりもはるかに正確です。
  論文  参考訳（メタデータ） (2020-11-23T17:26:19Z)
• Causal Expectation-Maximisation [70.45873402967297]
  ポリツリーグラフを特徴とするモデルにおいても因果推論はNPハードであることを示す。 我々は因果EMアルゴリズムを導入し、分類的表現変数のデータから潜伏変数の不確かさを再構築する。 我々は、反事実境界が構造方程式の知識なしにしばしば計算できるというトレンドのアイデアには、目立たずの制限があるように思える。
  論文  参考訳（メタデータ） (2020-11-04T10:25:13Z)
• One head is better than two: a polynomial restriction for propositional definite Horn forgetting [0.0]
  忘れることは、命題ホルンの公式の単純な場合でさえ np-完全である。 いくつかの公式はシングルヘッドではなく、忘れるのを簡単にするために作成することができる。
  論文  参考訳（メタデータ） (2020-09-16T06:49:08Z)
• Hardness of Random Optimization Problems for Boolean Circuits, Low-Degree Polynomials, and Langevin Dynamics [78.46689176407936]
  アルゴリズムの族は高い確率でほぼ最適な解を生成できないことを示す。 ブール回路の場合、回路複雑性理論で知られている最先端境界を改善する。
  論文  参考訳（メタデータ） (2020-04-25T05:45:59Z)

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

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