論文の概要: 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方式の解解能力を拡張できることが示唆された。
関連論文リスト
- Self-Satisfied: An end-to-end framework for SAT generation and prediction [0.7340017786387768]
高速SAT問題生成のためのハードウェアアクセラレーションアルゴリズムと幾何SAT符号化を導入する。
これらの進歩により、何千もの変数と数万の節でSAT問題へのアプローチをスケールできます。
私たちの研究の基本的な側面は、SATデータの本質と、機械学習モデルのトレーニングに適合する可能性に関するものです。
論文 参考訳(メタデータ) (2024-10-18T22:25:54Z) - GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection [45.222591894755105]
インスタンスの3部グラフ表現に基づくSATソルバ自動選択のための新しいアプローチであるGraSSを提案する。
我々は、新しいノードの特徴設計のようなドメイン固有の決定でグラフ表現を豊かにします。
生の表現とドメイン固有の選択の組み合わせが実行時の改善につながることを実証する。
論文 参考訳(メタデータ) (2024-05-17T18:00:50Z) - 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 [7.951021955925275]
グラフニューラルネットワーク(GNN)は、ブール満足度問題(SAT)を解決するための有望なアプローチとして登場した。
G4SATBenchは、GNNベースのSATソルバの包括的な評価フレームワークを確立する最初のベンチマーク研究である。
本結果は,GNNベースのSATソルバの性能に関する貴重な知見を提供する。
論文 参考訳(メタデータ) (2023-09-29T02:50:57Z) - A hybrid Quantum proposal to deal with 3-SAT problem [75.38606213726906]
本稿では,3SAT問題を解くためのハイブリッド量子コンピューティング戦略について述べる。
この近似の性能は、量子コンピューティングの観点から3-SATを扱う際に、一連の代表的なシナリオで検証されている。
論文 参考訳(メタデータ) (2023-06-07T12:19:22Z) - 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) - Transformer-based Machine Learning for Fast SAT Solvers and Logic
Synthesis [63.53283025435107]
CNFベースのSATとMaxSATは論理合成と検証システムの中心である。
そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
論文 参考訳(メタデータ) (2021-07-15T04:47:35Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。