論文の概要: Massively Parallel Continuous Local Search for Hybrid SAT Solving on GPUs

• arxiv url: http://arxiv.org/abs/2308.15020v1
• Date: Tue, 29 Aug 2023 04:50:07 GMT
• ステータス: 処理完了
• システム内更新日: 2023-08-30 15:49:08.117384
• Title: Massively Parallel Continuous Local Search for Hybrid SAT Solving on GPUs
• Title（参考訳）: GPUを用いたハイブリッドSAT解の大規模並列連続探索
• Authors: Yunuo Cen, Zhiwei Zhang, Xuanyao Fong
• Abstract要約: 我々は、勾配駆動連続局所探索に基づく高並列ハイブリッドSATソルバであるFastFourierSATを提案する。 以上の結果から,FastFourierSATはCPU上で実装された以前のプロトタイプの100倍以上の速度で勾配を計算することがわかった。 FastFourierSATは、ほとんどのインスタンスを解決し、より大きなインスタンスで有望なパフォーマンスを示す。
• 参考スコア（独自算出の注目度）: 5.245714076090567
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Although state-of-the-art (SOTA) SAT solvers based on conflict-driven clause learning (CDCL) have achieved remarkable engineering success, their sequential nature limits the parallelism that may be extracted for acceleration on platforms such as the graphics processing unit (GPU). In this work, we propose FastFourierSAT, a highly parallel hybrid SAT solver based on gradient-driven continuous local search (CLS). This is realized by a novel parallel algorithm inspired by the Fast Fourier Transform (FFT)-based convolution for computing the elementary symmetric polynomials (ESPs), which is the major computational task in previous CLS methods. The complexity of our algorithm matches the best previous result. Furthermore, the substantial parallelism inherent in our algorithm can leverage the GPU for acceleration, demonstrating significant improvement over the previous CLS approaches. We also propose to incorporate the restart heuristics in CLS to improve search efficiency. We compare our approach with the SOTA parallel SAT solvers on several benchmarks. Our results show that FastFourierSAT computes the gradient 100+ times faster than previous prototypes implemented on CPU. Moreover, FastFourierSAT solves most instances and demonstrates promising performance on larger-size instances.
• Abstract（参考訳）: コンフリクト駆動型節学習(CDCL)に基づく最新技術(SOTA)SATソルバは、優れたエンジニアリング成功を達成しているが、そのシーケンシャルな性質は、グラフィクス処理ユニット(GPU)のようなプラットフォーム上でのアクセラレーションのために抽出できる並列性を制限する。 本研究では,勾配駆動型連続局所探索(CLS)に基づく高並列ハイブリッドSATソルバであるFastFourierSATを提案する。 これは、従来の cls 法の主要な計算課題である基本対称多項式(英語版)(esps)を計算するための高速フーリエ変換(fft)に基づく畳み込みに触発された新しい並列アルゴリズムによって実現される。 アルゴリズムの複雑さは、最も古い結果と一致します。 さらに,本アルゴリズムが生み出す並列性はgpuをアクセラレーションに活用し,従来のcls法に比べて大幅に改善する。 また,再起動ヒューリスティックスをCRSに組み込んで探索効率を向上させることを提案する。 いくつかのベンチマークでSOTA並列SATソルバとの比較を行った。 この結果から,FastFourierSATはCPU上で実装されたプロトタイプの100倍以上の速度で勾配を計算することがわかった。 さらにFastFourierSATは、ほとんどのインスタンスを解決し、より大きなインスタンスで有望なパフォーマンスを示す。

関連論文リスト

• Iterative quantum optimization of spin glass problems with rapidly oscillating transverse fields [0.0]
  IST-SAT(Iterative Symphonic Tunneling for Satisfiability Problem)と呼ばれる新しい反復量子アルゴリズムを導入する。 IST-SATは高周波振動横場を用いた量子スピンガラス最適化問題を解く。
  論文  参考訳（メタデータ） (2024-08-13T02:09:30Z)
• Sparsity-Constraint Optimization via Splicing Iteration [1.3622424109977902]
  我々は sPlicing itEration (SCOPE) を用いたスペーサリティ制約最適化アルゴリズムを開発した。 SCOPEはパラメータをチューニングせずに効率的に収束する。 SCOPEを用いて2次最適化を解き、スパース分類器を学習し、バイナリ変数のスパースマルコフネットワークを復元する。 C++実装に基づいたオープンソースのPythonパッケージskscopeがGitHubで公開されている。
  論文  参考訳（メタデータ） (2024-06-17T18:34:51Z)
