論文の概要: ML Supported Predictions for SAT Solvers Performance

• arxiv url: http://arxiv.org/abs/2112.09438v1
• Date: Fri, 17 Dec 2021 11:17:29 GMT
• ステータス: 処理完了
• システム内更新日: 2021-12-20 13:58:45.124087
• Title: ML Supported Predictions for SAT Solvers Performance
• Title（参考訳）: SATソリューションのパフォーマンス予測のためのMLサポート
• Authors: A.-M. Leventi-Peetz, J\"org-Volker Peetz, Martina Rohde
• Abstract要約: 内部のソルバランタイムパラメータが収集され、分析されている。 問題解決者の終了動作のバイナリ分類のための機械学習モデルが作成されている。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: In order to classify the indeterministic termination behavior of the open source SAT solver CryptoMiniSat in multi-threading mode while processing hard to solve boolean satisfiability problem instances, internal solver runtime parameters have been collected and analyzed. A subset of these parameters has been selected and employed as features vector to successfully create a machine learning model for the binary classification of the solver's termination behavior with any single new solving run of a not yet solved instance. The model can be used for the early estimation of a solving attempt as belonging or not belonging to the class of candidates with good chances for a fast termination. In this context a combination of active profiles of runtime characteristics appear to mirror the influence of the solver's momentary heuristics on the immediate quality of the solver's resolution process. Because runtime parameters of already the first two solving iterations are enough to forecast termination of the attempt with good success scores, the results of the present work deliver a promising basis which can be further developed in order to enrich CryptoMiniSat or generally any modern SAT solver with AI abilities.
• Abstract（参考訳）: オープンソースのSATソルバCryptoMiniSatの非決定論的終了動作をマルチスレッドモードで分類するために,ブール整合性問題インスタンスの処理を困難にし,内部ソルバ実行パラメータを収集し解析した。 これらのパラメータのサブセットが選択され、特徴ベクトルとして採用され、未解決のインスタンスの1つの新しい解決実行で、ソルバの終了動作のバイナリ分類のための機械学習モデルの作成に成功している。 このモデルは、迅速な終了確率の高い候補のクラスに属するか否かに関わらず、解決の試みを早期に見積もることができる。 この文脈では、ランタイム特性のアクティブプロファイルの組み合わせは、ソルバの瞬間的ヒューリスティックがソルバの解決プロセスの即時品質に与える影響を反映しているように見える。 最初の2つの解決イテレーションのランタイムパラメータは、良好な成功スコアで試行の終了を予測するのに十分であるため、本研究の結果は、CryptoMiniSatやAI能力を備えた現代のSATソルバの強化のために、さらに発展できる有望な基礎を提供する。

関連論文リスト

• Accelerated zero-order SGD under high-order smoothness and overparameterized regime [79.85163929026146]
  凸最適化問題を解くための新しい勾配のないアルゴリズムを提案する。 このような問題は医学、物理学、機械学習で発生する。 両種類の雑音下で提案アルゴリズムの収束保証を行う。
  論文  参考訳（メタデータ） (2024-11-21T10:26:17Z)
• Self-Supervised Learning of Iterative Solvers for Constrained Optimization [0.0]
  制約付き最適化のための学習型反復解法を提案する。 解法を特定のパラメトリック最適化問題にカスタマイズすることで、非常に高速で正確な解を得ることができる。 最適性のKarush-Kuhn-Tucker条件に基づく新しい損失関数を導入し、両ニューラルネットワークの完全な自己教師付きトレーニングを可能にする。
  論文  参考訳（メタデータ） (2024-09-12T14:17:23Z)
• torchmSAT: A GPU-Accelerated Approximation To The Maximum Satisfiability Problem [1.5850859526672516]
  最大満足度問題(MaxSAT)の解を近似できる単一の微分可能関数を導出する。 我々は,我々の微分可能な関数をモデル化する新しいニューラルネットワークアーキテクチャを提案し,バックプロパゲーションを用いてMaxSATを段階的に解く。
  論文  参考訳（メタデータ） (2024-02-06T02:33:00Z)
• Automatic Algorithm Selection for Pseudo-Boolean Optimization with Given Computational Time Limits [0.9831489366502301]
  機械学習(ML)技術は、解決者のポートフォリオから最適な解法を自動選択するために提案されている。 これらのメソッドはメタソルバと呼ばれ、問題のインスタンスと解決者のポートフォリオを入力として取ります。 「Anytime」メタソルバは、指定された時間制限内で最高の性能の解決器を予測する。
  論文  参考訳（メタデータ） (2023-09-07T03:04:50Z)
• Machine Learning for SAT: Restricted Heuristics and New Graph Representations [0.8870188183999854]
  SATは、自動スケジューリングを含む多くのアプリケーションにおいて、基本的なNP完全問題である。 大きなインスタンスを解決するためには、SATソルバは、例えばDPLLとCDCLソルバの分岐変数を選択するなど、ブールアンに依存する必要がある。 我々は、訓練されたMLモデルでいくつかの初期ステップを行い、古典的なランタイムに制御をリリースする戦略を提案する。
  論文  参考訳（メタデータ） (2023-07-18T10:46:28Z)
• 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)
• Learning Proximal Operators to Discover Multiple Optima [66.98045013486794]
  非家族問題における近位演算子を学習するためのエンドツーエンド手法を提案する。 本手法は,弱い目的と穏やかな条件下では,世界規模で収束することを示す。
  論文  参考訳（メタデータ） (2022-01-28T05:53:28Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
  論文  参考訳（メタデータ） (2021-07-15T04:47:35Z)
• QROSS: QUBO Relaxation Parameter Optimisation via Learning Solver Surrogates [14.905085636501438]
  問題のインスタンスの集合に関するソルバデータから学習することで,quboソルバのサロゲートモデルを構築する。 このようにして、インスタンスの共通構造とそれらの解決者との相互作用を捉えることができ、ペナルティパラメータを適切に選択することができる。 qrossは分散型データセットや様々な種類のquboソルバによく一般化されている。
  論文  参考訳（メタデータ） (2021-03-19T09:06:12Z)
• Meta-Solver for Neural Ordinary Differential Equations [77.8918415523446]
  本研究では,ソルバ空間の変動がニューラルODEの性能を向上する方法について検討する。 解法パラメータ化の正しい選択は, 敵の攻撃に対するロバスト性の観点から, 神経odesモデルに大きな影響を与える可能性がある。
  論文  参考訳（メタデータ） (2021-03-15T17:26:34Z)
• Adaptive Sampling for Best Policy Identification in Markov Decision Processes [79.4957965474334]
  本稿では,学習者が生成モデルにアクセスできる場合の,割引マルコフ決定(MDP)における最良の政治的識別の問題について検討する。 最先端アルゴリズムの利点を論じ、解説する。
  論文  参考訳（メタデータ） (2020-09-28T15:22:24Z)

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

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