論文の概要: Accelerated Fourier SAT (AFSAT): Fully Realising a GPU-based Symmetric Pseudo-Boolean SAT Solver

• arxiv url: http://arxiv.org/abs/2606.06641v1
• Date: Thu, 04 Jun 2026 18:47:45 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-08 14:33:29.407245
• Title: Accelerated Fourier SAT (AFSAT): Fully Realising a GPU-based Symmetric Pseudo-Boolean SAT Solver
• Title（参考訳）: 加速フーリエSAT(AFSAT):GPUベースの擬似ブールSATソルバーの完全実現
• Authors: Cody J Christopher, Charles Gretton,
• Abstract要約: 連続局所探索に基づく疑似ブール充足性のためのGPU加速型解法 AFSAT を提案する。 本研究では,概念実証よりも数値安定性,実行時性能,メモリ効率が大幅に向上したことを示す。 JAXシャーディングによる複数のアクセラレータへのスケーリングでは,ほぼ直線的なスループットを実現しています。
• 参考スコア（独自算出の注目度）: 0.6353525052246608
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We present Accelerated Fourier SAT (AFSAT), a GPU-accelerated solver for pseudo-Boolean satisfiability based on continuous local search (CLS). AFSAT realises the proof-of-concept approach, FastFourierSAT, into a fully-engineered solver supporting any heterogeneous mixture of symmetric constraint types and lengths within a single problem instance. Using the JAX compiler, AFSAT leverages pure function composition, automatic vectorisation, automatic differentiation, and just-in-time (JIT) compilation to perform massively parallel CLS across batches of candidate assignments. We demonstrate substantially improved numerical stability, runtime performance, and memory efficiency over the proof-of-concept. We achieve this by way of identifying and addressing various limitations that arise from memory latency and floating-point representation, as well as leveraging automatic parallelisation and compact representations. The inherent representational and stability limitations of floating point are partially addressed by a tailored discrete Fourier transform implementation. We achieve near-linear throughput when scaling to multiple accelerators via JAX array sharding.
• Abstract（参考訳）: 本稿では,連続局所探索(CLS)に基づく疑似ブール充足性のためのGPU高速化解法である Accelerated Fourier SAT (AFSAT) を提案する。 AFSATは、概念実証アプローチであるFastFourierSATを、単一の問題インスタンス内で対称制約型と長さの不均一な混合をサポートする、完全にエンジニアリングされた解決器に実現している。 JAXコンパイラを使用すると、AFSATは純粋な関数合成、自動ベクトル化、自動微分、ジャスト・イン・タイム(JIT)コンパイルを利用して、候補割り当てのバッチ間で非常に並列なCLSを実行する。 本研究では,概念実証よりも数値安定性,実行時性能,メモリ効率が大幅に向上したことを示す。 我々は、メモリ遅延や浮動小数点表現から生じる様々な制限を識別し、対処し、自動並列化とコンパクト表現を活用することでこれを実現する。 浮動小数点の固有表現と安定性の制限は、部分的に調整された離散フーリエ変換の実装によって対処される。 JAX配列シャーディングによる複数のアクセラレータへのスケーリングでは,ほぼ線形スループットを実現しています。

関連論文リスト

• TurboSAT: Gradient-Guided Boolean Satisfiability Accelerated on GPU-CPU Hybrid System [7.530665570222049]
  最先端の満足度解決者は、本質的に競合駆動型検索アルゴリズムに大きく依存している。 ニューラルネットワークのトレーニングに着想を得て、SAT問題を二項行列行列行列乗法層として定式化する。 我々は、並列微分可能最適化とシーケンシャルサーチの長所を組み合わせて、ハイブリッドGPU-CPUシステムでSATを高速化する。
  論文  参考訳（メタデータ） (2025-11-11T01:41:40Z)
• Orthogonal Finetuning Made Scalable [92.34573849209238]
  OFT(Orthogonal Finetuning)は、壊滅的な忘れ込みを防止しつつ、パラメータ効率の高い適応を提供するが、実行時とメモリの要求が高いため、実際のデプロイメントが制限される。 ここでは,OFTの計算ボトルネックを重み中心の実装とみなす。 本稿では,行列ベクトル乗法(行列フリー計算)を用いて,計算コストを2次に削減する入力中心の変換法OFTv2を提案する。 これらの変更により、OFTv2は最大10倍の高速トレーニングと3倍のGPUメモリ使用率を達成することができる。
  論文  参考訳（メタデータ） (2025-06-24T17:59:49Z)
