論文の概要: GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection

• arxiv url: http://arxiv.org/abs/2405.11024v1
• Date: Fri, 17 May 2024 18:00:50 GMT
• ステータス: 処理完了
• システム内更新日: 2024-05-21 19:46:29.524508
• Title: GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection
• Title（参考訳）: GraSS:SATソルバー選択のための専門知識とグラフニューラルネットワークを組み合わせる
• Authors: Zhanguang Zhang, Didier Chetelat, Joseph Cotnareanu, Amur Ghose, Wenyi Xiao, Hui-Ling Zhen, Yingxue Zhang, Jianye Hao, Mark Coates, Mingxuan Yuan,
• Abstract要約: インスタンスの3部グラフ表現に基づくSATソルバ自動選択のための新しいアプローチであるGraSSを提案する。 我々は、新しいノードの特徴設計のようなドメイン固有の決定でグラフ表現を豊かにします。 生の表現とドメイン固有の選択の組み合わせが実行時の改善につながることを実証する。
• 参考スコア（独自算出の注目度）: 45.222591894755105
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Boolean satisfiability (SAT) problems are routinely solved by SAT solvers in real-life applications, yet solving time can vary drastically between solvers for the same instance. This has motivated research into machine learning models that can predict, for a given SAT instance, which solver to select among several options. Existing SAT solver selection methods all rely on some hand-picked instance features, which are costly to compute and ignore the structural information in SAT graphs. In this paper we present GraSS, a novel approach for automatic SAT solver selection based on tripartite graph representations of instances and a heterogeneous graph neural network (GNN) model. While GNNs have been previously adopted in other SAT-related tasks, they do not incorporate any domain-specific knowledge and ignore the runtime variation introduced by different clause orders. We enrich the graph representation with domain-specific decisions, such as novel node feature design, positional encodings for clauses in the graph, a GNN architecture tailored to our tripartite graphs and a runtime-sensitive loss function. Through extensive experiments, we demonstrate that this combination of raw representations and domain-specific choices leads to improvements in runtime for a pool of seven state-of-the-art solvers on both an industrial circuit design benchmark, and on instances from the 20-year Anniversary Track of the 2022 SAT Competition.
• Abstract（参考訳）: SAT問題(Boolean satisfiability)は、SATソルバによって現実のアプリケーションで日常的に解決されるが、同じインスタンスのソルバ間では時間が大きく異なることがある。 これは、特定のSATインスタンスに対して、いくつかの選択肢の中からソルバを選択することができる機械学習モデルの研究を動機付けている。 既存のSATソルバ選択手法はすべて、SATグラフの構造情報を計算し無視するのにコストがかかる手書きのインスタンス機能に依存している。 本稿では、インスタンスの3部グラフ表現に基づくSATソルバ自動選択のための新しいアプローチであるGraSSと、異種グラフニューラルネットワーク(GNN)モデルを提案する。 GNNは以前、SAT関連のタスクで採用されていたが、ドメイン固有の知識は一切含みておらず、異なる節順で導入されたランタイムのバリエーションを無視している。 我々は、新しいノードの特徴設計、グラフ内の節の位置エンコーディング、三部グラフに適したGNNアーキテクチャ、実行時依存の損失関数など、ドメイン固有の決定でグラフ表現を豊かにする。 2022 SATコンペティションの20年記念トラックの事例と産業用回路設計ベンチマークの両方において,この生の表現とドメイン固有の選択の組み合わせが,7つの最先端ソルバプールのランタイム改善につながることを実証した。

関連論文リスト

• Machine Learning for SAT: Restricted Heuristics and New Graph Representations [0.8870188183999854]
  SATは、自動スケジューリングを含む多くのアプリケーションにおいて、基本的なNP完全問題である。 大きなインスタンスを解決するためには、SATソルバは、例えばDPLLとCDCLソルバの分岐変数を選択するなど、ブールアンに依存する必要がある。 我々は、訓練されたMLモデルでいくつかの初期ステップを行い、古典的なランタイムに制御をリリースする戦略を提案する。
  論文  参考訳（メタデータ） (2023-07-18T10:46:28Z)
• 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)
• 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)
• 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)
• Learning on Attribute-Missing Graphs [66.76561524848304]
  部分ノードのみの属性が利用できるグラフがあり、他の属性が完全に欠落している可能性がある。 一般的なGNNを含む既存のグラフ学習手法では、満足な学習性能が得られない。 我々は,属性欠落グラフのための構造属性変換器(SAT)と呼ばれる新しい分布マッチングベースGNNを開発した。
  論文  参考訳（メタデータ） (2020-11-03T11:09:52Z)
• Evaluating Logical Generalization in Graph Neural Networks [59.70452462833374]
  グラフニューラルネットワーク(GNN)を用いた論理一般化の課題について検討する。 ベンチマークスイートであるGraphLogでは、学習アルゴリズムが異なる合成論理でルール誘導を実行する必要がある。 モデルが一般化し適応する能力は、トレーニング中に遭遇する論理規則の多様性によって強く決定される。
  論文  参考訳（メタデータ） (2020-03-14T05:45:55Z)

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

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