論文の概要: Circuit-Aware SAT Solving: Guiding CDCL via Conditional Probabilities

• arxiv url: http://arxiv.org/abs/2508.04235v1
• Date: Wed, 06 Aug 2025 09:16:47 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-08-07 20:09:22.650372
• Title: Circuit-Aware SAT Solving: Guiding CDCL via Conditional Probabilities
• Title（参考訳）: サーキット対応SATソルビング:条件付き確率によるCDCLの誘導
• Authors: Jiaying Zhu, Ziyang Zheng, Zhengyuan Shi, Yalun Cai, Qiang Xu,
• Abstract要約: 回路満足度(CSAT)は電子設計自動化において重要な役割を担っている。 本稿では,新しいサーキット対応SAT解決フレームワークであるCASCADを紹介する。 我々はCASCADが最先端のCNFベースのアプローチと比較して最大10倍の解時間を短縮することを示した。
• 参考スコア（独自算出の注目度）: 8.18310731992061
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Circuit Satisfiability (CSAT) plays a pivotal role in Electronic Design Automation. The standard workflow for solving CSAT problems converts circuits into Conjunctive Normal Form (CNF) and employs generic SAT solvers powered by Conflict-Driven Clause Learning (CDCL). However, this process inherently discards rich structural and functional information, leading to suboptimal solver performance. To address this limitation, we introduce CASCAD, a novel circuit-aware SAT solving framework that directly leverages circuit-level conditional probabilities computed via Graph Neural Networks (GNNs). By explicitly modeling gate-level conditional probabilities, CASCAD dynamically guides two critical CDCL heuristics -- variable phase selection and clause managementto significantly enhance solver efficiency. Extensive evaluations on challenging real-world Logical Equivalence Checking (LEC) benchmarks demonstrate that CASCAD reduces solving times by up to 10x compared to state-of-the-art CNF-based approaches, achieving an additional 23.5% runtime reduction via our probability-guided clause filtering strategy. Our results underscore the importance of preserving circuit-level structural insights within SAT solvers, providing a robust foundation for future improvements in SAT-solving efficiency and EDA tool design.
• Abstract（参考訳）: 回路満足度(CSAT)は電子設計自動化において重要な役割を担っている。 CSAT問題の標準的なワークフローは、回路を接続正規形式 (CNF) に変換し、Conflict-Driven Clause Learning (CDCL) を利用した一般的なSATソルバを使用する。 しかし、このプロセスは本質的にリッチな構造的および機能的な情報を破棄し、最適部分解法の性能をもたらす。 この制限に対処するために、我々は、グラフニューラルネットワーク(GNN)を介して計算される回路レベルの条件付き確率を直接活用する新しいサーキット対応SAT解決フレームワークであるCASCADを紹介する。 ゲートレベルの条件付き確率を明示的にモデル化することにより、CASCADは2つの重要なCDCLヒューリスティック(可変位相選択と節管理)を動的にガイドし、ソルバ効率を大幅に向上させる。 実世界の論理等価チェック(LEC)ベンチマークの大規模な評価では、CASCADは最先端のCNFベースのアプローチと比較して最大10倍の解時間を削減し、確率誘導された節フィルタリング戦略によってさらに23.5%のランタイム削減を実現している。 その結果,SATソルバ内における回路レベルの構造的洞察の保存の重要性を浮き彫りにし,SATソルバの高効率化とEDAツール設計のための堅牢な基盤を提供することができた。

関連論文リスト

• Learning from Algorithm Feedback: One-Shot SAT Solver Guidance with GNNs [2.722939308105689]
  この研究は、グラフニューラルネットワーク(GNN)を用いたSATソルバ分岐をガイドするパラダイムとして、RLAF(Reinforcement Learning from Algorithm Feedback)を導入している。 RLAFを訓練したポリシーは、多様なSAT問題分布にまたがる様々なベースソルバの平均解時間を著しく削減し、場合によっては2倍以上のスピードアップを達成する。
  論文  参考訳（メタデータ） (2025-05-21T22:07:08Z)
• Architect of the Bits World: Masked Autoregressive Modeling for Circuit Generation Guided by Truth Table [5.300504429005315]
  本稿では,回路生成のための条件生成モデルと微分可能なアーキテクチャ探索(DAS)を組み合わせた新しい手法を提案する。 まず、Circuit AutoEncoderに基づいてトレーニングされた回路トークンであるCircuitVQを紹介する。 次に,トークンとしてCircuitVQを活用するマスク付き自己回帰モデルであるCircuitARを開発した。
  論文  参考訳（メタデータ） (2025-02-18T11:13:03Z)
