論文の概要: Machine Learning Methods in Solving the Boolean Satisfiability Problem
- arxiv url: http://arxiv.org/abs/2203.04755v1
- Date: Wed, 2 Mar 2022 05:14:12 GMT
- ステータス: 処理完了
- システム内更新日: 2022-03-13 13:25:57.623676
- Title: Machine Learning Methods in Solving the Boolean Satisfiability Problem
- Title(参考訳): ブール満足度問題の解法における機械学習手法
- Authors: Wenxuan Guo, Junchi Yan, Hui-Ling Zhen, Xijun Li, Mingxuan Yuan,
Yaohui Jin
- Abstract要約: 本論文は, Boolean satisfiability problem (SAT) を機械学習技術で解くことに関する最近の文献をレビューする。
ML-SATソルバを手作り特徴を持つナイーブ分類器からNeuroSATのような新たなエンド・ツー・エンドSATソルバまで,進化するML-SATソルバについて検討する。
- 参考スコア(独自算出の注目度): 72.21206588430645
- License: http://creativecommons.org/licenses/by-nc-sa/4.0/
- Abstract: This paper reviews the recent literature on solving the Boolean
satisfiability problem (SAT), an archetypal NP-complete problem, with the help
of machine learning techniques. Despite the great success of modern SAT solvers
to solve large industrial instances, the design of handcrafted heuristics is
time-consuming and empirical. Under the circumstances, the flexible and
expressive machine learning methods provide a proper alternative to solve this
long-standing problem. We examine the evolving ML-SAT solvers from naive
classifiers with handcrafted features to the emerging end-to-end SAT solvers
such as NeuroSAT, as well as recent progress on combinations of existing CDCL
and local search solvers with machine learning methods. Overall, solving SAT
with machine learning is a promising yet challenging research topic. We
conclude the limitations of current works and suggest possible future
directions.
- Abstract(参考訳): 本稿では,従来のNP完全問題であるBoolean satisfiability problem(SAT)の解法に関する最近の文献を,機械学習技術の助けを借りてレビューする。
現代のsatソルバが大規模な産業事例を解決したにもかかわらず、手作りのヒューリスティックの設計は時間がかかり、経験的なものである。
このような状況下では、フレキシブルで表現力のある機械学習手法がこの長年の問題を解決するための適切な代替手段を提供する。
ML-SATソルバは,手作りの特徴を持つナイーブな分類器から,NuroSATのような新たなエンドツーエンドSATソルバに至るまでの進化と,既存のCDCLとローカル検索ソルバを機械学習手法で組み合わせた最近の進歩について検討する。
全体として、SATを機械学習で解決することは、有望だが挑戦的な研究トピックである。
我々は現在の作業の限界を結論し、今後の方向性を示唆する。
関連論文リスト
- 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) - Machine Learning Insides OptVerse AI Solver: Design Principles and
Applications [74.67495900436728]
本稿では,Huawei CloudのOpsVerse AIソルバに機械学習(ML)技術を統合するための総合的研究について述べる。
本稿では,実世界の多面構造を反映した生成モデルを用いて,複雑なSATインスタンスとMILPインスタンスを生成する手法を紹介する。
本稿では,解解器性能を著しく向上させる,最先端パラメータチューニングアルゴリズムの導入について詳述する。
論文 参考訳(メタデータ) (2024-01-11T15:02:15Z) - G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networks [7.951021955925275]
グラフニューラルネットワーク(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) - Evolutionary Diversity Optimisation in Constructing Satisfying
Assignments [20.386139395296215]
本稿では,EDOの文脈におけるブール充足可能性問題(SAT)について検討する。
SATは計算機科学において非常に重要であり、KPやTSPといったEDO文献で研究されている他の問題とは異なる。
本稿では,SAT解の集合間の多様性を明示的に最大化するために,よく知られたSATソルバを用いた進化的アルゴリズムを提案する。
論文 参考訳(メタデータ) (2023-05-19T06:26:10Z) - 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) - Transformer-based Machine Learning for Fast SAT Solvers and Logic
Synthesis [63.53283025435107]
CNFベースのSATとMaxSATは論理合成と検証システムの中心である。
そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
論文 参考訳(メタデータ) (2021-07-15T04:47:35Z) - End-to-End Constrained Optimization Learning: A Survey [69.22203885491534]
機械学習アーキテクチャとソルバと最適化手法を統合する作業の調査に焦点を当てている。
これらのアプローチは、問題に対する迅速、近似、構造的、解決策を予測し、論理的推論を可能にする新しいハイブリッド機械学習と最適化手法を開発することを約束します。
論文 参考訳(メタデータ) (2021-03-30T14:19:30Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。