論文の概要: Canonical Decision Diagrams Modulo Theories
- arxiv url: http://arxiv.org/abs/2404.16455v1
- Date: Thu, 25 Apr 2024 09:34:49 GMT
- ステータス: 処理完了
- システム内更新日: 2024-04-26 14:19:10.419821
- Title: Canonical Decision Diagrams Modulo Theories
- Title(参考訳): 正準決定ダイアグラムによるモデュロ理論
- Authors: Massimo Michelutti, Gabriele Masina, Giuseppe Spallitta, Roberto Sebastiani,
- Abstract要約: 決定図は命題公式を表現する強力なツールである。
いくつかの形式(例えば OBDD や SDD など)は標準的であり、(原子リスト上の与えられた条件の下では)公式の同値類を単項的に表す。
DDをSMTレベルに活用する新しい手法を提案する。
- 参考スコア(独自算出の注目度): 0.19285000127136376
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Decision diagrams (DDs) are powerful tools to represent effectively propositional formulas, which are largely used in many domains, in particular in formal verification and in knowledge compilation. Some forms of DDs (e.g., OBDDs, SDDs) are canonical, that is, (under given conditions on the atom list) they univocally represent equivalence classes of formulas. Given the limited expressiveness of propositional logic, a few attempts to leverage DDs to SMT level have been presented in the literature. Unfortunately, these techniques still suffer from some limitations: most procedures are theory-specific; some produce theory DDs (T-DDs) which do not univocally represent T-valid formulas or T-inconsistent formulas; none of these techniques provably produces theory-canonical T-DDs, which (under given conditions on the T-atom list) univocally represent T-equivalence classes of formulas. Also, these procedures are not easy to implement, and very few implementations are actually available. In this paper, we present a novel very-general technique to leverage DDs to SMT level, which has several advantages: it is very easy to implement on top of an AllSMT solver and a DD package, which are used as blackboxes; it works for every form of DDs and every theory, or combination thereof, supported by the AllSMT solver; it produces theory-canonical T-DDs if the propositional DD is canonical. We have implemented a prototype tool for both T-OBDDs and T-SDDs on top of OBDD and SDD packages and the MathSAT SMT solver. Some preliminary empirical evaluation supports the effectiveness of the approach.
- Abstract(参考訳): 決定図(Decision diagrams, DD)は、多くの領域、特に形式的検証や知識コンパイルにおいて、効果的に命題式を表現する強力なツールである。
DDのいくつかの形式(例: OBDDs, SDDs)は標準的であり、(原子リスト上の与えられた条件の下では)公式の同値類を一意的に表す。
命題論理の限られた表現性を考えると、DDをSMTレベルに活用する試みが文献で紹介されている。
残念なことに、これらの技術は依然としていくつかの制限に悩まされている: ほとんどの手順は理論固有のものであり、いくつかの生成理論DD(T-DDs)は T-valid 式や T-consistent 式を単項的に表さない。
また、これらの手順は実装が簡単ではなく、実際に実装できるものはほとんどありません。
本稿では,全SMT ソルバと DD パッケージをブラックボックスとして実装することは極めて容易であり,すべての DD の形式や,AllSMT ソルバがサポートする理論,あるいはその組み合わせに対して有効であり,提案 DD が正則であれば理論-正準 T-DD を生成するという,SMT レベルに DD を活用するための新しい手法を提案する。
我々は,OBDDとSDDパッケージとMathSAT SMTソルバ上に,T-OBDDとT-SDDのプロトタイプツールを実装した。
いくつかの予備的な経験的評価は、アプローチの有効性を支持する。
関連論文リスト
- MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [88.72298746872396]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳(メタデータ) (2024-02-14T05:57:58Z) - MDD-UNet: Domain Adaptation for Medical Image Segmentation with
Theoretical Guarantees, a Proof of Concept [3.376269351435396]
理論的保証付きU-Netのための教師なしドメイン適応フレームワークを提案する。
MDD-UNetは、ターゲットドメインのラベルに関する知識のない、ドメイン不変の機能を学ぶことができる。
この研究は、モダンな拡張なしに標準形式でのU-Netの改善を示すことによって、概念実証として機能する。
論文 参考訳(メタデータ) (2023-12-19T15:30:10Z) - An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes [4.393684402895834]
Algebraic Data Types (ADT) は関数型プログラミング言語で古典的に見られる構造である。
我々は,基本的に異なるアプローチ,エフェーガーアプローチを採るSMTソルバを提案する。
論文 参考訳(メタデータ) (2023-10-18T18:14:18Z) - Top-Down Knowledge Compilation for Counting Modulo Theories [11.086759883832505]
入力式が決定論的分解可能な否定正規形(d-DNNF)である場合、仮説モデルカウントは効率的に解ける。
トップダウン知識コンパイルは#SAT問題を解決する最先端技術である。
我々は,DPLL(T)探索の痕跡に基づくトップダウンコンパイラを提唱する。
論文 参考訳(メタデータ) (2023-06-07T15:46:28Z) - On Pitfalls of Test-Time Adaptation [82.8392232222119]
TTA(Test-Time Adaptation)は、分散シフトの下で堅牢性に取り組むための有望なアプローチとして登場した。
TTABは,10の最先端アルゴリズム,多種多様な分散シフト,および2つの評価プロトコルを含むテスト時間適応ベンチマークである。
論文 参考訳(メタデータ) (2023-06-06T09:35:29Z) - AdaNPC: Exploring Non-Parametric Classifier for Test-Time Adaptation [64.9230895853942]
ドメインの一般化は、ターゲットのドメイン情報を活用することなく、任意に困難にすることができる。
この問題に対処するためにテスト時適応(TTA)手法が提案されている。
本研究では,テスト時間適応(AdaNPC)を行うためにNon-Parametricを採用する。
論文 参考訳(メタデータ) (2023-04-25T04:23:13Z) - Linear Temporal Logic Modulo Theories over Finite Traces (Extended
Version) [72.38188258853155]
有限トレース(LTLf)上の線形時間論理について検討する。
命題の文字は任意の理論で解釈された一階述語式に置き換えられる。
Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
論文 参考訳(メタデータ) (2022-04-28T17:57:33Z) - Measuring dissimilarity with diffeomorphism invariance [94.02751799024684]
DID(DID)は、幅広いデータ空間に適用可能なペアワイズな相似性尺度である。
我々は、DIDが理論的研究と実用に関係のある特性を享受していることを証明する。
論文 参考訳(メタデータ) (2022-02-11T13:51:30Z) - Belief Revision in Sentential Decision Diagrams [126.94029917018733]
本研究では,Dalリビジョンの構文的特徴化に基づくSDDの一般的なリビジョンアルゴリズムを開発する。
ランダムに生成した知識ベースを用いた予備実験は、SDDフォーマリズム内で直接リビジョンを行う利点を示している。
論文 参考訳(メタデータ) (2022-01-20T11:01:41Z) - Variable Shift SDD: A More Succinct Sentential Decision Diagram [10.91026094237478]
Sentential Decision Diagram (SDD) はブール関数の抽出可能な表現である。
可変シフトSDD(VS-SDD)という,より簡潔なSDD変種を提案する。
我々は,VS-SDDがSDDよりも大きくなることはなく,VS-SDDのサイズがSDDよりも指数関数的に小さいケースがあることを示した。
論文 参考訳(メタデータ) (2020-04-06T09:18:19Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。