論文の概要: G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural
Networks
- arxiv url: http://arxiv.org/abs/2309.16941v1
- Date: Fri, 29 Sep 2023 02:50:57 GMT
- ステータス: 処理完了
- システム内更新日: 2023-10-02 15:46:51.963932
- Title: G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural
Networks
- Title(参考訳): G4SATBench: グラフニューラルネットワークによるSAT解決のベンチマークと改善
- Authors: Zhaoyu Li, Jinpei Guo, Xujie Si
- Abstract要約: グラフニューラルネットワーク(GNN)は、ブール満足度問題(SAT)を解決するための有望なアプローチとして登場した。
G4SATBenchは、GNNベースのSATソルバの包括的な評価フレームワークを確立する最初のベンチマーク研究である。
GNNベースのSATソルバの性能について,実験結果から貴重な知見を得た。
- 参考スコア(独自算出の注目度): 8.936151867825112
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Graph neural networks (GNNs) have recently emerged as a promising approach
for solving the Boolean Satisfiability Problem (SAT), offering potential
alternatives to traditional backtracking or local search SAT solvers. However,
despite the growing volume of literature in this field, there remains a notable
absence of a unified dataset and a fair benchmark to evaluate and compare
existing approaches. To address this crucial gap, we present G4SATBench, the
first benchmark study that establishes a comprehensive evaluation framework for
GNN-based SAT solvers. In G4SATBench, we meticulously curate a large and
diverse set of SAT datasets comprising 7 problems with 3 difficulty levels and
benchmark a broad range of GNN models across various prediction tasks, training
objectives, and inference algorithms. To explore the learning abilities and
comprehend the strengths and limitations of GNN-based SAT solvers, we also
compare their solving processes with the heuristics in search-based SAT
solvers. Our empirical results provide valuable insights into the performance
of GNN-based SAT solvers and further suggest that existing GNN models can
effectively learn a solving strategy akin to greedy local search but struggle
to learn backtracking search in the latent space.
- Abstract(参考訳): グラフニューラルネットワーク(GNN)は先頃、従来のバックトラックやローカルサーチSATソルバに代わる選択肢を提供する、Boolean Satisfiability Problem(SAT)を解決するための有望なアプローチとして登場した。
しかし、この分野における文献の量の増加にもかかわらず、既存のアプローチを評価し比較するための統一データセットと公正なベンチマークが存在しないことは注目すべきである。
G4SATBenchは、GNNベースのSATソルバの総合的な評価フレームワークを確立する最初のベンチマーク研究である。
G4SATBenchでは,3つの難易度を持つ7つの問題からなるSATデータセットの大規模かつ多種多様な集合を慎重にキュレートし,様々な予測タスク,学習目標,推論アルゴリズムを含む幅広いGNNモデルをベンチマークする。
学習能力を探究し,GNNベースのSATソルバの強みと限界を理解するために,それらの解法とサーチベースのSATソルバのヒューリスティックスを比較する。
実験結果から,既存のGNNモデルでは,局所探索に類似した解法を効果的に学習できるが,潜在空間における探索のバックトラックを学習できないことが示唆された。
関連論文リスト
- SEGO: Sequential Subgoal Optimization for Mathematical Problem-Solving [64.38649623473626]
大規模言語モデル(LLM)は人工知能の大幅な進歩を導いた。
数学的問題を解く能力を高めるために,textbfSEquential subtextbfGoal textbfOptimization (SEGO) という新しいフレームワークを提案する。
論文 参考訳(メタデータ) (2023-10-19T17:56:40Z) - Using deep learning to construct stochastic local search SAT solvers
with performance bounds [0.0]
グラフニューラルネットワークを用いてオーラクルを訓練し、2つのSLSソルバ上で、様々な難易度を持つランダムSATインスタンス上でそれらを評価する。
GNNベースのオラクルへのアクセスは,両者のパフォーマンスを著しく向上させることがわかった。
論文 参考訳(メタデータ) (2023-09-20T16:27:52Z) - Evolutionary Diversity Optimisation in Constructing Satisfying
Assignments [20.386139395296215]
本稿では,EDOの文脈におけるブール充足可能性問題(SAT)について検討する。
SATは計算機科学において非常に重要であり、KPやTSPといったEDO文献で研究されている他の問題とは異なる。
本稿では,SAT解の集合間の多様性を明示的に最大化するために,よく知られたSATソルバを用いた進化的アルゴリズムを提案する。
論文 参考訳(メタデータ) (2023-05-19T06:26:10Z) - Addressing Variable Dependency in GNN-based SAT Solving [19.38746341365531]
本稿では、繰り返しニューラルネットワークを統合したGNNベースのアーキテクチャであるAsymSATを提案し、可変代入に対する依存予測を生成する。
実験結果から,大規模テストセット上でのSATインスタンスの解数を改善することにより,依存変数予測がGNN方式の解解能力を拡張できることが示唆された。
論文 参考訳(メタデータ) (2023-04-18T05:33:33Z) - W2SAT: Learning to generate SAT instances from Weighted Literal
Incidence Graphs [13.173307471333619]
W2SATは、現実世界/産業インスタンスから固有の構造と特性を学ぶことによってSAT式を生成するフレームワークである。
Weighted Literal Incidence Graph (WLIG)と呼ばれる新しいSAT表現を導入する。
WLIGからSAT問題への復号化は、新しい丘登り最適化法で重なり合う斜角を見つけることをモデル化する。
論文 参考訳(メタデータ) (2023-02-01T06:30:41Z) - Towards Better Out-of-Distribution Generalization of Neural Algorithmic
Reasoning Tasks [51.8723187709964]
ニューラルネットワーク推論タスクのOOD一般化について検討する。
目標は、ディープニューラルネットワークを使用して入出力ペアからアルゴリズムを学ぶことである。
論文 参考訳(メタデータ) (2022-11-01T18:33:20Z) - 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) - GNNRank: Learning Global Rankings from Pairwise Comparisons via Directed
Graph Neural Networks [68.61934077627085]
本稿では,グラフ埋め込みを学習可能なGNNと互換性のあるモデリングフレームワークであるGNNRankを紹介する。
既存の手法と比較して,我々の手法が競争力があり,しばしば優れた性能を発揮することを示す。
論文 参考訳(メタデータ) (2022-02-01T04:19:50Z) - NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks [13.972034148686205]
提案的満足度(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) - Graph Neural Networks for Motion Planning [108.51253840181677]
低次元問題に対する高密度固定グラフ上のGNNと高次元問題に対するサンプリングベースGNNの2つの手法を提案する。
RRT(Rapidly-Exploring Random Trees)におけるクリティカルノードの特定やサンプリング分布の学習といった計画上の問題にGNNが取り組む能力について検討する。
臨界サンプリング、振り子、6つのDoFロボットアームによる実験では、GNNは従来の分析手法の改善だけでなく、完全に接続されたニューラルネットワークや畳み込みニューラルネットワークを用いた学習アプローチも示している。
論文 参考訳(メタデータ) (2020-06-11T08:19:06Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。