論文の概要: High-Throughput SAT Sampling

• arxiv url: http://arxiv.org/abs/2502.08673v1
• Date: Wed, 12 Feb 2025 03:20:45 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-02-14 13:49:54.801147
• Title: High-Throughput SAT Sampling
• Title（参考訳）: 高出力SATサンプリング
• Authors: Arash Ardakani, Minwoo Kang, Kevin He, Qijing Huang, John Wawrzynek,
• Abstract要約: 本稿では,GPUアクセラレーション・サシフィビリティ(SAT)サンプリングのための新しい手法を提案する。 提案手法は,CNF表現を単純化した多レベル多出力ブール関数に分解することで,SAT問題の論理的制約を変換する。 最先端のサンプリングよりも33.6times$から523.6times$まで、大幅に改善されたGPUアクセラレーションサンプリングを実現しています。
• 参考スコア（独自算出の注目度）: 3.8108678341258138
• License:
• Abstract: In this work, we present a novel technique for GPU-accelerated Boolean satisfiability (SAT) sampling. Unlike conventional sampling algorithms that directly operate on conjunctive normal form (CNF), our method transforms the logical constraints of SAT problems by factoring their CNF representations into simplified multi-level, multi-output Boolean functions. It then leverages gradient-based optimization to guide the search for a diverse set of valid solutions. Our method operates directly on the circuit structure of refactored SAT instances, reinterpreting the SAT problem as a supervised multi-output regression task. This differentiable technique enables independent bit-wise operations on each tensor element, allowing parallel execution of learning processes. As a result, we achieve GPU-accelerated sampling with significant runtime improvements ranging from $33.6\times$ to $523.6\times$ over state-of-the-art heuristic samplers. We demonstrate the superior performance of our sampling method through an extensive evaluation on $60$ instances from a public domain benchmark suite utilized in previous studies.
• Abstract（参考訳）: 本稿では,GPUを高速化したBoolean satisfiability(SAT)サンプリングのための新しい手法を提案する。 共役正規形式(CNF)を直接操作する従来のサンプリングアルゴリズムとは異なり、本手法は、CNF表現を単純化されたマルチレベル多出力ブール関数に分解することでSAT問題の論理的制約を変換する。 次に、勾配に基づく最適化を活用して、様々な有効なソリューションの探索をガイドする。 本手法は、SATインスタンスの回路構造を直接操作し、SAT問題を教師付き多出力回帰タスクとして再解釈する。 この微分可能な技術は、各テンソル要素に対する独立したビット演算を可能にし、学習プロセスの並列実行を可能にする。 その結果、最先端のヒューリスティックサンプリングよりも33.6\times$から523.6\times$まで大幅に改善されたGPUアクセラレーションサンプリングを実現した。 過去の研究で利用したパブリックドメインベンチマークスイートから60ドルのインスタンスを広範囲に評価することで,サンプリング手法の優れた性能を実証する。

関連論文リスト

• Smart Cubing for Graph Search: A Comparative Study [15.989407883187962]
  立方体とコンカヤによる並列解法はSATソルバをハードインスタンスに拡張するための重要な方法である。 キューブ・アンド・コンカーは純粋なSAT問題に対して成功したが、SATソルバへの応用はプロパゲータによって拡張され、ユニークな課題が提示される。 本研究では, SATモジュロ対称性(SMS)を用いて, 対称性を破るプロパゲータが等方性グラフを除去する制約を学習することで探索空間を減少させる問題について検討する。
  論文  参考訳（メタデータ） (2025-01-27T22:15:54Z)
• Quasi-random Multi-Sample Inference for Large Language Models [1.647759094903376]
  大規模言語モデル(LLM)は、しばしばマルチサンプルデコード戦略を備えている。 ビームサーチやサンプリングベース技術のような従来のテキスト生成手法には、顕著な制限がある。 本研究では,算術的サンプリングの可能性について検討し,祖先的サンプリングと対比する。
  論文  参考訳（メタデータ） (2024-11-09T18:55:04Z)
• Provably Faster Algorithms for Bilevel Optimization via Without-Replacement Sampling [96.47086913559289]
  勾配に基づくアルゴリズムはバイレベル最適化に広く用いられている。 本研究では,より高速な収束率を実現する非置換サンプリングに基づくアルゴリズムを提案する。 合成および実世界の両方のアプリケーションに対してアルゴリズムを検証する。
  論文  参考訳（メタデータ） (2024-11-07T17:05:31Z)
• Resource-Constrained Heuristic for Max-SAT [0.848762374187855]
  より大規模な問題をより小さなサブコンポーネントに繰り返し分解する,Max-SATのインスタンスに対するリソース制約を提案する。 本研究では,所定のSATインスタンスの構造を利用するグラフベースの新しい手法を含む,変数選択手法の集合を分析する。 我々は,Max-SAT評価ベンチマークを用いて,ランダムに生成されたMax-SATインスタンスと実世界の実例について実験を行った。
  論文  参考訳（メタデータ） (2024-10-11T18:20:08Z)
• 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)
• Multi-block-Single-probe Variance Reduced Estimator for Coupled Compositional Optimization [49.58290066287418]
  構成問題の複雑さを軽減するために,MSVR (Multi-block-probe Variance Reduced) という新しい手法を提案する。 本研究の結果は, 試料の複雑さの順序や強靭性への依存など, 様々な面で先行して改善された。
  論文  参考訳（メタデータ） (2022-07-18T12:03:26Z)
• Fast Differentiable Matrix Square Root and Inverse Square Root [65.67315418971688]
  微分可能な行列平方根と逆平方根を計算するためのより効率的な2つの変種を提案する。 前方伝搬には, Matrix Taylor Polynomial (MTP) を用いる方法と, Matrix Pad'e Approximants (MPA) を使用する方法がある。 一連の数値実験により、両方の手法がSVDやNSの繰り返しと比較してかなりスピードアップすることが示された。
  論文  参考訳（メタデータ） (2022-01-29T10:00:35Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
  論文  参考訳（メタデータ） (2021-07-15T04:47:35Z)
• Adaptive Sampling for Best Policy Identification in Markov Decision Processes [79.4957965474334]
  本稿では,学習者が生成モデルにアクセスできる場合の,割引マルコフ決定(MDP)における最良の政治的識別の問題について検討する。 最先端アルゴリズムの利点を論じ、解説する。
  論文  参考訳（メタデータ） (2020-09-28T15:22:24Z)
• Non-Adaptive Adaptive Sampling on Turnstile Streams [57.619901304728366]
  カラムサブセット選択、部分空間近似、射影クラスタリング、および空間サブリニアを$n$で使用するターンタイルストリームのボリュームに対する最初の相対エラーアルゴリズムを提供する。 我々の適応的なサンプリング手法は、様々なデータ要約問題に多くの応用をもたらしており、これは最先端を改善するか、より緩和された行列列モデルで以前に研究されただけである。
  論文  参考訳（メタデータ） (2020-04-23T05:00:21Z)

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

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