論文の概要: Proof Complexity of Symbolic QBF Reasoning
- arxiv url: http://arxiv.org/abs/2104.02563v1
- Date: Tue, 6 Apr 2021 15:01:56 GMT
- ステータス: 処理完了
- システム内更新日: 2021-04-07 13:55:32.725777
- Title: Proof Complexity of Symbolic QBF Reasoning
- Title(参考訳): シンボリックQBF推論の複雑さの証明
- Authors: Stefan Mengel, Friedrich Slivovsky
- Abstract要約: OBDD(Ordered Binary Decision Diagrams)を用いたQBF(Quantified Boolean Formulas)のシンボリック証明システムの導入と検討
これらのシステムは記号量子化子除去を行うqbfソルバをキャプチャし、有界パス幅と量子化子複雑性の公式の短い証明を与える。
我々は,通信複雑性から既知の下限を取り除く戦略抽出に基づく記号的qbf証明システムのための下限手法を開発した。
- 参考スコア(独自算出の注目度): 6.85316573653194
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We introduce and investigate symbolic proof systems for Quantified Boolean
Formulas (QBF) operating on Ordered Binary Decision Diagrams (OBDDs). These
systems capture QBF solvers that perform symbolic quantifier elimination, and
as such admit short proofs of formulas of bounded path-width and quantifier
complexity. As a consequence, we obtain exponential separations from standard
clausal proof systems, specifically (long-distance) QU-Resolution and IR-Calc.
We further develop a lower bound technique for symbolic QBF proof systems
based on strategy extraction that lifts known lower bounds from communication
complexity. This allows us to derive strong lower bounds against symbolic QBF
proof systems that are independent of the variable ordering of the underlying
OBDDs, and that hold even if the proof system is allowed access to an
NP-oracle.
- Abstract(参考訳): 順序付き二項決定図(OBDD)で動作する量子ブール式(QBF)の記号的証明システムを導入・検討する。
これらのシステムは記号量子化子除去を行うqbfソルバをキャプチャし、有界パス幅と量子化子複雑性の公式の短い証明を与える。
その結果、標準クラス証明システム、特に(長距離)QU-ResolutionとIR-Calcから指数的分離が得られる。
さらに,通信複雑性から既知の下界を持ち上げる戦略抽出に基づく,記号的QBF証明システムのための下界技術を開発した。
これにより、基礎となる OBDD の変数順序に依存しない記号的 QBF 証明系に対して強い下位境界を導出することができ、証明系が NP-オラクルにアクセスできるとしても保持できる。
関連論文リスト
- Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [102.00359477458029]
本稿では,ニューラル・シンボリック統合法について述べる。
LLMフリーのシンボリック・ソルバを用いて、知識を用いた熟考的推論を行う。
論文 参考訳(メタデータ) (2023-11-16T11:26:21Z) - Tractable Bounding of Counterfactual Queries by Knowledge Compilation [51.47174989680976]
本稿では, パール構造因果モデルにおいて, 因果関係などの部分的特定可能なクエリのバウンダリングの問題について議論する。
最近提案された反復EMスキームは初期化パラメータをサンプリングしてそれらの境界を内部近似する。
シンボルパラメータを実際の値に置き換えた回路構造を,単一のシンボル知識コンパイルによって得られることを示す。
論文 参考訳(メタデータ) (2023-10-05T07:10:40Z) - A Hybrid System for Systematic Generalization in Simple Arithmetic
Problems [70.91780996370326]
本稿では,記号列に対する合成的および体系的推論を必要とする算術的問題を解くことができるハイブリッドシステムを提案する。
提案システムは,最も単純なケースを含むサブセットでのみ訓練された場合においても,ネストした数式を正確に解くことができることを示す。
論文 参考訳(メタデータ) (2023-06-29T18:35:41Z) - Advanced Tools and Methods for Treewidth-Based Problem Solving --
Extended Abstract [9.480212602202517]
この研究は、論理ベースの問題とツリー幅ベースの方法とそれを解決するツールに焦点を当てている。
本稿では,分解誘導(DG)による新しいタイプの問題削減について述べる。
木幅を直接利用して,Satの拡張を効率的に解くアルゴリズムを実装した。
論文 参考訳(メタデータ) (2022-08-24T07:43:58Z) - Sequential measurements, TQFTs, and TQNNs [0.0]
スケールフリーアーキテクチャで汎用量子情報を実装する新しい手法を提案する。
システムの境界となるホログラフィック画面から導出される測定演算子によって導出される有限ビット列が、観測結果をどのように捉えているかを示す。
解析を拡張して、トポロジカル量子ニューラルネットワーク(TQNN)を開発し、量子ニューラルネットワーク2-複素方程式の関手進化による機械学習を可能にする。
論文 参考訳(メタデータ) (2022-05-26T06:37:57Z) - Logical blocks for fault-tolerant topological quantum computation [55.41644538483948]
本稿では,プラットフォームに依存しない論理ゲート定義の必要性から,普遍的なフォールトトレラント論理の枠組みを提案する。
資源オーバーヘッドを改善するユニバーサル論理の新しいスキームについて検討する。
境界のない計算に好適な論理誤差率を動機として,新しい計算手法を提案する。
論文 参考訳(メタデータ) (2021-12-22T19:00:03Z) - Lifting Symmetry Breaking Constraints with Inductive Logic Programming [2.036811219647753]
我々は、Symmetry Breaking Constraintsを解釈可能な一階制約の集合に引き上げる、Answer Set Programmingのための新しいモデル指向のアプローチを導入する。
実験は、我々のフレームワークがインスタンス固有のSBCから一般的な制約を学習できることを実証する。
論文 参考訳(メタデータ) (2021-12-22T11:27:48Z) - Numerical estimation of reachable and controllability sets for a
two-level open quantum system driven by coherent and incoherent controls [77.34726150561087]
この記事では、ゴリーニ-コサコフスキー--リンドブラッド--スダルシャンマスター方程式によって支配される2段階の開量子系を考える。
系の密度行列のブロッホパラメトリゼーションを用いて解析する。
論文 参考訳(メタデータ) (2021-06-18T14:23:29Z) - Solution to the Quantum Symmetric Simple Exclusion Process : the
Continuous Case [0.0]
無限大極限における一次元 Q-SSEP の不変確率測度に対する解を提案する。
本稿では,Q-SSEP相関関数の解釈を,驚くべきコネラトニクスとアソシアヘドロン多面体を通して,偶然に指摘する。
論文 参考訳(メタデータ) (2020-06-22T13:20:40Z) - A tetrachotomy of ontology-mediated queries with a covering axiom [1.749935196721634]
我々の懸念は、標準的なデータベースクエリへの記述とそれらの最適な書き換えを介し、クエリに応答する際のデータ複雑さを効率的に決定することである。
我々は、疎結合シロップ(d-シロップ)と呼ばれるブール共役型クエリに焦点を当てる。
一部のd-シロップは指数的な大きさの分解能しか持たないが、そのうちのいくつかは二重指数サイズの正存在量書き換えと単帰的データログ書き換えのみである。
論文 参考訳(メタデータ) (2020-06-07T14:47:07Z) - Using Quantum Metrological Bounds in Quantum Error Correction: A Simple
Proof of the Approximate Eastin-Knill Theorem [77.34726150561087]
本稿では、量子誤り訂正符号の品質と、論理ゲートの普遍的な集合を達成する能力とを結びつける、近似したイージン・クニル定理の証明を示す。
我々の導出は、一般的な量子気象プロトコルにおける量子フィッシャー情報に強力な境界を用いる。
論文 参考訳(メタデータ) (2020-04-24T17:58:10Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。