論文の概要: Presburger Functional Synthesis: Complexity and Tractable Normal Forms
- arxiv url: http://arxiv.org/abs/2508.07207v1
- Date: Sun, 10 Aug 2025 07:00:34 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-08-12 21:23:28.753219
- Title: Presburger Functional Synthesis: Complexity and Tractable Normal Forms
- Title（参考訳）: プレスバーグ官能基合成 : 複雑度とトラクタブル正規形
- Authors: S. Akshay, A. R. Balasubramanian, Supratik Chakraborty, Georg Zetzsche,
- Abstract要約: プレスバーグ関数合成 (PFnS) は EXPTIME で解くことができ, 指数的下界が一致することを示す。
次に、PSyNFと呼ばれる特殊正規形式を、PFnSのポリ時間およびポリサイズ可溶性を保証する仕様式として同定する。
我々はPSyNFのいくつかの特性を証明し、PSyNFにポリ時間でPSyNFのポリ時間可溶性を保証する他の形式をPSyNFにコンパイルできる条件について述べる。
- 参考スコア（独自算出の注目度）: 0.4499833362998487
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Given a relational specification between inputs and outputs as a logic formula, the problem of functional synthesis is to automatically synthesize a function from inputs to outputs satisfying the relation. Recently, a rich line of work has emerged tackling this problem for specifications in different theories, from Boolean to general first-order logic. In this paper, we launch an investigation of this problem for the theory of Presburger Arithmetic, that we call Presburger Functional Synthesis (PFnS). We show that PFnS can be solved in EXPTIME and provide a matching exponential lower bound. This is unlike the case for Boolean functional synthesis (BFnS), where only conditional exponential lower bounds are known. Further, we show that PFnS for one input and one output variable is as hard as BFnS in general. We then identify a special normal form, called PSyNF, for the specification formula that guarantees poly-time and poly-size solvability of PFnS. We prove several properties of PSyNF, including how to check and compile to this form, and conditions under which any other form that guarantees poly-time solvability of PFnS can be compiled in poly-time to PSyNF. Finally, we identify a syntactic normal form that is easier to check but is exponentially less succinct than PSyNF.
- Abstract（参考訳）: 論理式として入力と出力の間の関係仕様が与えられたとき、関数合成の問題は、入力からその関係を満たす出力まで関数を自動的に合成することである。
近年,ブール理論から一般一階述語論理まで,様々な理論でこの問題に対処する研究が盛んに行われている。
本稿では,プレズバーグ関数合成(PFnS)と呼ばれる,プレズバーグの算術理論に対するこの問題の調査を開始する。
PFnS は EXPTIME で解けることを示すとともに,指数的下界が一致することを示す。
これはブール汎関数合成(BFnS)の場合と異なり、条件付き指数的な下界のみが知られている。
さらに、1つの入力と1つの出力変数に対するPFnSは、一般的にはBFnSと同じくらい硬いことを示す。
次に、PSyNFと呼ばれる特殊正規形式を、PFnSのポリ時間およびポリサイズ可溶性を保証する仕様式として同定する。
我々はPSyNFのいくつかの特性を証明し、PSyNFにポリ時間でPSyNFのポリ時間可溶性を保証する他の形式をPSyNFにコンパイルできる条件について述べる。
最後に,PSyNFよりも指数的に簡潔でない構文正規形式を同定する。
関連論文リスト
- Explicit Solution Equation for Every Combinatorial Problem via Tensor Networks: MeLoCoToN [55.2480439325792]
計算問題はすべて、解を返却する厳密な明示的な方程式を持つことを示す。
本稿では, インバージョン, 制約満足度, 最適化の両面から, 正確に任意の問題を解く方程式を得る方法を提案する。
論文 参考訳（メタデータ） (2025-02-09T18:16:53Z) - Compilation and Fast Model Counting beyond CNF [31.620928650659586]
本稿では,関数のクラスを効率的にd-DNNFに変換するか,あるいはコンパイルするかに関する理論的知識を強化する。
問題の制約は、すべての変数順序付けに対して、定数幅順序付きバイナリ決定図(OBDD)で表現可能なすべての関数である。
制約のサブファミリーに適用し,コンパイルを必要としないモデルカウントのためのより効率的なFPTアルゴリズムを提案する。
論文 参考訳（メタデータ） (2025-02-01T14:00:04Z) - Linear Temporal Logic Modulo Theories over Finite Traces (Extended
Version) [72.38188258853155]
有限トレース(LTLf)上の線形時間論理について検討する。
命題の文字は任意の理論で解釈された一階述語式に置き換えられる。
Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
論文 参考訳（メタデータ） (2022-04-28T17:57:33Z) - Evolutionary Construction of Perfectly Balanced Boolean Functions [7.673465837624365]
遺伝的プログラミング (GP) と遺伝的アルゴリズム (GA) を用いて, 特性, 完全均衡性, および優れた非線形性プロファイルを満たすブール関数を構築する。
意外なことに、重み付けされた表現を持つGAは、非常に非線形なWPB関数を見つける際に、古典的真理表表現型でGPより優れていた。
論文 参考訳（メタデータ） (2022-02-16T18:03:04Z) - Interactive Proofs for Synthesizing Quantum States and Unitaries [0.15229257192293197]
量子状態の構築やユニタリ変換の実行など、本質的に量子演算の複雑さについて検討する。
量子状態とユニタリの対話的証明のモデルを定義する。
複数の絡み合ったプロバーの設定でも類似した結果が得られる。
論文 参考訳（メタデータ） (2021-08-16T15:59:33Z) - A Normal Form Characterization for Efficient Boolean Skolem Function
Synthesis [2.093287944284448]
本稿では,通常の合成をトラクタブルに特徴づけるSAUNFという表現形式を提案する。
AIの問題の文脈で使用されるBDDやDNNFのような確立された通常の形式よりも指数関数的に簡潔であり、SynNNFのような他のより最近提案された形式を厳密に推定する。
論文 参考訳（メタデータ） (2021-04-29T04:16:41Z) - Finite-Function-Encoding Quantum States [52.77024349608834]
任意の$d$値論理関数を符号化する有限関数符号化(FFE)を導入する。
それらの構造的特性について検討する。
論文 参考訳（メタデータ） (2020-12-01T13:53:23Z) - On Function Approximation in Reinforcement Learning: Optimism in the
Face of Large State Spaces [208.67848059021915]
強化学習のコアにおける探索・探索トレードオフについて検討する。
特に、関数クラス $mathcalF$ の複雑さが関数の複雑さを特徴づけていることを証明する。
私たちの後悔の限界はエピソードの数とは無関係です。
論文 参考訳（メタデータ） (2020-11-09T18:32:22Z) - A tetrachotomy of ontology-mediated queries with a covering axiom [1.749935196721634]
我々の懸念は、標準的なデータベースクエリへの記述とそれらの最適な書き換えを介し、クエリに応答する際のデータ複雑さを効率的に決定することである。
我々は、疎結合シロップ(d-シロップ)と呼ばれるブール共役型クエリに焦点を当てる。
一部のd-シロップは指数的な大きさの分解能しか持たないが、そのうちのいくつかは二重指数サイズの正存在量書き換えと単帰的データログ書き換えのみである。
論文 参考訳（メタデータ） (2020-06-07T14:47:07Z) - On estimating the entropy of shallow circuit outputs [49.1574468325115]
確率分布と量子状態のエントロピーを推定することは情報処理の基本的な課題である。
本稿では,有界ファンインと非有界ファンアウトのゲートを持つ対数深度回路か定数深度回路のいずれかによって生成された分布や状態に対するエントロピー推定が,少なくともLearning with Errors問題と同程度難しいことを示す。
論文 参考訳（メタデータ） (2020-02-27T15:32:08Z) - Learning Likelihoods with Conditional Normalizing Flows [54.60456010771409]
条件正規化フロー(CNF)はサンプリングと推論において効率的である。
出力空間写像に対する基底密度が入力 x 上で条件づけられた CNF について、条件密度 p(y|x) をモデル化する。
論文 参考訳（メタデータ） (2019-11-29T19:17:58Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。