論文の概要: Solving Quantified Boolean Formulas with Few Existential Variables
- arxiv url: http://arxiv.org/abs/2405.06485v1
- Date: Fri, 10 May 2024 14:07:29 GMT
- ステータス: 処理完了
- システム内更新日: 2024-05-13 15:38:11.196296
- Title: Solving Quantified Boolean Formulas with Few Existential Variables
- Title（参考訳）: 存在変数の少ない量化ブール方程式の解法
- Authors: Leif Eriksson, Victor Lagerkvist, George Osipov, Sebastian Ordyniak, Fahad Panolan, Mateusz Rychlicki,
- Abstract要約: QBF問題(Quantified Boolean formula)は、PSPACE完全性のアーキタイプとして一般的に見なされる重要な決定問題である。
本稿では,実数量化変数の数という,単純だが見過ごされたパラメータについて考察する。
次に、有界節長の共役正規形(CNF)のQBFインスタンスに適用可能な新しいFPTアルゴリズムを開発する。
- 参考スコア（独自算出の注目度）: 19.221715574358207
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: The quantified Boolean formula (QBF) problem is an important decision problem generally viewed as the archetype for PSPACE-completeness. Many problems of central interest in AI are in general not included in NP, e.g., planning, model checking, and non-monotonic reasoning, and for such problems QBF has successfully been used as a modelling tool. However, solvers for QBF are not as advanced as state of the art SAT solvers, which has prevented QBF from becoming a universal modelling language for PSPACE-complete problems. A theoretical explanation is that QBF (as well as many other PSPACE-complete problems) lacks natural parameters} guaranteeing fixed-parameter tractability (FPT). In this paper we tackle this problem and consider a simple but overlooked parameter: the number of existentially quantified variables. This natural parameter is virtually unexplored in the literature which one might find surprising given the general scarcity of FPT algorithms for QBF. Via this parameterization we then develop a novel FPT algorithm applicable to QBF instances in conjunctive normal form (CNF) of bounded clause length. We complement this by a W[1]-hardness result for QBF in CNF of unbounded clause length as well as sharper lower bounds for the bounded arity case under the (strong) exponential-time hypothesis.
- Abstract（参考訳）: QBF問題(Quantified Boolean formula)は、PSPACE完全性のアーキタイプとして一般的に見なされる重要な決定問題である。
AIに中心的な関心を持つ多くの問題は、一般的にNP、プランニング、モデルチェック、非モノトニック推論に含まれておらず、そのような問題に対してQBFはモデリングツールとしてうまく使われてきた。
しかし、QBFの解法は最先端のSATソルバほど進まないため、PSPACE完全問題の普遍的なモデリング言語にはならない。
理論的な説明として、QBF(他の多くのPSPACE完全問題と同様に)は、固定パラメータトラクタビリティ(FPT)を保証する自然パラメータを欠いている。
本稿では,この問題に対処し,実数量化変数の数という,単純だが見過ごされたパラメータについて考察する。
この自然パラメータは、QBFに対するFPTアルゴリズムの全般的不足を考えると、意外なことに文献ではほとんど探索されていない。
このパラメータ化により、有界節長の共役正規形(CNF)のQBFインスタンスに適用可能な新しいFPTアルゴリズムを開発する。
非有界節長のCNFにおけるQBFのW[1]-ハードネス結果と、(強い)指数時間仮説の下での有界アーニティケースのよりシャープな下界を補完する。
関連論文リスト
- Learning Solution-Aware Transformers for Efficiently Solving Quadratic Assignment Problem [27.33966993065248]
本研究は,2次割当て問題(QAP)を効率的に解くための学習ベースソリューションに焦点を当てる。
QAPに関する現在の研究は、限られた規模と非効率性に悩まされている。
そこで本研究では,QAPの学習と改善のカテゴリにおける第1の解法を提案する。
論文 参考訳（メタデータ） (2024-06-14T10:15:03Z) - Reverse em-problem based on Bregman divergence and its application to classical and quantum information theory [53.64687146666141]
近年,反復を必要とせずにチャネル容量を計算できる解析手法が提案されている。
トヨタが提案した逆のEm-problemに注意を向けます。
逆の Em-problem の非定型式を導出する。
論文 参考訳（メタデータ） (2024-03-14T10:20:28Z) - Where the Really Hard Quadratic Assignment Problems Are: the QAP-SAT
instances [0.0]
二次割当問題 (QAP) は、進化的計算最適化の分野における主要な領域の1つである。
本稿では,QAPの相転移について検討し,問題の計算複雑性と充足可能性の劇的な変化と説明できる。
論文 参考訳（メタデータ） (2024-03-05T08:56:30Z) - General Boolean Formula Minimization with QBF Solvers [4.264192013842096]
我々は任意の形式で同等の式を得るという問題に興味を持っている。
我々は、最小化アルゴリズムを適用して、元の公式の自然言語翻訳を生成する動機付けをしている。
我々はその問題を解決するための3つの可能な(実践的な)アプローチを分析する。
論文 参考訳（メタデータ） (2023-03-12T12:08:58Z) - Symmetric Tensor Networks for Generative Modeling and Constrained
Combinatorial Optimization [72.41480594026815]
ポートフォリオ最適化からロジスティクスに至るまで、制約付き最適化問題は業界に多い。
これらの問題の解決における主要な障害の1つは、有効な検索空間を制限する非自明なハード制約の存在である。
本研究では、Ax=bという形の任意の整数値等式制約をU(1)対称ネットワーク(TN)に直接エンコードし、それらの適用性を量子に着想を得た生成モデルとして活用する。
論文 参考訳（メタデータ） (2022-11-16T18:59:54Z) - Complexity-Theoretic Limitations on Quantum Algorithms for Topological
Data Analysis [59.545114016224254]
トポロジカルデータ解析のための量子アルゴリズムは、古典的手法よりも指数関数的に有利である。
我々は、量子コンピュータにおいても、TDA(ベッチ数の推定)の中心的なタスクが難解であることを示します。
我々は、入力データが単純さの仕様として与えられると、指数的量子優位性を取り戻すことができると論じる。
論文 参考訳（メタデータ） (2022-09-28T17:53:25Z) - Optimal Solutions for Joint Beamforming and Antenna Selection: From
Branch and Bound to Machine Learning [47.10315221141495]
本研究は、不完全なチャネル状態情報(CSI)の下で、継手ビームフォーミング(BF)とアンテナ選択(AS)の問題およびロバストビームフォーミング(RBF)バージョンを再検討する。
この研究の主な貢献は3つある。まず、関心事の問題を解決する効果的な分岐と境界(B&B)フレームワークを提案する。
第二に、潜在的にコストのかかるB&Bアルゴリズムを高速化するために、B&B検索ツリーの中間状態を省略する機械学習(ML)ベースのスキームが提案されている。
論文 参考訳（メタデータ） (2022-06-11T17:43:02Z) - Hyperparameter-free deep active learning for regression problems via
query synthesis [5.572747615014008]
回帰問題に対する最初のDALクエリ合成手法を提案する。
我々は、最近提案されたニューラルアジョイント(NA)ソルバを用いて、連続入力領域のポイントを効率的に見つける。
NA-QBCは,各ベンチマーク問題に対するランダムサンプリングよりも平均性能がよいことがわかった。
論文 参考訳（メタデータ） (2022-01-29T18:41:08Z) - TAT-QA: A Question Answering Benchmark on a Hybrid of Tabular and
Textual Content in Finance [71.76018597965378]
TAT-QAと呼ばれるタブラデータとテクスチャデータの両方を含む新しい大規模な質問応答データセットを構築します。
本稿では,テーブルとテキストの両方を推論可能な新しいQAモデルであるTAGOPを提案する。
論文 参考訳（メタデータ） (2021-05-17T06:12:06Z) - Q-Match: Iterative Shape Matching via Quantum Annealing [64.74942589569596]
形状対応を見つけることは、NP-hard quadratic assignment problem (QAP)として定式化できる。
本稿では,アルファ拡大アルゴリズムに触発されたQAPの反復量子法Q-Matchを提案する。
Q-Match は、実世界の問題にスケールできるような長文対応のサブセットにおいて、反復的に形状マッチング問題に適用できる。
論文 参考訳（メタデータ） (2021-05-06T17:59:38Z) - Bayesian Probabilistic Numerical Integration with Tree-Based Models [5.353941016039247]
BQはベイズ方式で数値積分問題を解く方法である。
BART-Int. BART はチューニングが容易で、不連続関数に適している。
論文 参考訳（メタデータ） (2020-06-09T16:04:00Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。