論文の概要: Enhancing SAT solvers with glue variable predictions

• arxiv url: http://arxiv.org/abs/2007.02559v1
• Date: Mon, 6 Jul 2020 07:16:49 GMT
• ステータス: 処理完了
• システム内更新日: 2022-11-13 02:00:09.276179
• Title: Enhancing SAT solvers with glue variable predictions
• Title（参考訳）: グルー変数予測によるSATソルバの強化
• Authors: Jesse Michael Han
• Abstract要約: 我々は、最先端のSATソルバであるCaDiCaLを改良し、SATCOMP 2018とSATRACE 2019のパフォーマンスを改善し、教師付き学習と強化学習によるSHA-1プレイメージアタックのデータセット上でのパフォーマンスを向上する。 我々はこれらの制限に対処し、より単純なネットワークアーキテクチャを用いて、数百万の節を含む大規模産業問題に対してCPU推論を行い、代わりにエミュレート変数を予測する訓練を行い、ラベル付きデータを簡単に生成し、強化学習タスクとして定式化することができる。
• 参考スコア（独自算出の注目度）: 2.635832975589208
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Modern SAT solvers routinely operate at scales that make it impractical to query a neural network for every branching decision. NeuroCore, proposed by Selsam and Bjorner, offered a proof-of-concept that neural networks can still accelerate SAT solvers by only periodically refocusing a score-based branching heuristic. However, that work suffered from several limitations: their modified solvers require GPU acceleration, further ablations showed that they were no better than a random baseline on the SATCOMP 2018 benchmark, and their training target of unsat cores required an expensive data pipeline which only labels relatively easy unsatisfiable problems. We address all these limitations, using a simpler network architecture allowing CPU inference for even large industrial problems with millions of clauses, and training instead to predict {\em glue variables}---a target for which it is easier to generate labelled data, and which can also be formulated as a reinforcement learning task. We demonstrate the effectiveness of our approach by modifying the state-of-the-art SAT solver CaDiCaL, improving its performance on SATCOMP 2018 and SATRACE 2019 with supervised learning and its performance on a dataset of SHA-1 preimage attacks with reinforcement learning.
• Abstract（参考訳）: 現代的なSATソルバは、分岐決定毎にニューラルネットワークに問い合わせる非現実的なスケールで日常的に動作する。 SelsamとBjornerによって提案されたNeuroCoreは、スコアベースの分岐ヒューリスティックを定期的に再フォーカスするだけで、ニューラルネットワークがSATソルバを加速できるという概念実証を提供した。 しかし、その作業にはいくつかの制限があった: 修正されたソルバはGPUアクセラレーションを必要とし、さらなる改善によりSATCOMP 2018ベンチマークのランダムなベースラインに匹敵せず、トレーニング対象の未満足なコアは、比較的容易な問題のみをラベル付けする高価なデータパイプラインを必要とした。 私たちはこれらの制限をすべて解決し、数百万の節を持つ巨大な産業問題に対するcpu推論を可能にするシンプルなネットワークアーキテクチャと、ラベル付きデータの生成が容易で強化学習タスクとしても定式化可能な、"em glue variable" 予測のためのトレーニングを使用しています。 本研究では,最先端のSATソルバであるCaDiCaLを改良し,SATCOMP 2018とSATRACE 2019の性能を改善し,SHA-1プレイメージ攻撃と強化学習を併用したデータセット上での有効性を示す。

関連論文リスト

• Self-Satisfied: An end-to-end framework for SAT generation and prediction [0.7340017786387768]
  高速SAT問題生成のためのハードウェアアクセラレーションアルゴリズムと幾何SAT符号化を導入する。 これらの進歩により、何千もの変数と数万の節でSAT問題へのアプローチをスケールできます。 私たちの研究の基本的な側面は、SATデータの本質と、機械学習モデルのトレーニングに適合する可能性に関するものです。
  論文  参考訳（メタデータ） (2024-10-18T22:25:54Z)
