論文の概要: Addressing Variable Dependency in GNN-based SAT Solving
- arxiv url: http://arxiv.org/abs/2304.08738v1
- Date: Tue, 18 Apr 2023 05:33:33 GMT
- ステータス: 処理完了
- システム内更新日: 2023-04-19 16:04:32.147752
- Title: Addressing Variable Dependency in GNN-based SAT Solving
- Title(参考訳): GNNに基づくSATソルビングにおける可変依存性の対応
- Authors: Zhiyuan Yan, Min Li, Zhengyuan Shi, Wenjie Zhang, Yingcong Chen and
Hongce Zhang
- Abstract要約: 本稿では、繰り返しニューラルネットワークを統合したGNNベースのアーキテクチャであるAsymSATを提案し、可変代入に対する依存予測を生成する。
実験結果から,大規模テストセット上でのSATインスタンスの解数を改善することにより,依存変数予測がGNN方式の解解能力を拡張できることが示唆された。
- 参考スコア(独自算出の注目度): 19.38746341365531
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Boolean satisfiability problem (SAT) is fundamental to many applications.
Existing works have used graph neural networks (GNNs) for (approximate) SAT
solving. Typical GNN-based end-to-end SAT solvers predict SAT solutions
concurrently. We show that for a group of symmetric SAT problems, the
concurrent prediction is guaranteed to produce a wrong answer because it
neglects the dependency among Boolean variables in SAT problems. % We propose
AsymSAT, a GNN-based architecture which integrates recurrent neural networks to
generate dependent predictions for variable assignments. The experiment results
show that dependent variable prediction extends the solving capability of the
GNN-based method as it improves the number of solved SAT instances on large
test sets.
- Abstract(参考訳): Boolean satisfiability problem (SAT)は、多くのアプリケーションに基本的な問題である。
既存の研究では(近似)SAT解決にグラフニューラルネットワーク(GNN)が使用されている。
典型的なGNNベースのエンドツーエンドSATソルバはSATソリューションを同時に予測する。
対称SAT問題の群では,SAT問題におけるブール変数間の依存性を無視するため,同時予測が間違った解を生成することが保証されている。
%) のasymsatを提案する。これはgnnベースのアーキテクチャで、再帰ニューラルネットワークを統合し、変数割り当てに対する依存予測を生成する。
実験結果から,大規模テストセット上でのSATインスタンスの解数を改善することにより,依存変数予測がGNN方式の解解能力を拡張できることが示唆された。
関連論文リスト
- Decomposing Hard SAT Instances with Metaheuristic Optimization [52.03315747221343]
分解硬度(d硬度)の概念を導入する。
d-硬度が$C$ w.r.tの硬度の推定値を示すことを示す。
論文 参考訳(メタデータ) (2023-12-16T12:44:36Z) - G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural
Networks [8.936151867825112]
グラフニューラルネットワーク(GNN)は、ブール満足度問題(SAT)を解決するための有望なアプローチとして登場した。
G4SATBenchは、GNNベースのSATソルバの包括的な評価フレームワークを確立する最初のベンチマーク研究である。
GNNベースのSATソルバの性能について,実験結果から貴重な知見を得た。
論文 参考訳(メタデータ) (2023-09-29T02:50:57Z) - Machine Learning for SAT: Restricted Heuristics and New Graph
Representations [0.8870188183999854]
SATは、自動スケジューリングを含む多くのアプリケーションにおいて、基本的なNP完全問題である。
大きなインスタンスを解決するためには、SATソルバは、例えばDPLLとCDCLソルバの分岐変数を選択するなど、ブールアンに依存する必要がある。
我々は、訓練されたMLモデルでいくつかの初期ステップを行い、古典的なランタイムに制御をリリースする戦略を提案する。
論文 参考訳(メタデータ) (2023-07-18T10:46:28Z) - A hybrid Quantum proposal to deal with 3-SAT problem [75.38606213726906]
本稿では,3SAT問題を解くためのハイブリッド量子コンピューティング戦略について述べる。
この近似の性能は、量子コンピューティングの観点から3-SATを扱う際に、一連の代表的なシナリオで検証されている。
論文 参考訳(メタデータ) (2023-06-07T12:19:22Z) - Amplitude amplification-inspired QAOA: Improving the success probability
for solving 3SAT [55.78588835407174]
振幅増幅アルゴリズムは、可変代入を満たすために非構造化探索に適用することができる。
Quantum Approximate Optimization Algorithm (QAOA)は、ノイズのある中間量子デバイスのための3SATを解くための有望な候補である。
振幅増幅によるQAOAの変種を導入し、3SATの成功確率を改善する。
論文 参考訳(メタデータ) (2023-03-02T11:52:39Z) - 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) - SATformer: Transformer-Based UNSAT Core Learning [0.0]
本稿では,SAT 問題に対する Transformer ベースのアプローチである SATformer を紹介する。
SATformerは、問題を直接解決するのではなく、満足できないことに焦点をあてて、その問題を反対方向からアプローチする。
SATformerは、シングルビットの満足度結果と最小限の不満コアを使用して、マルチタスク学習アプローチでトレーニングされる。
実験の結果,SATformerは既存のソルバのランタイムを平均21.33%削減できることがわかった。
論文 参考訳(メタデータ) (2022-09-02T11:17:39Z) - 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) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。