論文の概要: Treewidth-Aware Complexity in ASP: Not all Positive Cycles are Equally Hard

• arxiv url: http://arxiv.org/abs/2007.04620v1
• Date: Thu, 9 Jul 2020 08:09:41 GMT
• ステータス: 処理完了
• システム内更新日: 2022-11-12 05:20:57.382323
• Title: Treewidth-Aware Complexity in ASP: Not all Positive Cycles are Equally Hard
• Title（参考訳）: ASPのTreewidth-Aware Complexity: すべての正のサイクルが等しく難しいわけではない
• Authors: Markus Hecher, Jorge Fandinno
• Abstract要約: 正規解集合プログラム (ASP) の整合性は、古典命題論理 (SAT) の満足度問題と同様にNP完全であることが知られている。 プログラムの正の依存性グラフにおいて, ラムダが木幅と最大の強結合成分のサイズの間の最小値であるような, k cdot log(lambda) において, ASP の整合性問題は指数時間で解くことができることを示す。
• 参考スコア（独自算出の注目度）: 15.5385123560379
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: It is well-know that deciding consistency for normal answer set programs (ASP) is NP-complete, thus, as hard as the satisfaction problem for classical propositional logic (SAT). The best algorithms to solve these problems take exponential time in the worst case. The exponential time hypothesis (ETH) implies that this result is tight for SAT, that is, SAT cannot be solved in subexponential time. This immediately establishes that the result is also tight for the consistency problem for ASP. However, accounting for the treewidth of the problem, the consistency problem for ASP is slightly harder than SAT: while SAT can be solved by an algorithm that runs in exponential time in the treewidth k, it was recently shown that ASP requires exponential time in k \cdot log(k). This extra cost is due checking that there are no self-supported true atoms due to positive cycles in the program. In this paper, we refine the above result and show that the consistency problem for ASP can be solved in exponential time in k \cdot log({\lambda}) where {\lambda} is the minimum between the treewidth and the size of the largest strongly-connected component in the positive dependency graph of the program. We provide a dynamic programming algorithm that solves the problem and a treewidth-aware reduction from ASP to SAT that adhere to the above limit.
• Abstract（参考訳）: 正規解集合プログラム(ASP)の整合性を決定することはNP完全であり、古典命題論理(SAT)の満足度問題と同じくらい難しいことはよく知られている。 これらの問題を解決する最良のアルゴリズムは、最悪の場合指数関数的な時間がかかる。 指数時間仮説 (eth) は、この結果がsat、すなわちsatがサブ指数時間で解くことができないことを示唆する。 これにより、ASP.NETの一貫性の問題にも結果がきついことがすぐに証明される。 しかし、問題のツリー幅を考慮すると、ASP の一貫性問題は SAT よりもわずかに難しい:SAT は木幅 k において指数時間で実行されるアルゴリズムによって解けるが、最近、ASP は k \cdot log(k) において指数時間を必要とすることを示した。 この追加コストは、プログラムの正のサイクルのために自己支持の真の原子が存在しないことをチェックするためである。 本稿では,上述の結果を洗練し,プログラムの正の依存性グラフにおける最大強連結成分の最小値である k \cdot log({\lambda}) において,asp の一貫性問題を指数関数時間で解くことができることを示す。 上述の制限に従うASPからSATへのツリー幅対応の削減と問題を解く動的プログラミングアルゴリズムを提供する。

関連論文リスト

• Self-Satisfied: An end-to-end framework for SAT generation and prediction [0.7340017786387768]
  高速SAT問題生成のためのハードウェアアクセラレーションアルゴリズムと幾何SAT符号化を導入する。 これらの進歩により、何千もの変数と数万の節でSAT問題へのアプローチをスケールできます。 私たちの研究の基本的な側面は、SATデータの本質と、機械学習モデルのトレーニングに適合する可能性に関するものです。
  論文  参考訳（メタデータ） (2024-10-18T22:25:54Z)
• Decomposing Hard SAT Instances with Metaheuristic Optimization [52.03315747221343]
  分解硬度(d硬度)の概念を導入する。 d-硬度が$C$ w.r.tの硬度の推定値を示すことを示す。
  論文  参考訳（メタデータ） (2023-12-16T12:44:36Z)
• A Parallel and Distributed Quantum SAT Solver Based on Entanglement and Quantum Teleportation [1.5201992393140886]
  並列量子SATソルバは,線形時間 O(m) から定数時間 O(1) までの繰り返しの時間複雑性を,余分な絡み合った量子ビットを用いて低減する。 我々は、我々のアプローチの正しさを証明し、シミュレーションでそれらを実証した。
  論文  参考訳（メタデータ） (2023-08-07T06:52:06Z)
• Information-Computation Tradeoffs for Learning Margin Halfspaces with Random Classification Noise [50.64137465792738]
  ランダム分類ノイズを用いたPAC$gamma$-marginハーフスペースの問題について検討する。 我々は、問題のサンプル複雑性と計算効率の良いアルゴリズムのサンプル複雑性との間に固有のギャップを示唆する情報計算トレードオフを確立する。
  論文  参考訳（メタデータ） (2023-06-28T16:33:39Z)
• W2SAT: Learning to generate SAT instances from Weighted Literal Incidence Graphs [11.139131079925113]
  W2SATは、現実世界/産業インスタンスから固有の構造と特性を学ぶことによってSAT式を生成するフレームワークである。 Weighted Literal Incidence Graph (WLIG)と呼ばれる新しいSAT表現を導入する。 WLIGからSAT問題への復号化は、新しい丘登り最適化法で重なり合う斜角を見つけることをモデル化する。
  論文  参考訳（メタデータ） (2023-02-01T06:30:41Z)
• Characterizing Structural Hardness of Logic Programs: What makes Cycles and Reachability Hard for Treewidth? [9.480212602202517]
  本稿では、よく知られたエンコーディングを超えるSATから通常のASPへの新規な削減について述べる。 これは依存性グラフのサイクル長の必要な機能的依存性を確立することによって、きめ細かい方法で硬さを特徴づける。
  論文  参考訳（メタデータ） (2023-01-18T12:29:45Z)
• Treewidth-aware Reductions of Normal ASP to SAT -- Is Normal ASP Harder than SAT after All? [9.480212602202517]
  木幅を考えると、通常のASPのフラグメントはSATよりもわずかに難しいことが判明した。 本報告では, 通常のASPからSATへの新規な縮小について実証的研究を行い, 既知分解による木幅上界の比較を行った。
  論文  参考訳（メタデータ） (2022-10-07T13:40:07Z)
• 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)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
  論文  参考訳（メタデータ） (2021-07-15T04:47:35Z)
• From Checking to Inference: Actual Causality Computations as Optimization Problems [79.87179017975235]
  本稿では、最適化問題として二元非巡回モデルよりも、因果推論の異なる概念を定式化するための新しいアプローチを提案する。 8000ドル以上の変数を持つモデルを用いて,MaxSAT が ILP を上回り,数秒単位でチェック処理を行う場合が多い。
  論文  参考訳（メタデータ） (2020-06-05T10:56:52Z)

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

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