論文の概要: On the Expressive Power of GNNs for Boolean Satisfiability

• arxiv url: http://arxiv.org/abs/2602.08745v1
• Date: Mon, 09 Feb 2026 14:48:16 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-02-10 20:26:25.306074
• Title: On the Expressive Power of GNNs for Boolean Satisfiability
• Title（参考訳）: ブール満足度のためのGNNの表現力について
• Authors: Saku Peltonen, Roger Wattenhofer,
• Abstract要約: ブール満足度(SAT)解決のためのグラフニューラルネットワークの表現力の解析 より高階の WL に対する不連続性は,変数を逐次設定する WL 有界な解法に対して,実用上の制限を負うことを示す。 この結果から, ランダムなインスタンスは概ね区別可能であるが, 満足な割り当てを予測するためには, 工業的インスタンスの方が表現力が高いことが示唆された。
• 参考スコア（独自算出の注目度）: 34.662213518530315
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Machine learning approaches to solving Boolean Satisfiability (SAT) aim to replace handcrafted heuristics with learning-based models. Graph Neural Networks have emerged as the main architecture for SAT solving, due to the natural graph representation of Boolean formulas. We analyze the expressive power of GNNs for SAT solving through the lens of the Weisfeiler-Leman (WL) test. As our main result, we prove that the full WL hierarchy cannot, in general, distinguish between satisfiable and unsatisfiable instances. We show that indistinguishability under higher-order WL carries over to practical limitations for WL-bounded solvers that set variables sequentially. We further study the expressivity required for several important families of SAT instances, including regular, random and planar instances. To quantify expressivity needs in practice, we conduct experiments on random instances from the G4SAT benchmark and industrial instances from the International SAT Competition. Our results suggest that while random instances are largely distinguishable, industrial instances often require more expressivity to predict a satisfying assignment.
• Abstract（参考訳）: Boolean Satisfiability(SAT)を解決する機械学習アプローチは、手作りのヒューリスティックを学習ベースモデルに置き換えることを目的としている。 グラフニューラルネットワークは、ブール公式の自然なグラフ表現のため、SAT解決の主要なアーキテクチャとして登場した。 Wesfeiler-Leman (WL) テストのレンズを用いて, SAT問題解決のためのGNNの表現力を解析した。 我々の主な結果として、完全なWL階層は、一般的に、満足できるインスタンスと不満足なインスタンスを区別できないことを証明している。 より高階の WL 下での不連続性は、変数を逐次設定する WL 有界な解法に対して、実用的な制限を負うことを示す。 さらに、正規、ランダム、平面のインスタンスを含むSATインスタンスのいくつかの重要なファミリーに必要とされる表現性について検討する。 本研究は,G4SATベンチマークと国際SATコンペティションの産業用インスタンスからランダムなインスタンスに関する実験を行う。 この結果から, ランダムなインスタンスは概ね区別可能であるが, 満足な割り当てを予測するためには, 工業的インスタンスの方が表現力が高いことが示唆された。

関連論文リスト

• GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection [45.222591894755105]
  インスタンスの3部グラフ表現に基づくSATソルバ自動選択のための新しいアプローチであるGraSSを提案する。 我々は、新しいノードの特徴設計のようなドメイン固有の決定でグラフ表現を豊かにします。 生の表現とドメイン固有の選択の組み合わせが実行時の改善につながることを実証する。
  論文  参考訳（メタデータ） (2024-05-17T18:00:50Z)
• 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)
• 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)
• 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)
• Generalization of Neural Combinatorial Solvers Through the Lens of Adversarial Robustness [68.97830259849086]
  ほとんどのデータセットは単純なサブプロブレムのみをキャプチャし、おそらくは突発的な特徴に悩まされる。 本研究では, 局所的な一般化特性である対向ロバスト性について検討し, 厳密でモデル固有な例と突発的な特徴を明らかにする。 他のアプリケーションとは異なり、摂動モデルは知覚できないという主観的な概念に基づいて設計されているため、摂動モデルは効率的かつ健全である。 驚くべきことに、そのような摂動によって、十分に表現力のあるニューラルソルバは、教師あり学習で共通する正確さと悪質さのトレードオフの限界に悩まされない。
  論文  参考訳（メタデータ） (2021-10-21T07:28:11Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
  論文  参考訳（メタデータ） (2021-07-15T04:47:35Z)
• Improving Graph Neural Network Expressivity via Subgraph Isomorphism Counting [63.04999833264299]
  グラフサブストラクチャネットワーク(GSN)は,サブストラクチャエンコーディングに基づくトポロジ的に認識可能なメッセージパッシング方式である。 Wesfeiler-Leman (WL) グラフ同型テストよりも厳密に表現可能であることを示す。 グラフ分類と回帰タスクについて広範囲に評価を行い、様々な実世界の環境において最先端の結果を得る。
  論文  参考訳（メタデータ） (2020-06-16T15:30:31Z)

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

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