• torchmSAT: A GPU-Accelerated Approximation To The Maximum Satisfiability Problem [1.5850859526672516]
  最大満足度問題(MaxSAT)の解を近似できる単一の微分可能関数を導出する。 我々は,我々の微分可能な関数をモデル化する新しいニューラルネットワークアーキテクチャを提案し,バックプロパゲーションを用いてMaxSATを段階的に解く。
  論文  参考訳（メタデータ） (2024-02-06T02:33:00Z)
• Fast, Scalable, Warm-Start Semidefinite Programming with Spectral Bundling and Sketching [53.91395791840179]
  我々は、大規模なSDPを解くための、証明可能な正確で高速でスケーラブルなアルゴリズムであるUnified Spectral Bundling with Sketching (USBS)を提案する。 USBSは、20億以上の決定変数を持つインスタンス上で、最先端のスケーラブルなSDP解決器よりも500倍のスピードアップを提供する。
  論文  参考訳（メタデータ） (2023-12-19T02:27:22Z)
• Solving MaxSAT with Matrix Multiplication [15.349236934751897]
  本稿では,GPUやTPUなどのニューラルネットワークアクセラレータ上での動作に特化して設計されたMaxSAT(Maximum Satisfiability)アルゴリズムを提案する。 我々のアプローチはRbmSATと呼ばれ、MaxSATのアルゴリズム・ハードウェア共同設計における新しい設計点である。 我々は、2018年から2021年までの毎年恒例のMaxSAT評価不完全不完全トラックの課題事例のサブセットについて、時間的結果を提示した。
  論文  参考訳（メタデータ） (2023-11-01T14:46:46Z)
• Stochastic Optimization for Non-convex Problem with Inexact Hessian Matrix, Gradient, and Function [99.31457740916815]
  信頼領域(TR)と立方体を用いた適応正則化は、非常に魅力的な理論的性質を持つことが証明されている。 TR法とARC法はヘッセン関数,勾配関数,関数値の非コンパクトな計算を同時に行うことができることを示す。
  論文  参考訳（メタデータ） (2023-10-18T10:29:58Z)
• High Performance Computing Applied to Logistic Regression: A CPU and GPU Implementation Comparison [0.0]
  汎用GPUによるロジスティック回帰(LR)の並列バージョンを提案する。 我々の実装は、X. Zouらによって提案された並列なグラディエントDescent Logistic Regressionアルゴリズムの直接変換である。 本手法は,画像認識,スパム検出,不正検出などのリアルタイム予測に特に有用である。
  論文  参考訳（メタデータ） (2023-08-19T14:49:37Z)
• Matching Pursuit Based Scheduling for Over-the-Air Federated Learning [67.59503935237676]
  本稿では,フェデレートラーニング手法を用いて,オーバー・ザ・エアラーニングのための低複雑さデバイススケジューリングアルゴリズムのクラスを開発する。 最先端の提案方式と比較すると,提案方式は極めて低効率なシステムである。 提案手法の有効性は,CIFARデータセットを用いた実験により確認した。
  論文  参考訳（メタデータ） (2022-06-14T08:14:14Z)
• AsySQN: Faster Vertical Federated Learning Algorithms with Better Computation Resource Utilization [159.75564904944707]
  垂直連合学習(VFL)のための非同期準ニュートン(AsySQN)フレームワークを提案する。 提案アルゴリズムは、逆ヘッセン行列を明示的に計算することなく、近似して降下ステップをスケールする。 本稿では,非同期計算を採用することにより,計算資源の有効利用が期待できることを示す。
  論文  参考訳（メタデータ） (2021-09-26T07:56:10Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
  論文  参考訳（メタデータ） (2021-07-15T04:47:35Z)
• Accelerating Feedforward Computation via Parallel Nonlinear Equation Solving [106.63673243937492]
  ニューラルネットワークの評価や自己回帰モデルからのサンプリングなどのフィードフォワード計算は、機械学習においてユビキタスである。 本稿では,非線形方程式の解法としてフィードフォワード計算の課題を定式化し,ジャコビ・ガウス・シーデル固定点法とハイブリッド法を用いて解を求める。 提案手法は, 並列化可能な繰り返し回数の削減(あるいは等値化)により, 元のフィードフォワード計算と全く同じ値が与えられることを保証し, 十分な並列化計算能力を付与する。
  論文  参考訳（メタデータ） (2020-02-10T10:11:31Z)

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

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