論文の概要: NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks

• arxiv url: http://arxiv.org/abs/2110.14053v4
• Date: Wed, 4 Oct 2023 01:31:48 GMT
• ステータス: 処理完了
• システム内更新日: 2023-10-05 23:04:26.722745
• Title: NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks
• Title（参考訳）: NeuroBack: グラフニューラルネットワークによるCDCL SAT解決の改善
• Authors: Wenxi Wang, Yang Hu, Mohit Tiwari, Sarfraz Khurshid, Kenneth McMillan, Risto Miikkulainen
• Abstract要約: 提案的満足度(SAT)は、計画、検証、セキュリティなど、多くの研究分野に影響を与えるNP完全問題である。 グラフニューラルネットワーク(GNN)を用いたCDCL SATソルバの高速化に向けた最近の研究 本稿では,(1)CDCL SATの解法に必要不可欠である変数の位相(すなわち値)を予測すること,(2)SATの解法開始前に1回だけニューラルネットワークに問い合わせること,の2つの知見に基づくNeuroBackという手法を提案する。
• 参考スコア（独自算出の注目度）: 13.972034148686205
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Propositional satisfiability (SAT) is an NP-complete problem that impacts many research fields, such as planning, verification, and security. Mainstream modern SAT solvers are based on the Conflict-Driven Clause Learning (CDCL) algorithm. Recent work aimed to enhance CDCL SAT solvers using Graph Neural Networks (GNNs). However, so far this approach either has not made solving more effective, or required substantial GPU resources for frequent online model inferences. Aiming to make GNN improvements practical, this paper proposes an approach called NeuroBack, which builds on two insights: (1) predicting phases (i.e., values) of variables appearing in the majority (or even all) of the satisfying assignments are essential for CDCL SAT solving, and (2) it is sufficient to query the neural model only once for the predictions before the SAT solving starts. Once trained, the offline model inference allows NeuroBack to execute exclusively on the CPU, removing its reliance on GPU resources. To train NeuroBack, a new dataset called DataBack containing 120,286 data samples is created. Finally, NeuroBack is implemented as an enhancement to a state-of-the-art SAT solver called Kissat. As a result, it allowed Kissat to solve 5.2% more problems on the recent SAT competition problem set, SATCOMP-2022. NeuroBack therefore shows how machine learning can be harnessed to improve SAT solving in an effective and practical manner.
• Abstract（参考訳）: 提案的満足度(SAT)は、計画、検証、セキュリティなど、多くの研究分野に影響を与えるNP完全問題である。 主流のSATソルバは、Conflict-Driven Clause Learning (CDCL)アルゴリズムに基づいている。 グラフニューラルネットワーク(GNN)を用いたCDCL SATソルバの高速化を目的とした最近の研究。 しかし、これまでのところこのアプローチは、より効果的に解決できないか、または頻繁にオンラインモデル推論のために、相当なgpuリソースを必要とした。 本稿では,GNNの改良を現実的なものにすることを目的としたNeuroBackという手法を提案する。(1)CDCL SATの解法において,満たされる課題の多数(あるいはすべて)に現れる変数の位相(すなわち値)を予測すること,(2)SATの解法が始まる前に1回だけ神経モデルに問い合わせること,である。 トレーニングが完了すると、オフラインモデル推論によって、neurobackはcpuのみで動作するようになり、gpuリソースへの依存がなくなる。 NeuroBackをトレーニングするために、120,286のデータサンプルを含むDataBackと呼ばれる新しいデータセットが作成される。 最後に、NeuroBackはKissatと呼ばれる最先端のSATソルバの拡張として実装されている。 その結果、Kissatは最近のSAT競合問題SATCOMP-2022でさらに5.2%の問題を解決することができた。 したがってneurobackは、sat解決を効果的かつ実用的な方法で改善するために機械学習をどのように活用できるかを示している。

関連論文リスト

• Self-Satisfied: An end-to-end framework for SAT generation and prediction [0.7340017786387768]
  高速SAT問題生成のためのハードウェアアクセラレーションアルゴリズムと幾何SAT符号化を導入する。 これらの進歩により、何千もの変数と数万の節でSAT問題へのアプローチをスケールできます。 私たちの研究の基本的な側面は、SATデータの本質と、機械学習モデルのトレーニングに適合する可能性に関するものです。
  論文  参考訳（メタデータ） (2024-10-18T22:25:54Z)
• LinSATNet: The Positive Linear Satisfiability Neural Networks [116.65291739666303]
  本稿では,ニューラルネットワークに人気の高い正の線形満足度を導入する方法について検討する。 本稿では,古典的なシンクホーンアルゴリズムを拡張し,複数の辺分布の集合を共同で符号化する,最初の微分可能満足層を提案する。
  論文  参考訳（メタデータ） (2024-07-18T22:05:21Z)
• GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection [45.222591894755105]
  インスタンスの3部グラフ表現に基づくSATソルバ自動選択のための新しいアプローチであるGraSSを提案する。 我々は、新しいノードの特徴設計のようなドメイン固有の決定でグラフ表現を豊かにします。 生の表現とドメイン固有の選択の組み合わせが実行時の改善につながることを実証する。
  論文  参考訳（メタデータ） (2024-05-17T18:00:50Z)
• Energy-Efficient On-Board Radio Resource Management for Satellite Communications via Neuromorphic Computing [59.40731173370976]
  本研究は,エネルギー効率のよい脳誘発機械学習モデルのオンボード無線リソース管理への応用について検討する。 関連するワークロードでは、Loihi 2に実装されたスパイクニューラルネットワーク(SNN)の方が精度が高く、CNNベースのリファレンスプラットフォームと比較して消費電力が100ドル以上削減される。
  論文  参考訳（メタデータ） (2023-08-22T03:13:57Z)
• A hybrid Quantum proposal to deal with 3-SAT problem [75.38606213726906]
  本稿では,3SAT問題を解くためのハイブリッド量子コンピューティング戦略について述べる。 この近似の性能は、量子コンピューティングの観点から3-SATを扱う際に、一連の代表的なシナリオで検証されている。
  論文  参考訳（メタデータ） (2023-06-07T12:19:22Z)
• Addressing Variable Dependency in GNN-based SAT Solving [19.38746341365531]
  本稿では、繰り返しニューラルネットワークを統合したGNNベースのアーキテクチャであるAsymSATを提案し、可変代入に対する依存予測を生成する。 実験結果から,大規模テストセット上でのSATインスタンスの解数を改善することにより,依存変数予測がGNN方式の解解能力を拡張できることが示唆された。
  論文  参考訳（メタデータ） (2023-04-18T05:33:33Z)
• 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)
• Enhancing SAT solvers with glue variable predictions [2.635832975589208]
  我々は、最先端のSATソルバであるCaDiCaLを改良し、SATCOMP 2018とSATRACE 2019のパフォーマンスを改善し、教師付き学習と強化学習によるSHA-1プレイメージアタックのデータセット上でのパフォーマンスを向上する。 我々はこれらの制限に対処し、より単純なネットワークアーキテクチャを用いて、数百万の節を含む大規模産業問題に対してCPU推論を行い、代わりにエミュレート変数を予測する訓練を行い、ラベル付きデータを簡単に生成し、強化学習タスクとして定式化することができる。
  論文  参考訳（メタデータ） (2020-07-06T07:16:49Z)

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

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