• Bayesian Parameterized Quantum Circuit Optimization (BPQCO): A task and hardware-dependent approach [49.89480853499917]
  変分量子アルゴリズム(VQA)は、最適化と機械学習問題を解決するための有望な量子代替手段として登場した。 本稿では,回路設計が2つの分類問題に対して得られる性能に与える影響を実験的に示す。 また、実量子コンピュータのシミュレーションにおいて、ノイズの存在下で得られた回路の劣化について検討する。
  論文  参考訳（メタデータ） (2024-04-17T11:00:12Z)
• An Efficient Learning-based Solver Comparable to Metaheuristics for the Capacitated Arc Routing Problem [67.92544792239086]
  我々は,高度メタヒューリスティックスとのギャップを著しく狭めるため,NNベースの解法を導入する。 まず,方向対応型注意モデル(DaAM)を提案する。 第2に、教師付き事前学習を伴い、堅牢な初期方針を確立するための教師付き強化学習スキームを設計する。
  論文  参考訳（メタデータ） (2024-03-11T02:17:42Z)
• AutoSAT: Automatically Optimize SAT Solvers via Large Language Models [10.359005620433136]
  本稿では,既存のCDCLソルバをベースとしたモジュール型検索空間の自動最適化フレームワークであるAutoSATを提案する。 AutoSATは12データセット中9データセットでMiniSatを上回り、4データセットで最先端のハイブリッドソルバKissatを上回ります。
  論文  参考訳（メタデータ） (2024-02-16T14:04:56Z)
• Transformers as Statisticians: Provable In-Context Learning with In-Context Algorithm Selection [88.23337313766353]
  この研究はまず、変換器がICLを実行するための包括的な統計理論を提供する。 コンテクストにおいて、トランスフォーマーは、幅広い種類の標準機械学習アルゴリズムを実装可能であることを示す。 エンフィングル変換器は、異なるベースICLアルゴリズムを適応的に選択することができる。
  論文  参考訳（メタデータ） (2023-06-07T17:59:31Z)
• Actor-Critic based Improper Reinforcement Learning [61.430513757337486]
  我々は,未知のマルコフ決定プロセスに対して,学習者に100万ドルのベースコントローラを付与する不適切な強化学習環境を考える。 本稿では,(1)ポリシーグラディエントに基づくアプローチ,(2)単純なアクター・クリティカル・スキームとNatural Actor-Criticスキームを切り替えるアルゴリズムを提案する。
  論文  参考訳（メタデータ） (2022-07-19T05:55:02Z)
• Efficient Quantum Circuit Design with a Standard Cell Approach, with an Application to Neutral Atom Quantum Computers [45.66259474547513]
  従来の回路設計から借用した標準セルアプローチを用いて量子回路を設計する。 本稿では,自動ルーティング方式と比較してレイアウト対応ルータが大幅に高速で,より浅い3D回路を実現することを示す。
  論文  参考訳（メタデータ） (2022-06-10T10:54:46Z)
• Efficient Knowledge Compilation Beyond Weighted Model Counting [7.828647825246474]
  このような問題に対する一般的なフレームワークとして,第2レベル代数モデルカウント (2AMC) を導入している。 KC(Knowledge Compilation)に基づく第1レベルのテクニックは、変数順序制約を課すことで、特定の2AMCインスタンスに適応している。 2AMC問題の論理構造を利用して、これらの制約の一部を省略し、負の効果を制限できることが示される。
  論文  参考訳（メタデータ） (2022-05-16T08:10:40Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
  論文  参考訳（メタデータ） (2021-07-15T04:47:35Z)
• On Continuous Local BDD-Based Search for Hybrid SAT Solving [40.252804008544985]
  CLSに必要な勾配を効率的に計算するための新しいアルゴリズムを提案する。 多くのベンチマークインスタンスに適用することにより、多用途CLSソルバであるGradSATの機能と限界について検討する。 実験結果から,GradSATは既存のSATおよびMaxSATソルバのポートフォリオに追加され,ブール適合性および最適化問題の解決に有用であることが示唆された。
  論文  参考訳（メタデータ） (2020-12-14T22:36:20Z)
• Combining Deep Learning and Optimization for Security-Constrained Optimal Power Flow [94.24763814458686]
  セキュリティに制約のある最適電力フロー(SCOPF)は、電力システムの基本である。 SCOPF問題におけるAPRのモデル化は、複雑な大規模混合整数プログラムをもたらす。 本稿では,ディープラーニングとロバスト最適化を組み合わせた新しい手法を提案する。
  論文  参考訳（メタデータ） (2020-07-14T12:38:21Z)

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

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