論文の概要: General Boolean Formula Minimization with QBF Solvers

• arxiv url: http://arxiv.org/abs/2303.06643v1
• Date: Sun, 12 Mar 2023 12:08:58 GMT
• ステータス: 処理完了
• システム内更新日: 2023-03-14 17:35:10.678064
• Title: General Boolean Formula Minimization with QBF Solvers
• Title（参考訳）: QBF解を用いた一般ブール式最小化
• Authors: Eduardo Cal\`o, Jordi Levy
• Abstract要約: 我々は任意の形式で同等の式を得るという問題に興味を持っている。 我々は、最小化アルゴリズムを適用して、元の公式の自然言語翻訳を生成する動機付けをしている。 我々はその問題を解決するための3つの可能な(実践的な)アプローチを分析する。
• 参考スコア（独自算出の注目度）: 4.264192013842096
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The minimization of propositional formulae is a classical problem in logic, whose first algorithms date back at least to the 1950s with the works of Quine and Karnaugh. Most previous work in the area has focused on obtaining minimal, or quasi-minimal, formulae in conjunctive normal form (CNF) or disjunctive normal form (DNF), with applications in hardware design. In this paper, we are interested in the problem of obtaining an equivalent formula in any format, also allowing connectives that are not present in the original formula. We are primarily motivated in applying minimization algorithms to generate natural language translations of the original formula, where using shorter equivalents as input may result in better translations. Recently, Buchfuhrer and Umans have proved that the (decisional version of the) problem is $\Sigma_2^p$-complete. We analyze three possible (practical) approaches to solving the problem. First, using brute force, generating all possible formulae in increasing size and checking if they are equivalent to the original formula by testing all possible variable assignments. Second, generating the Tseitin coding of all the formulae and checking equivalence with the original using a SAT solver. Third, encoding the problem as a Quantified Boolean Formula (QBF), and using a QBF solver. Our results show that the QBF approach largely outperforms the other two.
• Abstract（参考訳）: 命題公式の最小化は論理学における古典的な問題であり、その最初のアルゴリズムは1950年代にクワインとカルノーの業績によって遡る。 この分野のほとんどの以前の研究は、ハードウェア設計に応用された結合正規形(cnf)または分離正規形(dnf)における最小、あるいは準最小の式を得ることに重点を置いてきた。 本稿では,任意の形式で等価な公式を得る問題に関心を持ち,元の公式に存在しない接続性も許容する。 我々は主に、最小化アルゴリズムを適用して元の公式の自然言語翻訳を生成し、入力として短い等価値を使用することでより良い翻訳をもたらす。 近年、buchfuhrer と umans は(決定版)問題は $\sigma_2^p$-complete であることを証明した。 我々はその問題を解決するための3つの可能な(実践的な)アプローチを分析する。 まず、ブルト力を使い、サイズを増加させることで可能な全ての公式を生成し、それが元の公式と等価かどうかを全ての可能な変数割り当てをテストすることによって確認する。 第2に、SATソルバを用いて、すべての公式のTseitin符号を生成し、元の値をチェックする。 第3に、問題を量子ブール式(QBF)として符号化し、QBFソルバを使用する。 以上の結果から,qbfのアプローチは,他の2つを大きく上回っている。

関連論文リスト

• Neural Algorithmic Reasoning with Multiple Correct Solutions [16.045068056647676]
  一部のアプリケーションでは、複数の正しい解を回収することが望ましい。 BF(Bellman-Ford)とDFS(Depth-First Search)の2つの古典的アルゴリズムで本手法を実証する。 この方法は、モデル出力からソリューションをサンプリングし、検証するだけでなく、適切なトレーニングデータを生成することを含む。
  論文  参考訳（メタデータ） (2024-09-11T02:29:53Z)
• Sum-of-Squares inspired Quantum Metaheuristic for Polynomial Optimization with the Hadamard Test and Approximate Amplitude Constraints [76.53316706600717]
  最近提案された量子アルゴリズムarXiv:2206.14999は半定値プログラミング(SDP)に基づいている SDPにインスパイアされた量子アルゴリズムを2乗和に一般化する。 この結果から,本アルゴリズムは大きな問題に適応し,最もよく知られた古典学に近似することが示唆された。
  論文  参考訳（メタデータ） (2024-08-14T19:04:13Z)
• Solving Quantified Boolean Formulas with Few Existential Variables [19.221715574358207]
  QBF問題(Quantified Boolean formula)は、PSPACE完全性のアーキタイプとして一般的に見なされる重要な決定問題である。 本稿では,実数量化変数の数という,単純だが見過ごされたパラメータについて考察する。 次に、有界節長の共役正規形(CNF)のQBFインスタンスに適用可能な新しいFPTアルゴリズムを開発する。
  論文  参考訳（メタデータ） (2024-05-10T14:07:29Z)
• A Framework to Formulate Pathfinding Problems for Quantum Computing [2.9723999564214267]
  パスフィンディング問題に対するQUBOの定式化を自動的に生成するフレームワークを提案する。 手作業による修正作業を必要とせずに簡単に比較できる3つの異なる符号化スキームをサポートしている。 結果として得られるQUBOの定式化は堅牢で効率的であり、それまでの面倒でエラーを起こしやすい改定プロセスを減らす。
  論文  参考訳（メタデータ） (2024-04-16T18:00:06Z)
• Quantum Worst-Case to Average-Case Reductions for All Linear Problems [66.65497337069792]
  量子アルゴリズムにおける最悪のケースと平均ケースの削減を設計する問題について検討する。 量子アルゴリズムの明示的で効率的な変換は、入力のごく一部でのみ正し、全ての入力で正しくなる。
  論文  参考訳（メタデータ） (2022-12-06T22:01:49Z)
• Symmetric Tensor Networks for Generative Modeling and Constrained Combinatorial Optimization [72.41480594026815]
  ポートフォリオ最適化からロジスティクスに至るまで、制約付き最適化問題は業界に多い。 これらの問題の解決における主要な障害の1つは、有効な検索空間を制限する非自明なハード制約の存在である。 本研究では、Ax=bという形の任意の整数値等式制約をU(1)対称ネットワーク(TN)に直接エンコードし、それらの適用性を量子に着想を得た生成モデルとして活用する。
  論文  参考訳（メタデータ） (2022-11-16T18:59:54Z)
• Dynamic programming by polymorphic semiring algebraic shortcut fusion [1.9405875431318445]
  動的プログラミング(動的プログラミング、英: Dynamic Programming、DP)は、難解問題の効率的かつ正確な解法のためのアルゴリズム設計パラダイムである。 本稿では,セミリングに基づくDPアルゴリズムを体系的に導出するための厳密な代数形式について述べる。
  論文  参考訳（メタデータ） (2021-07-05T00:51:02Z)
• Boosting Data Reduction for the Maximum Weight Independent Set Problem Using Increasing Transformations [59.84561168501493]
  最大重み独立集合問題に対する新しい一般化データ削減および変換規則を導入する。 驚くべきことに、これらのいわゆる増進変換は問題を単純化し、還元空間を開き、アルゴリズムの後にさらに小さな既約グラフが得られる。 提案アルゴリズムは, 1つのインスタンスを除くすべての既約グラフを計算し, 従来よりも多くのインスタンスを最適に解き, 最高の最先端解法よりも最大2桁高速に解き, 解法DynWVCやHILSよりも高品質な解を求める。
  論文  参考訳（メタデータ） (2020-08-12T08:52:50Z)
• Strong Generalization and Efficiency in Neural Programs [69.18742158883869]
  本稿では,ニューラルプログラム誘導の枠組みを強く一般化する効率的なアルゴリズムを学習する問題について検討する。 ニューラルネットワークの入力/出力インターフェースを慎重に設計し、模倣することで、任意の入力サイズに対して正しい結果を生成するモデルを学ぶことができる。
  論文  参考訳（メタデータ） (2020-07-07T17:03:02Z)
• Sparse Hashing for Scalable Approximate Model Counting: Theory and Practice [36.8421113576893]
  n 変数上の CNF 式 F が与えられたとき、モデルカウントや #SAT の問題は F の満足な割り当ての数を計算することである。 近年,効率的なアルゴリズム技術開発への取り組みが急増している。
  論文  参考訳（メタデータ） (2020-04-30T11:17:26Z)
• Lagrangian Decomposition for Neural Network Verification [148.0448557991349]
  ニューラルネットワーク検証の基本的なコンポーネントは、出力が取ることのできる値のバウンダリの計算である。 ラグランジアン分解に基づく新しい手法を提案する。 ランニングタイムのごく一部で、既成の解法に匹敵するバウンダリが得られることを示す。
  論文  参考訳（メタデータ） (2020-02-24T17:55:10Z)

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

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