• High-Throughput SAT Sampling [3.8108678341258138]
  本稿では,GPUアクセラレーション・サシフィビリティ(SAT)サンプリングのための新しい手法を提案する。 提案手法は,CNF表現を単純化した多レベル多出力ブール関数に分解することで,SAT問題の論理的制約を変換する。 最先端のサンプリングよりも33.6times$から523.6times$まで、大幅に改善されたGPUアクセラレーションサンプリングを実現しています。
  論文  参考訳（メタデータ） (2025-02-12T03:20:45Z)
• Sparsity-Constraint Optimization via Splicing Iteration [1.3622424109977902]
  我々は sPlicing itEration (SCOPE) を用いたスペーサリティ制約最適化アルゴリズムを開発した。 SCOPEはパラメータをチューニングせずに効率的に収束する。 SCOPEを用いて2次最適化を解き、スパース分類器を学習し、バイナリ変数のスパースマルコフネットワークを復元する。 C++実装に基づいたオープンソースのPythonパッケージskscopeがGitHubで公開されている。
  論文  参考訳（メタデータ） (2024-06-17T18:34:51Z)
• Equivariant Scalar Fields for Molecular Docking with Fast Fourier Transforms [11.163940886337798]
  機械学習がより高速な最適化を可能にする機能形式でスコアリング関数を学習する方法を示す。 我々は,2つの簡易ドッキング関連タスク,デコイポーズスコアリングと剛性コンフォメータドッキングのスコアリング機能をベンチマークした。 提案手法は,広く使用されているVinaとGninaのスコアリング関数と比較して,結晶構造に類似しているが高速な性能を実現し,予測された構造に対してより堅牢である。
  論文  参考訳（メタデータ） (2023-12-07T14:32:32Z)
• Massively Parallel Continuous Local Search for Hybrid SAT Solving on GPUs [5.245714076090567]
  我々は、勾配駆動連続局所探索に基づく高並列ハイブリッドSATソルバであるFastFourierSATを提案する。 以上の結果から,FastFourierSATはCPU上で実装された以前のプロトタイプの100倍以上の速度で勾配を計算することがわかった。 FastFourierSATは、ほとんどのインスタンスを解決し、より大きなインスタンスで有望なパフォーマンスを示す。
  論文  参考訳（メタデータ） (2023-08-29T04:50:07Z)
• Performance Embeddings: A Similarity-based Approach to Automatic Performance Optimization [71.69092462147292]
  パフォーマンス埋め込みは、アプリケーション間でパフォーマンスチューニングの知識伝達を可能にする。 本研究では, 深層ニューラルネットワーク, 密度およびスパース線形代数合成, および数値風速予測ステンシルのケーススタディにおいて, この伝達チューニング手法を実証する。
  論文  参考訳（メタデータ） (2023-03-14T15:51:35Z)
• Multiway Non-rigid Point Cloud Registration via Learned Functional Map Synchronization [105.14877281665011]
  我々は、点雲上に定義された学習関数に関する地図を同期させることにより、複数の非剛体形状を登録する新しい方法であるSyNoRiMを提案する。 提案手法は,登録精度において最先端の性能を達成できることを実証する。
  論文  参考訳（メタデータ） (2021-11-25T02:37:59Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
  論文  参考訳（メタデータ） (2021-07-15T04:47:35Z)
• Square Root Bundle Adjustment for Large-Scale Reconstruction [56.44094187152862]
  QR分解によるランドマーク変数のnullspace marginalizationに依存するバンドル調整問題の新たな定式化を提案する。 平方根束調整と呼ばれる私たちのアプローチは、一般的に使用されるSchur補完トリックと代数的に等価です。 BALデータセットを用いた実世界での実験では、提案されたソルバが単一の精度でも平均的等しく正確なソリューションで達成できることを示す。
  論文  参考訳（メタデータ） (2021-03-02T16:26:20Z)

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

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