• Machine Learning for SAT: Restricted Heuristics and New Graph Representations [0.8870188183999854]
  SATは、自動スケジューリングを含む多くのアプリケーションにおいて、基本的なNP完全問題である。 大きなインスタンスを解決するためには、SATソルバは、例えばDPLLとCDCLソルバの分岐変数を選択するなど、ブールアンに依存する必要がある。 我々は、訓練されたMLモデルでいくつかの初期ステップを行い、古典的なランタイムに制御をリリースする戦略を提案する。
  論文  参考訳（メタデータ） (2023-07-18T10:46:28Z)
• SPIDE: A Purely Spike-based Method for Training Feedback Spiking Neural Networks [56.35403810762512]
  イベントベースの計算を伴うスパイキングニューラルネットワーク(SNN)は、ニューロモルフィックハードウェアにおけるエネルギー効率の高い応用のために、脳にインスパイアされたモデルを約束している。 本研究では,最近提案されたトレーニング手法を拡張した平衡状態(SPIDE)に対するスパイクに基づく暗黙差分法について検討した。
  論文  参考訳（メタデータ） (2023-02-01T04:22:59Z)
• Intelligence Processing Units Accelerate Neuromorphic Learning [52.952192990802345]
  スパイキングニューラルネットワーク(SNN)は、エネルギー消費と遅延の観点から、桁違いに改善されている。 我々は、カスタムSNN PythonパッケージsnnTorchのIPU最適化リリースを提示する。
  論文  参考訳（メタデータ） (2022-11-19T15:44:08Z)
• NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks [13.185943308470286]
  提案的満足度(SAT)は、計画、検証、セキュリティなど、多くの研究分野に影響を与えるNP完全問題である。 グラフニューラルネットワーク(GNN)を用いたCDCL SATソルバの高速化に向けた最近の研究 本稿では,(1)CDCL SATの解法に必要不可欠である変数の位相(すなわち値)を予測すること,(2)SATの解法開始前に1回だけニューラルネットワークに問い合わせること,の2つの知見に基づくNeuroBackという手法を提案する。
  論文  参考訳（メタデータ） (2021-10-26T22:08:22Z)
• Adaptive Anomaly Detection for Internet of Things in Hierarchical Edge Computing: A Contextual-Bandit Approach [81.5261621619557]
  階層エッジコンピューティング(HEC)を用いた適応型異常検出手法を提案する。 まず,複雑性を増した複数のDNNモデルを構築し,それぞれを対応するHEC層に関連付ける。 そこで我々は、文脈帯域問題として定式化され、強化学習ポリシーネットワークを用いて解決される適応モデル選択スキームを設計する。
  論文  参考訳（メタデータ） (2021-08-09T08:45:47Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
  論文  参考訳（メタデータ） (2021-07-15T04:47:35Z)
• Goal-Aware Neural SAT Solver [2.609784101826762]
  現代のニューラルネットワークは問題に関する情報を取得し、入力値からのみ出力を算出する。 我々は、必ずしも最適ではなく、クエリメカニズムで拡張することで、ネットワークの性能を大幅に改善できると主張している。 本稿では、QuerySATと呼ばれるクエリ機構を備えたニューラルSATソルバを提案し、幅広いSATタスクにおいてニューラルベースラインよりも優れていることを示す。
  論文  参考訳（メタデータ） (2021-06-14T04:51:24Z)
• S2-BNN: Bridging the Gap Between Self-Supervised Real and 1-bit Neural Networks via Guided Distribution Calibration [74.5509794733707]
  本研究では, 実数値から, 最終予測分布上のバイナリネットワークへの誘導型学習パラダイムを提案する。 提案手法は,bnn上で5.515%の絶対利得で,単純なコントラスト学習ベースラインを向上できる。 提案手法は、単純なコントラスト学習ベースラインよりも大幅に改善され、多くの主流教師付きBNN手法に匹敵する。
  論文  参考訳（メタデータ） (2021-02-17T18:59:28Z)
• GradInit: Learning to Initialize Neural Networks for Stable and Efficient Training [59.160154997555956]
  ニューラルネットワークを初期化するための自動化およびアーキテクチャ手法であるgradinitを提案する。 各ネットワーク層の分散は、SGDまたはAdamの単一ステップが最小の損失値をもたらすように調整される。 また、学習率のウォームアップを伴わずに、オリジナルのPost-LN Transformerを機械翻訳用にトレーニングすることもできる。
  論文  参考訳（メタデータ） (2021-02-16T11:45:35Z)

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

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