論文の概要: TurboSAT: Gradient-Guided Boolean Satisfiability Accelerated on GPU-CPU Hybrid System

• arxiv url: http://arxiv.org/abs/2511.07737v1
• Date: Wed, 12 Nov 2025 01:14:00 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-11-12 20:17:03.452864
• Title: TurboSAT: Gradient-Guided Boolean Satisfiability Accelerated on GPU-CPU Hybrid System
• Title（参考訳）: TurboSAT: GPU-CPUハイブリッドシステム上でのグラディエントガイドによるブール満足度向上
• Authors: Steve Dai, Cunxi Yu, Kalyan Krishnamani, Brucek Khailany,
• Abstract要約: 最先端の満足度解決者は、本質的に競合駆動型検索アルゴリズムに大きく依存している。 ニューラルネットワークのトレーニングに着想を得て、SAT問題を二項行列行列行列乗法層として定式化する。 我々は、並列微分可能最適化とシーケンシャルサーチの長所を組み合わせて、ハイブリッドGPU-CPUシステムでSATを高速化する。
• 参考スコア（独自算出の注目度）: 7.530665570222049
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: While accelerated computing has transformed many domains of computing, its impact on logical reasoning, specifically Boolean satisfiability (SAT), remains limited. State-of-the-art SAT solvers rely heavily on inherently sequential conflict-driven search algorithms that offer powerful heuristics but limit the amount of parallelism that could otherwise enable significantly more scalable SAT solving. Inspired by neural network training, we formulate the SAT problem as a binarized matrix-matrix multiplication layer that could be optimized using a differentiable objective function. Enabled by this encoding, we combine the strengths of parallel differentiable optimization and sequential search to accelerate SAT on a hybrid GPU-CPU system. In this system, the GPUs leverage parallel differentiable solving to rapidly evaluate SAT clauses and use gradients to stochastically explore the solution space and optimize variable assignments. Promising partial assignments generated by the GPUs are post-processed on many CPU threads which exploit conflict-driven sequential search to further traverse the solution subspaces and identify complete assignments. Prototyping the hybrid solver on an NVIDIA DGX GB200 node, our solver achieves runtime speedups up to over 200x when compared to a state-of-the-art CPU-based solver on public satisfiable benchmark problems from the SAT Competition.
• Abstract（参考訳）: 加速コンピューティングは多くの分野のコンピューティングに変化をもたらしたが、論理的推論、特にブール満足度(SAT)への影響は依然として限られている。 最先端のSATソルバは、強力なヒューリスティックを提供するが、よりスケーラブルなSATソルバを実現するために並列性を制限する、本質的に競合駆動型検索アルゴリズムに大きく依存している。 ニューラルネットワークのトレーニングに触発されて、SAT問題を二項行列行列行列乗法層として定式化し、微分可能な目的関数を用いて最適化する。 この符号化により、並列微分可能最適化の長所と逐次探索の長所を組み合わせて、ハイブリッドGPU-CPUシステム上でSATを高速化する。 このシステムでは、並列微分可能解を用いてSAT節を高速に評価し、勾配を用いて解空間を確率論的に探索し、変数割り当てを最適化する。 GPUが生成した部分代入のプロットは多くのCPUスレッドで後処理され、コンフリクト駆動シーケンシャルサーチを利用して、ソリューションサブスペースをさらにトラバースし、完全な代入を識別する。 NVIDIA DGX GB200ノード上でハイブリッド・ソルバをプロトタイピングすることで,SATコンペティションのベンチマーク問題に対する最先端CPUベース・ソルバと比較して,ランタイム・スピードアップを最大200倍に向上させる。

関連論文リスト

• Deeply Optimizing the SAT Solver for the IC3 Algorithm [0.23749905164931204]
  観測結果に基づいて,IC3におけるSATソルバの最適化について述べる。 バイナリヒープをバケットに置き換えて、一定時間操作を実現しています。 我々はこれらの最適化を統合した新しい軽量CDCL SATソルバであるGipSATを開発した。
  論文  参考訳（メタデータ） (2025-01-24T12:40:43Z)
• GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection [45.222591894755105]
  インスタンスの3部グラフ表現に基づくSATソルバ自動選択のための新しいアプローチであるGraSSを提案する。 我々は、新しいノードの特徴設計のようなドメイン固有の決定でグラフ表現を豊かにします。 生の表現とドメイン固有の選択の組み合わせが実行時の改善につながることを実証する。
  論文  参考訳（メタデータ） (2024-05-17T18:00:50Z)
• torchmSAT: A GPU-Accelerated Approximation To The Maximum Satisfiability Problem [1.5850859526672516]
  最大満足度問題(MaxSAT)の解を近似できる単一の微分可能関数を導出する。 我々は,我々の微分可能な関数をモデル化する新しいニューラルネットワークアーキテクチャを提案し,バックプロパゲーションを用いてMaxSATを段階的に解く。
  論文  参考訳（メタデータ） (2024-02-06T02:33:00Z)
• Massively Parallel Continuous Local Search for Hybrid SAT Solving on GPUs [5.245714076090567]
  我々は、勾配駆動連続局所探索に基づく高並列ハイブリッドSATソルバであるFastFourierSATを提案する。 以上の結果から,FastFourierSATはCPU上で実装された以前のプロトタイプの100倍以上の速度で勾配を計算することがわかった。 FastFourierSATは、ほとんどのインスタンスを解決し、より大きなインスタンスで有望なパフォーマンスを示す。
  論文  参考訳（メタデータ） (2023-08-29T04:50:07Z)
• A Parallel and Distributed Quantum SAT Solver Based on Entanglement and Quantum Teleportation [1.5201992393140886]
  並列量子SATソルバは,線形時間 O(m) から定数時間 O(1) までの繰り返しの時間複雑性を,余分な絡み合った量子ビットを用いて低減する。 我々は、我々のアプローチの正しさを証明し、シミュレーションでそれらを実証した。
  論文  参考訳（メタデータ） (2023-08-07T06:52:06Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
  論文  参考訳（メタデータ） (2021-07-15T04:47:35Z)
• Resource Allocation in Multi-armed Bandit Exploration: Overcoming Sublinear Scaling with Adaptive Parallelism [107.48538091418412]
  腕の引っ張りに様々な量の資源を割り当てることができる分割可能な資源にアクセス可能な場合,マルチアームの帯状地における探索について検討する。 特に、分散コンピューティングリソースの割り当てに重点を置いており、プル毎により多くのリソースを割り当てることで、結果をより早く得ることができます。
  論文  参考訳（メタデータ） (2020-10-31T18:19:29Z)
• Kernel methods through the roof: handling billions of points efficiently [94.31450736250918]
  カーネル法は、非パラメトリック学習に対するエレガントで原則化されたアプローチを提供するが、今のところ大規模な問題ではほとんど利用できない。 最近の進歩は、最適化、数値線形代数、ランダム射影など、多くのアルゴリズム的アイデアの利点を示している。 ここでは、これらの取り組みをさらに進めて、GPUハードウェアを最大限に活用する解決器を開発し、テストする。
  論文  参考訳（メタデータ） (2020-06-18T08:16:25Z)
• 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)
• Accelerating Feedforward Computation via Parallel Nonlinear Equation Solving [106.63673243937492]
  ニューラルネットワークの評価や自己回帰モデルからのサンプリングなどのフィードフォワード計算は、機械学習においてユビキタスである。 本稿では,非線形方程式の解法としてフィードフォワード計算の課題を定式化し,ジャコビ・ガウス・シーデル固定点法とハイブリッド法を用いて解を求める。 提案手法は, 並列化可能な繰り返し回数の削減(あるいは等値化)により, 元のフィードフォワード計算と全く同じ値が与えられることを保証し, 十分な並列化計算能力を付与する。
  論文  参考訳（メタデータ） (2020-02-10T10:11:31Z)

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

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