論文の概要: Exact ASP Counting with Compact Encodings

• arxiv url: http://arxiv.org/abs/2312.11936v1
• Date: Tue, 19 Dec 2023 08:27:29 GMT
• ステータス: 処理完了
• システム内更新日: 2023-12-20 16:30:25.285454
• Title: Exact ASP Counting with Compact Encodings
• Title（参考訳）: コンパクトエンコーディングによる正確な asp カウント
• Authors: Mohimenul Kabir and Supratik Chakraborty and Kuldeep S Meel
• Abstract要約: 本稿では、より大規模な入力式を避けるために、応答集合をカウントする sharpASP と呼ばれる新しいASPカウントフレームワークを提案する。 1470のベンチマークによる実証分析は、現在の最先端の正解集合カウンタよりも大きなパフォーマンス向上を示している。
• 参考スコア（独自算出の注目度）: 32.300155018027624
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Answer Set Programming (ASP) has emerged as a promising paradigm in knowledge representation and automated reasoning owing to its ability to model hard combinatorial problems from diverse domains in a natural way. Building on advances in propositional SAT solving, the past two decades have witnessed the emergence of well-engineered systems for solving the answer set satisfiability problem, i.e., finding models or answer sets for a given answer set program. In recent years, there has been growing interest in problems beyond satisfiability, such as model counting, in the context of ASP. Akin to the early days of propositional model counting, state-of-the-art exact answer set counters do not scale well beyond small instances. Exact ASP counters struggle with handling larger input formulas. The primary contribution of this paper is a new ASP counting framework, called sharpASP, which counts answer sets avoiding larger input formulas. This relies on an alternative way of defining answer sets that allows for the lifting of key techniques developed in the context of propositional model counting. Our extensive empirical analysis over 1470 benchmarks demonstrates significant performance gain over current state-of-the-art exact answer set counters. Specifically, by using sharpASP, we were able to solve 1062 benchmarks with PAR2 score of 3082 whereas using prior state-of-the-art, we could only solve 895 benchmarks with a PAR2 score of 4205, all other experimental conditions being the same.
• Abstract（参考訳）: 解集合プログラミング(asp)は、多様なドメインから自然な方法でハードコンビネート問題を記述する能力により、知識表現と自動推論において有望なパラダイムとして登場してきた。 命題SAT解決の進歩に基づいて、過去20年にわたって、解集合が満足できる問題、すなわち与えられた解集合プログラムのモデルや解集合を見つけるための、よく設計されたシステムの出現を目撃してきた。 近年、asp.net mvcの文脈では、モデルカウントなどの満足度を超えた問題への関心が高まっている。 命題モデルカウントの初期と同様に、最先端の正確な答え集合カウンタは、小さなインスタンス以上にはスケールしない。 ASPカウンタは、より大きな入力式を扱うのに苦労します。 この論文の主な貢献は、より大きな入力公式を避けるための回答集合をカウントするsharpaspと呼ばれる新しいaspカウントフレームワークである。 これは、命題モデル数え上げの文脈で開発された重要なテクニックの持ち上げを可能にする解集合を定義する別の方法に依存する。 1470ベンチマークに対する我々の広範な実証分析は、現在の最先端の正解集合カウンタよりも大きなパフォーマンス向上を示している。 具体的には、シャープASPを使用することで、PAR2スコアが3082の1062ベンチマークを解くことができたが、先行技術を使用した場合、PAR2スコアが4205の895ベンチマークしか解決できなかった。

関連論文リスト

• IASCAR: Incremental Answer Set Counting by Anytime Refinement [18.761758874408557]
  本稿では,CNFの知識コンパイルを前提として,サポート対象モデルを符号化する手法を提案する。 予備的な実証分析では,有望な結果を示す。
  論文  参考訳（メタデータ） (2023-11-13T10:53:48Z)
