論文の概要: NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks
- arxiv url: http://arxiv.org/abs/2110.14053v6
- Date: Tue, 28 Nov 2023 21:05:18 GMT
- ステータス: 処理完了
- システム内更新日: 2023-12-01 01:13:24.907226
- 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解決を効果的かつ実用的な方法で改善するために機械学習をどのように活用できるかを示している。
関連論文リスト
- 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) - Machine Learning for SAT: Restricted Heuristics and New Graph
Representations [0.8870188183999854]
SATは、自動スケジューリングを含む多くのアプリケーションにおいて、基本的なNP完全問題である。
大きなインスタンスを解決するためには、SATソルバは、例えばDPLLとCDCLソルバの分岐変数を選択するなど、ブールアンに依存する必要がある。
我々は、訓練されたMLモデルでいくつかの初期ステップを行い、古典的なランタイムに制御をリリースする戦略を提案する。
論文 参考訳(メタデータ) (2023-07-18T10:46:28Z) - 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) - Learning To Dive In Branch And Bound [95.13209326119153]
グラフニューラルネットワークを用いて特定の潜水構造を学習するためのL2Diveを提案する。
我々は、変数の割り当てを予測するために生成モデルを訓練し、線形プログラムの双対性を利用して潜水決定を行う。
論文 参考訳(メタデータ) (2023-01-24T12:01:45Z) - 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) - Recognizing and Verifying Mathematical Equations using Multiplicative
Differential Neural Units [86.9207811656179]
メモリ拡張ニューラルネットワーク(NN)は、高次、メモリ拡張外挿、安定した性能、より高速な収束を実現することができることを示す。
本モデルでは,現在の手法と比較して1.53%の精度向上を達成し,2.22%のtop-1平均精度と2.96%のtop-5平均精度を達成している。
論文 参考訳(メタデータ) (2021-04-07T03:50:11Z) - Enhancing SAT solvers with glue variable predictions [2.635832975589208]
我々は、最先端のSATソルバであるCaDiCaLを改良し、SATCOMP 2018とSATRACE 2019のパフォーマンスを改善し、教師付き学習と強化学習によるSHA-1プレイメージアタックのデータセット上でのパフォーマンスを向上する。
我々はこれらの制限に対処し、より単純なネットワークアーキテクチャを用いて、数百万の節を含む大規模産業問題に対してCPU推論を行い、代わりにエミュレート変数を予測する訓練を行い、ラベル付きデータを簡単に生成し、強化学習タスクとして定式化することができる。
論文 参考訳(メタデータ) (2020-07-06T07:16:49Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。