論文の概要: 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-オラクルにアクセスできるとしても保持できる。

関連論文リスト

• Data-Driven Abstractions via Binary-Tree Gaussian Processes for Formal Verification [0.22499166814992438]
  ガウス過程(GP)回帰に基づく抽象的解は、量子化された誤差を持つデータから潜在システムの表現を学習する能力で人気を博している。 二分木ガウス過程(BTGP)により未知系のマルコフ連鎖モデルを構築することができることを示す。 BTGPの関数空間に真の力学が存在しない場合でも、統一公式による非局在誤差量子化を提供する。
  論文  参考訳（メタデータ） (2024-07-15T11:49:44Z)
• Constructive Interpolation and Concept-Based Beth Definability for Description Logics via Sequents [0.0]
  本稿では,概念に基づくBeth Definability Properties (CBP) を確立するための構築的手法を提案する。 高い表現力を持つDL RIQをケーススタディとして、シークエント計算からインターポーラントをどのように計算できるかを示す。 これは、記述論理の文脈内で補間子と定義を計算するための最初のシーケントベースのアプローチである。
  論文  参考訳（メタデータ） (2024-04-24T12:28:27Z)
• 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)
• Sequential measurements, TQFTs, and TQNNs [0.0]
  スケールフリーアーキテクチャで汎用量子情報を実装する新しい手法を提案する。 システムの境界となるホログラフィック画面から導出される測定演算子によって導出される有限ビット列が、観測結果をどのように捉えているかを示す。 解析を拡張して、トポロジカル量子ニューラルネットワーク(TQNN)を開発し、量子ニューラルネットワーク2-複素方程式の関手進化による機械学習を可能にする。
  論文  参考訳（メタデータ） (2022-05-26T06:37:57Z)
• Decimation technique for open quantum systems: a case study with driven-dissipative bosonic chains [62.997667081978825]
  量子系の外部自由度への不可避結合は、散逸(非単体)ダイナミクスをもたらす。 本稿では,グリーン関数の(散逸的な)格子計算に基づいて,これらのシステムに対処する手法を提案する。 本手法のパワーを,複雑性を増大させる駆動散逸型ボゾン鎖のいくつかの例で説明する。
  論文  参考訳（メタデータ） (2022-02-15T19:00:09Z)
• 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)
• 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)

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

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