論文の概要: Strong Structural Bounds for MaxSAT: The Fine Details of Using Neuromorphic and Quantum Hardware Accelerators
- arxiv url: http://arxiv.org/abs/2412.10289v1
- Date: Fri, 13 Dec 2024 17:18:08 GMT
- ステータス: 翻訳完了
- システム内更新日: 2024-12-18 13:57:22.912725
- Title: Strong Structural Bounds for MaxSAT: The Fine Details of Using Neuromorphic and Quantum Hardware Accelerators
- Title(参考訳): MaxSATの強構造境界:ニューロモルフィック・量子ハードウェア加速器の細部
- Authors: Max Bannach, Jai Grover, Markus Hecher,
- Abstract要約: 量子アニールやニューロモルフィックチップのようなハードウェアアクセラレーターは、ハミルトンの基底状態を見つけることができる。
それまでの研究は、構文的・構造的特性ではなく、エンコーディングのサイズにのみ関係していた。
我々は、MaxSAT、Max2SAT、およびハードウェアアクセラレータの基盤となる2次非制約バイナリ最適化問題(QUBO)の間の構造認識の低減を確立する。
- 参考スコア(独自算出の注目度): 16.324368802296526
- License:
- Abstract: Hardware accelerators like quantum annealers or neuromorphic chips are capable of finding the ground state of a Hamiltonian. A promising route in utilizing these devices is via methods from automated reasoning: The problem at hand is first encoded into MaxSAT; then MaxSAT is reduced to Max2SAT; and finally, Max2SAT is translated into a Hamiltonian. It was observed that different encodings can dramatically affect the efficiency of the hardware accelerators. Yet, previous studies were only concerned with the size of the encodings rather than with syntactic or structural properties. We establish structure-aware reductions between MaxSAT, Max2SAT, and the quadratic unconstrained binary optimization problem (QUBO) that underlies such hardware accelerators. All these problems turn out to be equivalent under linear-time, treewidth-preserving reductions. As a consequence, we obtain tight lower bounds under ETH and SETH for Max2SAT and QUBO, as well as a new time-optimal fixed-parameter algorithm for QUBO. While our results are tight up to a constant additive factor for the primal treewidth, we require a constant multiplicative factor for the incidence treewidth. To close the emerging gap, we supplement our results with novel time-optimal algorithms for fragments of MaxSAT based on model counting.
- Abstract(参考訳): 量子アニールやニューロモルフィックチップのようなハードウェアアクセラレーターは、ハミルトンの基底状態を見つけることができる。
問題はまずMaxSATにエンコードされ、その後MaxSATはMax2SATに還元され、最後にMax2SATはハミルトン語に変換される。
異なるエンコーディングがハードウェアアクセラレーターの効率に劇的に影響を与えることが観察された。
しかし、以前の研究では、構文的あるいは構造的特性ではなく、エンコーディングのサイズにのみ関係していた。
我々は、MaxSAT、Max2SAT、およびハードウェアアクセラレータの基盤となる2次非制約バイナリ最適化問題(QUBO)の間の構造認識の低減を確立する。
これらの問題はすべて、線形時間木幅保存還元の下で等価であることが判明した。
その結果,Max2SAT と QUBO の ETH と SETH の下限は厳密であり,QUBO の新しい時間最適固定パラメータアルゴリズムが得られた。
本研究の結果は, 主樹幅に一定の添加因子が作用する一方で, 入射木幅に一定の乗算因子が要求される。
出現するギャップを埋めるために、モデルカウントに基づくMaxSATのフラグメントに対する新しい時間最適化アルゴリズムで結果を補足する。
関連論文リスト
- MaxSAT decoders for arbitrary CSS codes [2.3895981099137535]
任意の幾何およびパリティチェック重みを持つCSS符号の量子極大問題をMaxSAT問題にマップする方法を示す。
我々のデコーダはASICやFPGAでさらに並列化や実装が可能であり、数桁のさらなる高速化が期待できる。
論文 参考訳(メタデータ) (2024-10-02T15:45:05Z) - Solving MaxSAT with Matrix Multiplication [15.349236934751897]
本稿では,GPUやTPUなどのニューラルネットワークアクセラレータ上での動作に特化して設計されたMaxSAT(Maximum Satisfiability)アルゴリズムを提案する。
我々のアプローチはRbmSATと呼ばれ、MaxSATのアルゴリズム・ハードウェア共同設計における新しい設計点である。
我々は、2018年から2021年までの毎年恒例のMaxSAT評価不完全不完全トラックの課題事例のサブセットについて、時間的結果を提示した。
論文 参考訳(メタデータ) (2023-11-01T14:46:46Z) - Improving Dual-Encoder Training through Dynamic Indexes for Negative
Mining [61.09807522366773]
本稿では,ソフトマックスを証明可能な境界で近似し,木を動的に維持するアルゴリズムを提案する。
我々は,2000万以上のターゲットを持つデータセットについて検討し,オラクル・ブルート力負の鉱業に関して,誤差を半分に削減した。
論文 参考訳(メタデータ) (2023-03-27T15:18:32Z) - Towards Tackling MaxSAT by Combining Nested Monte Carlo with Local
Search [10.70006528984961]
UCTMAXSAT上でのアルゴリズム的バリエーションを2つ紹介する。
まず、Nested Monte Carlo Searchアルゴリズムにインスパイアされた木探索のネストは、ベンチマークのほとんどのインスタンスタイプに有効である。
第二に、SLSの静的フリップ制限を用いることで、理想的な予算はインスタンスサイズに大きく依存し、動的に設定することを提案する。
論文 参考訳(メタデータ) (2023-02-26T03:37:26Z) - Softmax-free Linear Transformers [90.83157268265654]
視覚変換器(ViT)は、視覚知覚タスクの最先端を推し進めている。
既存の手法は理論的に欠陥があるか、視覚認識に経験的に効果がないかのいずれかである。
我々はSoftmax-Free Transformers (SOFT) のファミリーを提案する。
論文 参考訳(メタデータ) (2022-07-05T03:08:27Z) - DPMS: An ADD-Based Symbolic Approach for Generalized MaxSAT Solving [45.21499915442282]
本稿では,ハイブリッド制約を用いた一般化MaxSAT問題の解法について,新しい動的プログラミング手法を提案する。
我々の汎用フレームワークは、MaxSAT、Min-MaxSAT、MinSATといったCNF-MaxSATの多くの一般化をハイブリッド制約で認めている。
実験の結果、DPMSは様々な手法に基づく他のアルゴリズムがすべて失敗し、特定の問題を迅速に解決できることがわかった。
論文 参考訳(メタデータ) (2022-05-08T00:31:53Z) - Transformer-based Machine Learning for Fast SAT Solvers and Logic
Synthesis [63.53283025435107]
CNFベースのSATとMaxSATは論理合成と検証システムの中心である。
そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
論文 参考訳(メタデータ) (2021-07-15T04:47:35Z) - Incomplete MaxSAT Approaches for Combinatorial Testing [0.0]
本稿では,最小長の制約付き混合被覆アレイを構築するためのSAT(Satifiability)に基づくアプローチを提案する。
この問題はシステム障害検出のためのコンビネータテストの中心である。
論文 参考訳(メタデータ) (2021-05-26T14:00:56Z) - Improved Branch and Bound for Neural Network Verification via Lagrangian
Decomposition [161.09660864941603]
ニューラルネットワークの入出力特性を公式に証明するためのブランチとバウンド(BaB)アルゴリズムのスケーラビリティを改善します。
活性化に基づく新しい分岐戦略とBaBフレームワークであるブランチとデュアルネットワーク境界(BaDNB)を提案する。
BaDNBは、従来の完全検証システムを大きなマージンで上回り、対数特性で平均検証時間を最大50倍に削減した。
論文 参考訳(メタデータ) (2021-04-14T09:22:42Z) - Lower Bounds and Accelerated Algorithms for Bilevel Optimization [62.192297758346484]
バイレベル最適化は、最近の機械学習問題に広く応用されているため、近年、関心が高まりつつある。
結果がminimaxアプリケーションよりも難しいことを示します。
論文 参考訳(メタデータ) (2021-02-07T21:46:29Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。