• Answer-Set Programming for Lexicographical Makespan Optimisation in Parallel Machine Scheduling [18.286430978487388]
  我々は、シーケンス依存のセットアップ時間とリリース日を持つ並列マシン上で、困難なスケジューリング問題に対処する。 個々のマシンを非到達順に配置し、結果として生じるロバスト性を語彙的に最小化する。 実験の結果,ASPは実際にこの問題に対して有望なKRRパラダイムであり,最先端のCPおよびMIPソルバと競合していることがわかった。
  論文  参考訳（メタデータ） (2022-12-18T12:43:24Z)
• Successive Prompting for Decomposing Complex Questions [50.00659445976735]
  最近の研究は、大規模言語モデル(LM)の機能を活用して、数ショットで複雑な質問応答を行う。 そこでは、複雑なタスクを単純なタスクに繰り返し分解し、それを解決し、最終解を得るまでプロセスを繰り返します。 我々の最良のモデル(逐次プロンプト付き)は、DROPデータセットの数ショットバージョンにおいて、5%の絶対F1の改善を実現します。
  論文  参考訳（メタデータ） (2022-12-08T06:03:38Z)
• Aggregate Semantics for Propositional Answer Set Programs [14.135212040150389]
  提案するASPプログラムに対して提案された主要な集合的セマンティクスを提示し、比較する。 計算複雑性や表現力などの重要な特性を強調し、異なるアプローチの能力と限界を概説する。
  論文  参考訳（メタデータ） (2021-09-17T17:38:55Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
  論文  参考訳（メタデータ） (2021-07-15T04:47:35Z)
• grASP: A Graph Based ASP-Solver and Justification System [5.098678276629787]
  本稿では,目標の結合をノードとして明示的に表現する,新たな依存グラフに基づく解集合探索手法を提案する。 私たちの表現は因果関係を保ち、答えセットの各リテラルをエレガントに見つけるために正当化します。
  論文  参考訳（メタデータ） (2021-04-02T18:16:20Z)
• Few-Shot Question Answering by Pretraining Span Selection [58.31911597824848]
  私たちは、数百のトレーニング例しか利用できない、より現実的な数ショット設定を探索します。 標準スパン選択モデルの性能が低下していることを示し,現在の事前学習目標が質問応答から遠ざかっていることを浮き彫りにした。 本研究は,事前学習方式とモデルアーキテクチャの注意深い設計が,数ショット設定における性能に劇的な影響を及ぼすことを示唆している。
  論文  参考訳（メタデータ） (2021-01-02T11:58:44Z)
• Session-Aware Query Auto-completion using Extreme Multi-label Ranking [61.753713147852125]
  本稿では,セッション対応クエリ自動補完の新たな手法を,XMR(Multi Multi-Xtreme Ranking)問題として取り上げる。 アルゴリズムのキーステップにいくつかの修正を提案することにより、この目的のために一般的なXMRアルゴリズムを適応させる。 当社のアプローチは、セッション情報を活用しながら、自動補完システムの厳しいレイテンシ要件を満たします。
  論文  参考訳（メタデータ） (2020-12-09T17:56:22Z)
• LP2PB: Translating Answer Set Programs into Pseudo-Boolean Theories [0.0]
  本稿では、ASPプログラムを擬似ブール理論に変換する新しいツールLP2PBを提案する。 従来のASPベンチマークで、当社のツールと、ASPに対するカットプレーンベースの問題解決の可能性を評価します。
  論文  参考訳（メタデータ） (2020-09-22T00:50:17Z)
• From Checking to Inference: Actual Causality Computations as Optimization Problems [79.87179017975235]
  本稿では、最適化問題として二元非巡回モデルよりも、因果推論の異なる概念を定式化するための新しいアプローチを提案する。 8000ドル以上の変数を持つモデルを用いて,MaxSAT が ILP を上回り,数秒単位でチェック処理を行う場合が多い。
  論文  参考訳（メタデータ） (2020-06-05T10:56:52Z)

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

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