論文の概要: 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節のヒット公式の正確な解複雑性も決定する。 実験結果から,打抜き式は解決が難しいことが示唆された。

関連論文リスト

• 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)
• Fast Feature Selection with Fairness Constraints [49.142308856826396]
  モデル構築における最適特徴の選択に関する基礎的問題について検討する。 この問題は、greedyアルゴリズムの変種を使用しても、大規模なデータセットで計算的に困難である。 適応クエリモデルは,最近提案された非モジュラー関数に対する直交整合探索のより高速なパラダイムに拡張する。 提案アルゴリズムは、適応型クエリモデルにおいて指数関数的に高速な並列実行を実現する。
  論文  参考訳（メタデータ） (2022-02-28T12:26: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)
• Bounds on the size of PC and URC formulas [0.0]
  式が存在量化された補助変数を使って関数を表す場合、それは関数の符号化と呼ばれる。 我々はPC と URC の公式とエンコーディングのサイズについていくつかの結果を示した。 任意のq-Horn式に対して、補助変数を用いて同じ関数を符号化する大きさのURCを示す。
  論文  参考訳（メタデータ） (2020-01-03T13:15:32Z)

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

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