論文の概要: Improving SAT Solving with Graph Neural Networks

• arxiv url: http://arxiv.org/abs/2110.14053v1
• Date: Tue, 26 Oct 2021 22:08:22 GMT
• ステータス: 処理完了
• システム内更新日: 2021-10-28 12:49:42.385820
• Title: Improving SAT Solving with Graph Neural Networks
• Title（参考訳）: グラフニューラルネットワークによるSAT解決の改善
• Authors: Wenxi Wang, Yang Hu, Mohit Tiwari, Sarfraz Khurshid, Kenneth McMillan, Risto Miikkulainen
• Abstract要約: 主要なストリーム SAT ソルバは Conflict-Driven Clause Learning (CDCL) アルゴリズムに基づいている。 グラフニューラルネット(GNN)による予測を通した可変分岐の改善によるCDCL SATソルバの強化を目的とした最近の研究 本稿では,(1)重要な変数と節の予測を動的分岐と組み合わせることで,より効果的なハイブリッド分岐戦略を実現できる,(2)SAT解決開始前の予測に対してのみ1回だけニューラルネットワークモデルに問い合わせる,という2つの知見に基づくNeuroCombというアプローチを提案する。
• 参考スコア（独自算出の注目度）: 21.136261444658135
• 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. Despite the remarkable success of modern SAT solvers, scalability still remains a challenge. Main stream modern SAT solvers are based on the Conflict-Driven Clause Learning (CDCL) algorithm. Recent work aimed to enhance CDCL SAT solvers by improving its variable branching heuristics through predictions generated by Graph Neural Networks (GNNs). However, so far this approach either has not made solving more effective, or has required frequent online accesses to substantial GPU resources. Aiming to make GNN improvements practical, this paper proposes an approach called NeuroComb, which builds on two insights: (1) predictions of important variables and clauses can be combined with dynamic branching into a more effective hybrid branching strategy, and (2) it is sufficient to query the neural model only once for the predictions before the SAT solving starts. Implemented as an enhancement to the classic MiniSat solver, NeuroComb allowed it to solve 18.5% more problems on the recent SATCOMP-2020 competition problem set. NeuroComb is therefore a practical approach to improving SAT solving through modern machine learning.
• Abstract（参考訳）: 提案的満足度(SAT)は、計画、検証、セキュリティなど、多くの研究分野に影響を与えるNP完全問題である。 現代的なSATソルバの顕著な成功にもかかわらず、スケーラビリティは依然として課題である。 主要なストリーム SAT ソルバは Conflict-Driven Clause Learning (CDCL) アルゴリズムに基づいている。 グラフニューラルネットワーク(gnns)による予測による可変分岐ヒューリスティックの改善によるcdcl satソルバの向上を目的とした最近の研究 しかし、これまでのところこのアプローチは、解決をより効果的にしないか、あるいは大量のgpuリソースへの頻繁にオンラインアクセスを必要としていた。 本論文はgnnの改善を実用的にするためのアプローチとして,(1)重要な変数と節の予測を,より効果的な分岐戦略に動的分岐と組み合わせることが可能であり,(2)sat解の開始前に1回だけニューラルネットワークに問い合わせるだけで十分である,という2つの洞察に基づくneurocombを提案する。 古典的なMiniSatソルバの強化として実装されたNeuroCombは、最近のSATCOMP-2020の競合問題の18.5%の問題を解決した。 それゆえNeuroCombは、現代的な機械学習によるSAT問題解決のための実践的なアプローチである。

関連論文リスト

• Self-Satisfied: An end-to-end framework for SAT generation and prediction [0.7340017786387768]
  高速SAT問題生成のためのハードウェアアクセラレーションアルゴリズムと幾何SAT符号化を導入する。 これらの進歩により、何千もの変数と数万の節でSAT問題へのアプローチをスケールできます。 私たちの研究の基本的な側面は、SATデータの本質と、機械学習モデルのトレーニングに適合する可能性に関するものです。
  論文  参考訳（メタデータ） (2024-10-18T22:25:54Z)
• LinSATNet: The Positive Linear Satisfiability Neural Networks [116.65291739666303]
  本稿では,ニューラルネットワークに人気の高い正の線形満足度を導入する方法について検討する。 本稿では,古典的なシンクホーンアルゴリズムを拡張し,複数の辺分布の集合を共同で符号化する,最初の微分可能満足層を提案する。
  論文  参考訳（メタデータ） (2024-07-18T22:05:21Z)
• GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection [45.222591894755105]
  インスタンスの3部グラフ表現に基づくSATソルバ自動選択のための新しいアプローチであるGraSSを提案する。 我々は、新しいノードの特徴設計のようなドメイン固有の決定でグラフ表現を豊かにします。 生の表現とドメイン固有の選択の組み合わせが実行時の改善につながることを実証する。
  論文  参考訳（メタデータ） (2024-05-17T18:00:50Z)
• 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)
• 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)
• 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)
• Enhancing SAT solvers with glue variable predictions [2.635832975589208]
  我々は、最先端のSATソルバであるCaDiCaLを改良し、SATCOMP 2018とSATRACE 2019のパフォーマンスを改善し、教師付き学習と強化学習によるSHA-1プレイメージアタックのデータセット上でのパフォーマンスを向上する。 我々はこれらの制限に対処し、より単純なネットワークアーキテクチャを用いて、数百万の節を含む大規模産業問題に対してCPU推論を行い、代わりにエミュレート変数を予測する訓練を行い、ラベル付きデータを簡単に生成し、強化学習タスクとして定式化することができる。
  論文  参考訳（メタデータ） (2020-07-06T07:16:49Z)

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

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