論文の概要: GaloisSAT: Differentiable Boolean Satisfiability Solving via Finite Field Algebra

• arxiv url: http://arxiv.org/abs/2603.28796v1
• Date: Wed, 25 Mar 2026 19:06:06 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-01 15:25:02.478842
• Title: GaloisSAT: Differentiable Boolean Satisfiability Solving via Finite Field Algebra
• Title（参考訳）: GaloisSAT:有限場代数による微分可能なブール満足度解法
• Authors: Curie Kim, Carsten Portner, Mingju Liu, Steve Dai, Haoxing Ren, Brucek Khailany, Alvaro Velasquez, Ismail Alkhouri, Cunxi Yu,
• Abstract要約: 本稿では,新しいGPU-CPU SATソルバであるGaloisSATを紹介する。 結果は、公式のSATコンペティション PAR-2 で大幅に改善された。 ガロワSATは、満足できるカテゴリーでは8.41倍のスピードアップ、満足できないカテゴリーでは1.29倍のスピードアップを達成する。
• 参考スコア（独自算出の注目度）: 17.171285034317087
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Boolean satisfiability (SAT) problem, the first problem proven to be NP-complete, has become a fundamental challenge in computational complexity, with widespread applications in optimization and verification across many domains. Despite significant algorithmic advances over the past two decades, the performance of SAT solvers has improved at a limited pace. Notably, the 2025 competition winner shows only about a 2X improvement over the 2006 winner in SAT Competition performance after nearly 20 years of effort. This paper introduces GaloisSAT, a novel hybrid GPU-CPU SAT solver that integrates a differentiable SAT solving engine powered by modern machine learning infrastructure on GPUs, followed by a traditional CDCL-based SAT solving stage on CPUs. GaloisSAT is benchmarked against the latest versions of state-of-the-art solvers, Kissat and CaDiCaL, using the SAT Competition 2024 benchmark suite. Results demonstrate substantial improvements in the official SAT Competition metric PAR-2 (penalized average runtime with a timeout of 5,000 seconds and a penalty factor of 2). Specifically, GaloisSAT achieves an 8.41X speedup in the satisfiable category and a 1.29X speedup in the unsatisfiable category compared to the strongest baselines.
• Abstract（参考訳）: NP完全であることが証明された最初の問題であるブール充足可能性(SAT)問題は、多くの領域にまたがる最適化と検証の幅広い応用において、計算複雑性の根本的な課題となっている。 過去20年間のアルゴリズムの進歩にもかかわらず、SATソルバの性能は限られたペースで向上した。 特に、2025年のコンペの勝者は、約20年の努力を経て、2006年のSATコンペティションの勝者の2倍の改善しか示さなかった。 本稿では,新しいGPU-CPU SATソルバであるGaloisSATについて紹介する。 GaloisSATは、SAT Competition 2024ベンチマークスイートを使用して、最先端の解決ツールであるKissatとCaDiCaLに対してベンチマークされている。 その結果,公式なSATコンペティション指標PAR-2(タイムアウトが5,000秒,ペナルティ係数が2。 具体的には、GaloisSATは満足度の高いカテゴリで8.41倍のスピードアップを達成し、最強のベースラインに比べて1.29倍のスピードアップを達成している。

関連論文リスト

• TurboSAT: Gradient-Guided Boolean Satisfiability Accelerated on GPU-CPU Hybrid System [7.530665570222049]
  最先端の満足度解決者は、本質的に競合駆動型検索アルゴリズムに大きく依存している。 ニューラルネットワークのトレーニングに着想を得て、SAT問題を二項行列行列行列乗法層として定式化する。 我々は、並列微分可能最適化とシーケンシャルサーチの長所を組み合わせて、ハイブリッドGPU-CPUシステムでSATを高速化する。
  論文  参考訳（メタデータ） (2025-11-11T01:41:40Z)
• 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)
• A hybrid Quantum proposal to deal with 3-SAT problem [75.38606213726906]
  本稿では,3SAT問題を解くためのハイブリッド量子コンピューティング戦略について述べる。 この近似の性能は、量子コンピューティングの観点から3-SATを扱う際に、一連の代表的なシナリオで検証されている。
  論文  参考訳（メタデータ） (2023-06-07T12:19:22Z)
• Estimating the hardness of SAT encodings for Logical Equivalence Checking of Boolean circuits [58.83758257568434]
  LEC インスタンスの SAT 符号化の硬さは SAT パーティショニングでは textitw.r. と推定できることを示す。 そこで本研究では, SAT符号化の難易度を精度良く推定できるパーティショニング法を提案する。
  論文  参考訳（メタデータ） (2022-10-04T09:19:13Z)
• Machine Learning Methods in Solving the Boolean Satisfiability Problem [72.21206588430645]
  本論文は, Boolean satisfiability problem (SAT) を機械学習技術で解くことに関する最近の文献をレビューする。 ML-SATソルバを手作り特徴を持つナイーブ分類器からNeuroSATのような新たなエンド・ツー・エンドSATソルバまで,進化するML-SATソルバについて検討する。
  論文  参考訳（メタデータ） (2022-03-02T05:14:12Z)
• NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks [13.185943308470286]
  提案的満足度(SAT)は、計画、検証、セキュリティなど、多くの研究分野に影響を与えるNP完全問題である。 グラフニューラルネットワーク(GNN)を用いたCDCL SATソルバの高速化に向けた最近の研究 本稿では,(1)CDCL SATの解法に必要不可欠である変数の位相(すなわち値)を予測すること,(2)SATの解法開始前に1回だけニューラルネットワークに問い合わせること,の2つの知見に基づくNeuroBackという手法を提案する。
  論文  参考訳（メタデータ） (2021-10-26T22:08:22Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
  論文  参考訳（メタデータ） (2021-07-15T04:47:35Z)

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

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