論文の概要: Solving MaxSAT with Matrix Multiplication

• arxiv url: http://arxiv.org/abs/2311.02101v1
• Date: Wed, 1 Nov 2023 14:46:46 GMT
• ステータス: 処理完了
• システム内更新日: 2023-11-12 19:45:52.720115
• Title: Solving MaxSAT with Matrix Multiplication
• Title（参考訳）: 行列乗算によるMaxSATの解法
• Authors: David Warde-Farley, Vinod Nair, Yujia Li, Ivan Lobov, Felix Gimeno, Simon Osindero
• Abstract要約: 本稿では,GPUやTPUなどのニューラルネットワークアクセラレータ上での動作に特化して設計されたMaxSAT(Maximum Satisfiability)アルゴリズムを提案する。 我々のアプローチはRbmSATと呼ばれ、MaxSATのアルゴリズム・ハードウェア共同設計における新しい設計点である。 我々は、2018年から2021年までの毎年恒例のMaxSAT評価不完全不完全トラックの課題事例のサブセットについて、時間的結果を提示した。
• 参考スコア（独自算出の注目度）: 15.349236934751897
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We propose an incomplete algorithm for Maximum Satisfiability (MaxSAT) specifically designed to run on neural network accelerators such as GPUs and TPUs. Given a MaxSAT problem instance in conjunctive normal form, our procedure constructs a Restricted Boltzmann Machine (RBM) with an equilibrium distribution wherein the probability of a Boolean assignment is exponential in the number of clauses it satisfies. Block Gibbs sampling is used to stochastically search the space of assignments with parallel Markov chains. Since matrix multiplication is the main computational primitive for block Gibbs sampling in an RBM, our approach leads to an elegantly simple algorithm (40 lines of JAX) well-suited for neural network accelerators. Theoretical results about RBMs guarantee that the required number of visible and hidden units of the RBM scale only linearly with the number of variables and constant-sized clauses in the MaxSAT instance, ensuring that the computational cost of a Gibbs step scales reasonably with the instance size. Search throughput can be increased by batching parallel chains within a single accelerator as well as by distributing them across multiple accelerators. As a further enhancement, a heuristic based on unit propagation running on CPU is periodically applied to the sampled assignments. Our approach, which we term RbmSAT, is a new design point in the algorithm-hardware co-design space for MaxSAT. We present timed results on a subset of problem instances from the annual MaxSAT Evaluation's Incomplete Unweighted Track for the years 2018 to 2021. When allotted the same running time and CPU compute budget (but no TPUs), RbmSAT outperforms other participating solvers on problems drawn from three out of the four years' competitions. Given the same running time on a TPU cluster for which RbmSAT is uniquely designed, it outperforms all solvers on problems drawn from all four years.
• Abstract（参考訳）: 本稿では,GPUやTPUなどのニューラルネットワークアクセラレータ上での動作に特化して設計されたMaxSAT(Maximum Satisfiability)のための不完全アルゴリズムを提案する。 直交正規形式のMaxSAT問題のインスタンスが与えられた場合、この手順は平衡分布を持つ制限ボルツマンマシン(RBM)を構築し、ブール代入の確率は満足する節数で指数関数的である。 ブロックギブスサンプリングは、並列マルコフ連鎖による代入空間を確率的に探索するために用いられる。 行列の乗算はrbmにおけるブロックギブスサンプリングの主要な計算プリミティブであるため、本手法はニューラルネットワーク加速器に適したエレガントにシンプルなアルゴリズム(40行のjax)を導出する。 RBMの理論的結果は、RBMの必要な可視単位と隠蔽単位の数が、MaxSATインスタンスの変数数と定数サイズの節数にのみ線形にスケールすることを保証し、ギブスステップの計算コストがインスタンスサイズと合理的にスケールすることを保証する。 検索スループットは、1つのアクセラレータ内で並列チェーンをバッチ化し、複数のアクセラレータに分散することで向上することができる。 さらに、CPU上で実行されている単位伝搬に基づくヒューリスティックが、サンプリングされた割り当てに定期的に適用される。 我々のアプローチはRbmSATと呼ばれ、MaxSATのアルゴリズム・ハードウェア共同設計における新しい設計点である。 我々は,2018年から2021年までの年次maxsat評価の不完全な非重み付けトラックから問題インスタンスのサブセットをタイムド結果として提示する。 同じ実行時間とCPUの計算予算(TPUは含まれていない)を割り当てると、RbmSATは4年のうち3つから引き出された問題で他の参加者よりも優れていた。 rbmsatが独特に設計されているtpuクラスタ上で同じ実行時間を考えると、4年間にわたって引き起こされた問題の解法を全て上回る。

