論文の概要: G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networks

• arxiv url: http://arxiv.org/abs/2309.16941v2
• Date: Fri, 10 May 2024 21:45:26 GMT
• ステータス: 処理完了
• システム内更新日: 2024-05-15 01:12:47.414768
• 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ソルバの性能に関する貴重な知見を提供する。
• 参考スコア（独自算出の注目度）: 7.951021955925275
• 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. Our codebase is available at https://github.com/zhaoyu-li/G4SATBench.
• Abstract（参考訳）: グラフニューラルネットワーク(GNN)は先頃、従来のバックトラックやローカルサーチSATソルバに代わる選択肢を提供する、Boolean Satisfiability Problem(SAT)を解決するための有望なアプローチとして登場した。 しかし、この分野の文献が増えているにもかかわらず、既存のアプローチを評価し比較するための統一データセットと公正なベンチマークが存在しないことは注目すべきである。 G4SATBenchは、GNNベースのSATソルバの総合的な評価フレームワークを確立する最初のベンチマーク研究である。 G4SATBenchでは,3つの難易度を持つ7つの問題からなるSATデータセットの大規模かつ多種多様な集合を慎重にキュレートし,様々な予測タスク,学習目標,推論アルゴリズムにまたがる広範囲なGNNモデルをベンチマークする。 学習能力を探究し,GNNベースのSATソルバの強みと限界を理解するために,それらの解法とサーチベースのSATソルバのヒューリスティックスを比較する。 実験結果から,既存のGNNモデルでは,局所探索に類似した解法を効果的に学べるが,潜在空間における探索のバックトラックを学べない可能性が示唆された。 私たちのコードベースはhttps://github.com/zhaoyu-li/G4SATBench.comで公開されています。

関連論文リスト

• GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection [45.222591894755105]
  インスタンスの3部グラフ表現に基づくSATソルバ自動選択のための新しいアプローチであるGraSSを提案する。 我々は、新しいノードの特徴設計のようなドメイン固有の決定でグラフ表現を豊かにします。 生の表現とドメイン固有の選択の組み合わせが実行時の改善につながることを実証する。
  論文  参考訳（メタデータ） (2024-05-17T18:00:50Z)
• Benchmarking ChatGPT on Algorithmic Reasoning [58.50071292008407]
  GNN向けに設計されたCLRSベンチマークスイートからChatGPTのアルゴリズム問題を解く能力を評価する。 ChatGPTは、Pythonを使ってこれらの問題を解決することで、専門家のGNNモデルより優れています。
  論文  参考訳（メタデータ） (2024-04-04T13:39:06Z)
• Using deep learning to construct stochastic local search SAT solvers with performance bounds [0.0]
  グラフニューラルネットワークを用いてオーラクルを訓練し、2つのSLSソルバ上で、様々な難易度を持つランダムSATインスタンス上でそれらを評価する。 GNNベースのオラクルへのアクセスは,両者のパフォーマンスを著しく向上させることがわかった。
  論文  参考訳（メタデータ） (2023-09-20T16:27:52Z)
• 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 [11.139131079925113]
  W2SATは、現実世界/産業インスタンスから固有の構造と特性を学ぶことによってSAT式を生成するフレームワークである。 Weighted Literal Incidence Graph (WLIG)と呼ばれる新しいSAT表現を導入する。 WLIGからSAT問題への復号化は、新しい丘登り最適化法で重なり合う斜角を見つけることをモデル化する。
  論文  参考訳（メタデータ） (2023-02-01T06:30:41Z)
• 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.185943308470286]
  提案的満足度(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)

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

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