論文の概要: Treewidth-aware Reductions of Normal ASP to SAT -- Is Normal ASP Harder
than SAT after All?
- arxiv url: http://arxiv.org/abs/2210.03553v1
- Date: Fri, 7 Oct 2022 13:40:07 GMT
- ステータス: 処理完了
- システム内更新日: 2022-10-10 15:04:16.154747
- Title: Treewidth-aware Reductions of Normal ASP to SAT -- Is Normal ASP Harder
than SAT after All?
- Title（参考訳）: 正常ASPからSATへの木幅対応化 -- 通常のASPはSATよりも難しいか?
- Authors: Markus Hecher
- Abstract要約: 木幅を考えると、通常のASPのフラグメントはSATよりもわずかに難しいことが判明した。
本報告では, 通常のASPからSATへの新規な縮小について実証的研究を行い, 既知分解による木幅上界の比較を行った。
- 参考スコア（独自算出の注目度）: 9.480212602202517
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Answer Set Programming (ASP) is a paradigm for modeling and solving problems
for knowledge representation and reasoning. There are plenty of results
dedicated to studying the hardness of (fragments of) ASP. So far, these studies
resulted in characterizations in terms of computational complexity as well as
in fine-grained insights presented in form of dichotomy-style results, lower
bounds when translating to other formalisms like propositional satisfiability
(SAT), and even detailed parameterized complexity landscapes. A generic
parameter in parameterized complexity originating from graph theory is the
so-called treewidth, which in a sense captures structural density of a program.
Recently, there was an increase in the number of treewidth-based solvers
related to SAT. While there are translations from (normal) ASP to SAT, no
reduction that preserves treewidth or at least keeps track of the treewidth
increase is known. In this paper we propose a novel reduction from normal ASP
to SAT that is aware of the treewidth, and guarantees that a slight increase of
treewidth is indeed sufficient. Further, we show a new result establishing
that, when considering treewidth, already the fragment of normal ASP is
slightly harder than SAT (under reasonable assumptions in computational
complexity). This also confirms that our reduction probably cannot be
significantly improved and that the slight increase of treewidth is
unavoidable. Finally, we present an empirical study of our novel reduction from
normal ASP to SAT, where we compare treewidth upper bounds that are obtained
via known decomposition heuristics. Overall, our reduction works better with
these heuristics than existing translations.
- Abstract（参考訳）: Answer Set Programming(ASP)は、知識表現と推論の問題をモデリングし、解決するためのパラダイムである。
asp.netの難しさ(フラグメント)を研究するための成果はたくさんあります。
これまでのこれらの研究は、計算複雑性や、二分法的な結果の形で提示されたきめ細かい洞察、命題的満足度(SAT)のような他の形式に翻訳する際の下限、さらには詳細なパラメータ化された複雑性の風景といった点で特徴づけられた。
グラフ理論に由来するパラメータ化複雑性の一般的なパラメータは木幅と呼ばれ、ある意味でプログラムの構造密度を捉える。
近年,SATに関連する木幅型解決器の数が増加している。
ASP から SAT への変換があるが、ツリー幅を保存したり、少なくともツリー幅の増加を追跡できる還元は知られていない。
本稿では,木幅を意識した通常の ASP から SAT への新規な削減を提案し,木幅のわずかな増加が十分であることを確認した。
さらに、木幅を考えると、通常のASPのフラグメントはSATよりもわずかに難しい(計算複雑性の合理的な仮定の下で)ことを示す新しい結果を示す。
これはまた、木幅のわずかな増加が避けられないため、この減少が著しく改善できないことも確認している。
最後に, 通常の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) - LiteSearch: Efficacious Tree Search for LLM [70.29796112457662]
本研究では,動的ノード選択とノードレベルの探索予算を備えた新しいガイド付き木探索アルゴリズムを提案する。
GSM8KおよびTabMWPデータセットを用いて行った実験により,本手法はベースライン法に比べて計算コストが大幅に低いことを示した。
論文 参考訳（メタデータ） (2024-06-29T05:14:04Z) - Extended Version of: On the Structural Hardness of Answer Set
Programming: Can Structure Efficiently Confine the Power of Disjunctions? [21.10339925217772]
プログラムのルール構造上での解離的ASPの構造パラメータの分類に対処する。
我々は、その範囲で最も顕著なパラメータに対して、二重指数下界を提供する。
本研究は, 通常のプログラムから解離プログラムへの新規な縮小に頼って, 深部硬度調査を行う。
論文 参考訳（メタデータ） (2024-02-05T21:51:36Z) - Tree Prompting: Efficient Task Adaptation without Fine-Tuning [112.71020326388029]
Tree Promptingはプロンプトの決定ツリーを構築し、複数のLMコールをリンクしてタスクを解決する。
分類データセットの実験により、Tree Promptingは競合するメソッドよりも精度が向上し、微調整と競合することが示された。
論文 参考訳（メタデータ） (2023-10-21T15:18:22Z) - 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) - 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) - Lassoed Tree Boosting [53.56229983630983]
有界断面変動のカドラー関数の大きな非パラメトリック空間において,早期に停止するn-1/4$ L2の収束速度を持つ勾配向上木アルゴリズムを証明した。
我々の収束証明は、ネストしたドンスカー類の経験的損失最小化子による早期停止に関する新しい一般定理に基づいている。
論文 参考訳（メタデータ） (2022-05-22T00:34:41Z) - Transformer-based Machine Learning for Fast SAT Solvers and Logic
Synthesis [63.53283025435107]
CNFベースのSATとMaxSATは論理合成と検証システムの中心である。
そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
論文 参考訳（メタデータ） (2021-07-15T04:47:35Z) - Treewidth-Aware Complexity in ASP: Not all Positive Cycles are Equally
Hard [15.5385123560379]
正規解集合プログラム (ASP) の整合性は、古典命題論理 (SAT) の満足度問題と同様にNP完全であることが知られている。
プログラムの正の依存性グラフにおいて, ラムダが木幅と最大の強結合成分のサイズの間の最小値であるような, k cdot log(lambda) において, ASP の整合性問題は指数時間で解くことができることを示す。
論文 参考訳（メタデータ） (2020-07-09T08:09:41Z) - From Checking to Inference: Actual Causality Computations as
Optimization Problems [79.87179017975235]
本稿では、最適化問題として二元非巡回モデルよりも、因果推論の異なる概念を定式化するための新しいアプローチを提案する。
8000ドル以上の変数を持つモデルを用いて,MaxSAT が ILP を上回り,数秒単位でチェック処理を行う場合が多い。
論文 参考訳（メタデータ） (2020-06-05T10:56:52Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。