論文の概要: Using deep learning to construct stochastic local search SAT solvers with performance bounds

• arxiv url: http://arxiv.org/abs/2309.11452v1
• Date: Wed, 20 Sep 2023 16:27:52 GMT
• ステータス: 処理完了
• システム内更新日: 2023-09-21 15:31:49.497972
• Title: Using deep learning to construct stochastic local search SAT solvers with performance bounds
• Title（参考訳）: 深層学習を用いた性能境界付き確率的局所探索SATソルバの構築
• Authors: Maximilian Kramer, Paul Boes
• Abstract要約: グラフニューラルネットワークを用いてオーラクルを訓練し、2つのSLSソルバ上で、様々な難易度を持つランダムSATインスタンス上でそれらを評価する。 GNNベースのオラクルへのアクセスは,両者のパフォーマンスを著しく向上させることがわかった。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The Boolean Satisfiability problem (SAT) is the most prototypical NP-complete problem and of great practical relevance. One important class of solvers for this problem are stochastic local search (SLS) algorithms that iteratively and randomly update a candidate assignment. Recent breakthrough results in theoretical computer science have established sufficient conditions under which SLS solvers are guaranteed to efficiently solve a SAT instance, provided they have access to suitable "oracles" that provide samples from an instance-specific distribution, exploiting an instance's local structure. Motivated by these results and the well established ability of neural networks to learn common structure in large datasets, in this work, we train oracles using Graph Neural Networks and evaluate them on two SLS solvers on random SAT instances of varying difficulty. We find that access to GNN-based oracles significantly boosts the performance of both solvers, allowing them, on average, to solve 17% more difficult instances (as measured by the ratio between clauses and variables), and to do so in 35% fewer steps, with improvements in the median number of steps of up to a factor of 8. As such, this work bridges formal results from theoretical computer science and practically motivated research on deep learning for constraint satisfaction problems and establishes the promise of purpose-trained SAT solvers with performance guarantees.
• Abstract（参考訳）: ブール満足度問題(SAT)は最も原始的なNP完全問題であり、非常に実践的な妥当性がある。 この問題に対する重要な解法の一つは、候補の割り当てを反復的かつランダムに更新する確率的局所探索(sls)アルゴリズムである。 理論計算機科学における最近の画期的な成果は、SLSソルバがSATインスタンスを効率的に解くことが保証される十分な条件を確立している。 これらの結果と、大規模なデータセットで共通構造を学習するニューラルネットワークの確立した能力により、我々はグラフニューラルネットワークを用いてオークルを訓練し、様々な難易度を持つランダムSATインスタンス上で2つのSLSソルバ上で評価する。 GNNベースのオラクルへのアクセスは、両者のパフォーマンスを大幅に向上させ、平均して17%の難解なインスタンス(節と変数の比率によって測定される)を解決し、35%のステップで解決できるようにし、最大8.5%までのステップの中央値の改善を実現した。 そこで本研究は, 理論計算機科学の正式な成果と, 制約満足度問題に対するディープラーニング研究の実践的動機を橋渡しし, 性能保証を伴う目的学習SATソルバの約束を確立する。

関連論文リスト

• torchmSAT: A GPU-Accelerated Approximation To The Maximum Satisfiability Problem [1.5850859526672516]
  最大満足度問題(MaxSAT)の解を近似できる単一の微分可能関数を導出する。 我々は,我々の微分可能な関数をモデル化する新しいニューラルネットワークアーキテクチャを提案し,バックプロパゲーションを用いてMaxSATを段階的に解く。
  論文  参考訳（メタデータ） (2024-02-06T02:33:00Z)
• G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networks [7.951021955925275]
  グラフニューラルネットワーク(GNN)は、ブール満足度問題(SAT)を解決するための有望なアプローチとして登場した。 G4SATBenchは、GNNベースのSATソルバの包括的な評価フレームワークを確立する最初のベンチマーク研究である。 本結果は,GNNベースのSATソルバの性能に関する貴重な知見を提供する。
  論文  参考訳（メタデータ） (2023-09-29T02:50:57Z)
• W2SAT: Learning to generate SAT instances from Weighted Literal Incidence Graphs [11.139131079925113]
  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)
• Simple Stochastic and Online Gradient DescentAlgorithms for Pairwise Learning [65.54757265434465]
  ペアワイズ学習(Pairwise learning)とは、損失関数がペアインスタンスに依存するタスクをいう。 オンライン降下(OGD)は、ペアワイズ学習でストリーミングデータを処理する一般的なアプローチである。 本稿では,ペアワイズ学習のための手法について,シンプルでオンラインな下降を提案する。
  論文  参考訳（メタデータ） (2021-11-23T18:10:48Z)
• Generalization of Neural Combinatorial Solvers Through the Lens of Adversarial Robustness [68.97830259849086]
  ほとんどのデータセットは単純なサブプロブレムのみをキャプチャし、おそらくは突発的な特徴に悩まされる。 本研究では, 局所的な一般化特性である対向ロバスト性について検討し, 厳密でモデル固有な例と突発的な特徴を明らかにする。 他のアプリケーションとは異なり、摂動モデルは知覚できないという主観的な概念に基づいて設計されているため、摂動モデルは効率的かつ健全である。 驚くべきことに、そのような摂動によって、十分に表現力のあるニューラルソルバは、教師あり学習で共通する正確さと悪質さのトレードオフの限界に悩まされない。
  論文  参考訳（メタデータ） (2021-10-21T07:28:11Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
  論文  参考訳（メタデータ） (2021-07-15T04:47:35Z)
• Fitting the Search Space of Weight-sharing NAS with Graph Convolutional Networks [100.14670789581811]
  サンプルサブネットワークの性能に適合するグラフ畳み込みネットワークを訓練する。 この戦略により、選択された候補集合において、より高いランク相関係数が得られる。
  論文  参考訳（メタデータ） (2020-04-17T19:12:39Z)

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

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