論文の概要: Learning Branching Heuristics for Propositional Model Counting

• arxiv url: http://arxiv.org/abs/2007.03204v2
• Date: Thu, 8 Sep 2022 21:47:20 GMT
• ステータス: 処理完了
• システム内更新日: 2022-11-12 18:22:24.383133
• Title: Learning Branching Heuristics for Propositional Model Counting
• Title（参考訳）: 命題モデルカウントのための学習分岐ヒューリスティックス
• Authors: Pashootan Vaezipoor, Gil Lederman, Yuhuai Wu, Chris J. Maddison, Roger Grosse, Sanjit A. Seshia, Fahiem Bacchus
• Abstract要約: #SAT はブール公式の充足数を計算する問題である。 Neuro#は、特定の問題ファミリからインスタンス上の正確な#SATソルバのパフォーマンスを改善するために、ブランチを学習するためのアプローチである。
• 参考スコア（独自算出の注目度）: 27.343084935521752
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Propositional model counting, or #SAT, is the problem of computing the number of satisfying assignments of a Boolean formula. Many problems from different application areas, including many discrete probabilistic inference problems, can be translated into model counting problems to be solved by #SAT solvers. Exact #SAT solvers, however, are often not scalable to industrial size instances. In this paper, we present Neuro#, an approach for learning branching heuristics to improve the performance of exact #SAT solvers on instances from a given family of problems. We experimentally show that our method reduces the step count on similarly distributed held-out instances and generalizes to much larger instances from the same problem family. It is able to achieve these results on a number of different problem families having very different structures. In addition to step count improvements, Neuro# can also achieve orders of magnitude wall-clock speedups over the vanilla solver on larger instances in some problem families, despite the runtime overhead of querying the model.
• Abstract（参考訳）: 命題モデルカウント(英: Propositional model counting, #SAT)は、ブール公式の充足数を計算する問題である。 多くの離散確率的推論問題を含む、異なるアプリケーション領域からの多くの問題は#satソルバによって解決されるモデルカウント問題に変換できる。 しかし、排他的な#SATソルバは工業規模のインスタンスには拡張性がないことが多い。 本稿では,特定の問題群からインスタンス上での#satソルバの正確な性能を改善するために,分岐ヒューリスティックスを学ぶためのアプローチであるneuro#を提案する。 本手法は,同様の分散ホールドアウトインスタンスのステップカウントを低減し,同じ問題ファミリーからさらに大きなインスタンスに一般化できることを実験的に示す。 異なる構造を持つ多くの異なる問題ファミリーでこれらの結果を達成することができる。 ステップ数の改善に加えて、neuro#では、モデルクエリのランタイムオーバヘッドにもかかわらず、問題ファミリー内の大きなインスタンスで、バニラソルバに対して1桁のウォールクロックスピードアップを実現することもできる。

関連論文リスト

• GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection [45.222591894755105]
  インスタンスの3部グラフ表現に基づくSATソルバ自動選択のための新しいアプローチであるGraSSを提案する。 我々は、新しいノードの特徴設計のようなドメイン固有の決定でグラフ表現を豊かにします。 生の表現とドメイン固有の選択の組み合わせが実行時の改善につながることを実証する。
  論文  参考訳（メタデータ） (2024-05-17T18:00:50Z)
• Using deep learning to construct stochastic local search SAT solvers with performance bounds [0.0]
  グラフニューラルネットワークを用いてオーラクルを訓練し、2つのSLSソルバ上で、様々な難易度を持つランダムSATインスタンス上でそれらを評価する。 GNNベースのオラクルへのアクセスは,両者のパフォーマンスを著しく向上させることがわかった。
  論文  参考訳（メタデータ） (2023-09-20T16:27:52Z)
• Machine Learning for SAT: Restricted Heuristics and New Graph Representations [0.8870188183999854]
  SATは、自動スケジューリングを含む多くのアプリケーションにおいて、基本的なNP完全問題である。 大きなインスタンスを解決するためには、SATソルバは、例えばDPLLとCDCLソルバの分岐変数を選択するなど、ブールアンに依存する必要がある。 我々は、訓練されたMLモデルでいくつかの初期ステップを行い、古典的なランタイムに制御をリリースする戦略を提案する。
  論文  参考訳（メタデータ） (2023-07-18T10:46:28Z)
• RetICL: Sequential Retrieval of In-Context Examples with Reinforcement Learning [53.52699766206808]
  In-Context Learning (RetICL) のための検索式を提案する。 RetICLは数学用語の問題解決と科学的質問応答のタスクに基づいて評価し,一貫した性能や一致,学習可能なベースラインを示す。
  論文  参考訳（メタデータ） (2023-05-23T20:15:56Z)
• Symmetric Tensor Networks for Generative Modeling and Constrained Combinatorial Optimization [72.41480594026815]
  ポートフォリオ最適化からロジスティクスに至るまで、制約付き最適化問題は業界に多い。 これらの問題の解決における主要な障害の1つは、有効な検索空間を制限する非自明なハード制約の存在である。 本研究では、Ax=bという形の任意の整数値等式制約をU(1)対称ネットワーク(TN)に直接エンコードし、それらの適用性を量子に着想を得た生成モデルとして活用する。
  論文  参考訳（メタデータ） (2022-11-16T18:59:54Z)
• Graph Neural Networks for Propositional Model Counting [1.0152838128195467]
  グラフネットワーク(GNN)は最近、論理的推論タスクの解決に活用されている。 本稿では, 自覚的GNNによって拡張され, #SAT 問題を大まかに解くために訓練された, Kuch 等の信念伝播のための GNN フレームワークに基づくアーキテクチャを提案する。
  論文  参考訳（メタデータ） (2022-05-09T17:03:13Z)
• 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)
• Provable Reinforcement Learning with a Short-Term Memory [68.00677878812908]
  我々はPMDPsの新しいサブクラスについて研究し、その潜在状態は、最近の短い長さ$m$の履歴によって復号化することができる。 特に、リッチ・オブザーブレーション・セッティングにおいて、指数関数的にスケールするサンプル複雑性を持つ新しい「モーメントマッチング」アプローチを用いて、新しいアルゴリズムを開発する。 以上の結果から,これらの環境下での強化学習には短期記憶が十分であることが示唆された。
  論文  参考訳（メタデータ） (2022-02-08T16:39:57Z)
• 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)

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

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