関連論文リスト

• torchmSAT: A GPU-Accelerated Approximation To The Maximum Satisfiability Problem [1.5850859526672516]
  最大満足度問題(MaxSAT)の解を近似できる単一の微分可能関数を導出する。 我々は,我々の微分可能な関数をモデル化する新しいニューラルネットワークアーキテクチャを提案し,バックプロパゲーションを用いてMaxSATを段階的に解く。
  論文  参考訳（メタデータ） (2024-02-06T02:33:00Z)
• Grover-QAOA for 3-SAT: Quadratic Speedup, Fair-Sampling, and Parameter Clustering [6.86850788361785]
  本研究では,Grover Quantum Approximate Optimization Algorithm (G-QAOA) の2次高速化の数値的証拠を示す。 G-QAOAはGroverのアルゴリズムよりもリソース集約性が低く、3-SATやMax-SATに適応しやすい。 また、小さなインスタンスに対してIonQ Aria量子コンピュータのG-QAOAの利点を観察し、現在のハードウェアが全てのソリューションを決定・サンプリングするのに十分であることを示した。
  論文  参考訳（メタデータ） (2024-02-04T19:01:27Z)
• Massively Parallel Continuous Local Search for Hybrid SAT Solving on GPUs [5.245714076090567]
  我々は、勾配駆動連続局所探索に基づく高並列ハイブリッドSATソルバであるFastFourierSATを提案する。 以上の結果から,FastFourierSATはCPU上で実装された以前のプロトタイプの100倍以上の速度で勾配を計算することがわかった。 FastFourierSATは、ほとんどのインスタンスを解決し、より大きなインスタンスで有望なパフォーマンスを示す。
  論文  参考訳（メタデータ） (2023-08-29T04:50:07Z)
• Approximating a RUM from Distributions on k-Slates [88.32814292632675]
  与えられた分布を平均で最もよく近似するRUMを求める一般化時間アルゴリズムを求める。 我々の理論的結果は、実世界のデータセットに効果的でスケール可能なものを得るという、実践的な結果も得られます。
  論文  参考訳（メタデータ） (2023-05-22T17:43:34Z)
• 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)
• 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)
• Unfolding Projection-free SDP Relaxation of Binary Graph Classifier via GDPA Linearization [59.87663954467815]
  アルゴリズムの展開は、モデルベースのアルゴリズムの各イテレーションをニューラルネットワーク層として実装することにより、解釈可能で類似のニューラルネットワークアーキテクチャを生成する。 本稿では、Gershgorin disc perfect alignment (GDPA)と呼ばれる最近の線形代数定理を利用して、二進グラフの半定値プログラミング緩和(SDR)のためのプロジェクションフリーアルゴリズムをアンロールする。 実験結果から,我々の未学習ネットワークは純粋モデルベースグラフ分類器よりも優れ,純粋データ駆動ネットワークに匹敵する性能を示したが,パラメータははるかに少なかった。
  論文  参考訳（メタデータ） (2021-09-10T07:01:15Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
  論文  参考訳（メタデータ） (2021-07-15T04:47:35Z)
• Computationally efficient sparse clustering [67.95910835079825]
  我々はPCAに基づく新しいクラスタリングアルゴリズムの有限サンプル解析を行う。 ここでは,ミニマックス最適誤クラスタ化率を,体制$|theta infty$で達成することを示す。
  論文  参考訳（メタデータ） (2020-05-21T17:51:30Z)
• MPLP++: Fast, Parallel Dual Block-Coordinate Ascent for Dense Graphical Models [96.1052289276254]
  この研究は、人気のあるDual Block-Coordinate Ascent原則に基づく新しいMAP-solverを導入している。 驚いたことに、性能の低い解法に小さな変更を加えることで、既存の解法を大きなマージンで大幅に上回る新しい解法MPLP++を導出します。
  論文  参考訳（メタデータ） (2020-04-16T16:20:53Z)

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

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