論文の概要: Deeply Optimizing the SAT Solver for the IC3 Algorithm

• arxiv url: http://arxiv.org/abs/2501.18612v2
• Date: Mon, 03 Feb 2025 02:49:14 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-02-04 16:03:57.436639
• Title: Deeply Optimizing the SAT Solver for the IC3 Algorithm
• Title（参考訳）: IC3アルゴリズムにおけるSATソルバーの最適化
• Authors: Yuheng Su, Qiusong Yang, Yiwei Ci, Yingcheng Li, Tianjun Bu, Ziyu Huang,
• Abstract要約: 観測結果に基づいて,IC3におけるSATソルバの最適化について述べる。 バイナリヒープをバケットに置き換えて、一定時間操作を実現しています。 我々はこれらの最適化を統合した新しい軽量CDCL SATソルバであるGipSATを開発した。
• 参考スコア（独自算出の注目度）: 0.23749905164931204
• License:
• Abstract: The IC3 algorithm, also known as PDR, is a SAT-based model checking algorithm that has significantly influenced the field in recent years due to its efficiency, scalability, and completeness. It utilizes SAT solvers to solve a series of SAT queries associated with relative induction. In this paper, we introduce several optimizations for the SAT solver in IC3 based on our observations of the unique characteristics of these SAT queries. By observing that SAT queries do not necessarily require decisions on all variables, we compute a subset of variables that need to be decided before each solving process while ensuring that the result remains unaffected. Additionally, noting that the overhead of binary heap operations in VSIDS is non-negligible, we replace the binary heap with buckets to achieve constant-time operations. Furthermore, we support temporary clauses without the need to allocate a new activation variable for each solving process, thereby eliminating the need to reset solvers. We developed a novel lightweight CDCL SAT solver, GipSAT, which integrates these optimizations. A comprehensive evaluation highlights the performance improvements achieved by GipSAT. Specifically, the GipSAT-based IC3 demonstrates an average speedup of 3.61 times in solving time compared to the IC3 implementation based on MiniSat.
• Abstract（参考訳）: PDRとしても知られるIC3アルゴリズムはSATベースのモデルチェックアルゴリズムであり、その効率性、スケーラビリティ、完全性により近年、この分野に大きな影響を与えている。 SATソルバを用いて、相対帰納に関連するSATクエリの一連の解決を行う。 本稿では、これらのSATクエリのユニークな特性の観測結果に基づいて、IC3におけるSATソルバの最適化について述べる。 SATクエリが必ずしもすべての変数の決定を必要としないことを観察することにより、各解決プロセスの前に決定する必要がある変数のサブセットを計算し、結果が影響を受けないことを保証する。 さらに、VSIDSにおけるバイナリヒープ操作のオーバーヘッドは無視できないことに注意し、バイナリヒープをバケットに置き換えて一定時間操作を実現する。 さらに、各問題解決プロセスに新たなアクティベーション変数を割り当てる必要がなく、仮節をサポートし、ソルバをリセットする必要がなくなる。 我々はこれらの最適化を統合した新しい軽量CDCL SATソルバGipSATを開発した。 包括的な評価では、GipSATによって達成されたパフォーマンス改善が強調されている。 具体的には、GipSATベースのIC3は、MiniSatをベースとしたIC3実装と比較して平均3.61倍のスピードアップを示している。

関連論文リスト

• SolSearch: An LLM-Driven Framework for Efficient SAT-Solving Code Generation [13.056487325961688]
  Satisfiability(SAT)問題は、ソフトウェア工学における重要な応用において、中核的な課題である。 本稿では,大規模言語モデル(LLM)を利用してSAT解決戦略の自動発見と最適化を行う新しいフレームワークであるSolSearchを提案する。
  論文  参考訳（メタデータ） (2025-02-20T07:25:21Z)
• Resource-Constrained Heuristic for Max-SAT [0.848762374187855]
  より大規模な問題をより小さなサブコンポーネントに繰り返し分解する,Max-SATのインスタンスに対するリソース制約を提案する。 本研究では,所定のSATインスタンスの構造を利用するグラフベースの新しい手法を含む,変数選択手法の集合を分析する。 我々は,Max-SAT評価ベンチマークを用いて,ランダムに生成されたMax-SATインスタンスと実世界の実例について実験を行った。
  論文  参考訳（メタデータ） (2024-10-11T18:20:08Z)
• GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection [45.222591894755105]
  インスタンスの3部グラフ表現に基づくSATソルバ自動選択のための新しいアプローチであるGraSSを提案する。 我々は、新しいノードの特徴設計のようなドメイン固有の決定でグラフ表現を豊かにします。 生の表現とドメイン固有の選択の組み合わせが実行時の改善につながることを実証する。
  論文  参考訳（メタデータ） (2024-05-17T18:00:50Z)
• 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)
• A hybrid Quantum proposal to deal with 3-SAT problem [75.38606213726906]
  本稿では,3SAT問題を解くためのハイブリッド量子コンピューティング戦略について述べる。 この近似の性能は、量子コンピューティングの観点から3-SATを扱う際に、一連の代表的なシナリオで検証されている。
  論文  参考訳（メタデータ） (2023-06-07T12:19:22Z)
• Amplitude amplification-inspired QAOA: Improving the success probability for solving 3SAT [55.78588835407174]
  振幅増幅アルゴリズムは、可変代入を満たすために非構造化探索に適用することができる。 Quantum Approximate Optimization Algorithm (QAOA)は、ノイズのある中間量子デバイスのための3SATを解くための有望な候補である。 振幅増幅によるQAOAの変種を導入し、3SATの成功確率を改善する。
  論文  参考訳（メタデータ） (2023-03-02T11:52:39Z)
• 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)
• SATformer: Transformer-Based UNSAT Core Learning [0.0]
  本稿では,SAT 問題に対する Transformer ベースのアプローチである SATformer を紹介する。 SATformerは、問題を直接解決するのではなく、満足できないことに焦点をあてて、その問題を反対方向からアプローチする。 SATformerは、シングルビットの満足度結果と最小限の不満コアを使用して、マルチタスク学習アプローチでトレーニングされる。 実験の結果,SATformerは既存のソルバのランタイムを平均21.33%削減できることがわかった。
  論文  参考訳（メタデータ） (2022-09-02T11:17:39Z)
• DeepSAT: An EDA-Driven Learning Framework for SAT [9.111341161918375]
  We present DeepSAT, a novel-to-end learning framework for the Boolean satisfiability (SAT) problem。 DeepSATは最先端の学習ベースSATソリューションに対して,大幅な精度向上を実現している。
  論文  参考訳（メタデータ） (2022-05-27T03:20:42Z)
• 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)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
  論文  参考訳（メタデータ） (2021-07-15T04:47:35Z)

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

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