論文の概要: AlphaMapleSAT: An MCTS-based Cube-and-Conquer SAT Solver for Hard Combinatorial Problems

• arxiv url: http://arxiv.org/abs/2401.13770v1
• Date: Wed, 24 Jan 2024 19:37:10 GMT
• ステータス: 処理完了
• システム内更新日: 2024-01-26 16:37:58.691427
• Title: AlphaMapleSAT: An MCTS-based Cube-and-Conquer SAT Solver for Hard Combinatorial Problems
• Title（参考訳）: AlphaMapleSAT: MCTSベースのキューブ・アンド・コンカヤSATソルバ
• Authors: Piyush Jha, Zhengyu Li, Zhengyang Lu, Curtis Bright, Vijay Ganesh
• Abstract要約: 本稿では,新しいモンテカルロ木探索法であるAlphaMapleSATを紹介する。 対照的に、我々の重要な革新は、演能的に駆動されるMCTSベースのルックアヘッドキューブ技術であり、効率的な立方体を見つけるためにより深い探索を行う。
• 参考スコア（独自算出の注目度）: 13.450216199781671
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: This paper introduces AlphaMapleSAT, a novel Monte Carlo Tree Search (MCTS) based Cube-and-Conquer (CnC) SAT solving method aimed at efficiently solving challenging combinatorial problems. Despite the tremendous success of CnC solvers in solving a variety of hard combinatorial problems, the lookahead cubing techniques at the heart of CnC have not evolved much for many years. Part of the reason is the sheer difficulty of coming up with new cubing techniques that are both low-cost and effective in partitioning input formulas into sub-formulas, such that the overall runtime is minimized. Lookahead cubing techniques used by current state-of-the-art CnC solvers, such as March, keep their cubing costs low by constraining the search for the optimal splitting variables. By contrast, our key innovation is a deductively-driven MCTS-based lookahead cubing technique, that performs a deeper heuristic search to find effective cubes, while keeping the cubing cost low. We perform an extensive comparison of AlphaMapleSAT against the March CnC solver on challenging combinatorial problems such as the minimum Kochen-Specker and Ramsey problems. We also perform ablation studies to verify the efficacy of the MCTS heuristic search for the cubing problem. Results show up to 2.3x speedup in parallel (and up to 27x in sequential) elapsed real time.
• Abstract（参考訳）: 本稿では,新しいモンテカルロ木探索法(mcts)に基づくcnc sat解法であるalphamaplesatを提案する。 様々な難解な組合せ問題の解決においてCnCソルバが驚くほど成功したにもかかわらず、CnCの中心にあるルックアヘッドキューブ技術は長年にわたってあまり進化していない。 その理由のひとつは、入力式をサブ形式に分割する上で、低コストかつ効果的な、ランタイム全体の最小化といった、新たなキューイングテクニックを思いつくことの難しさにある。 現在の最先端のcncソルバであるmarchなどのルックアヘッドキューイング技術は、最適分割変数の探索を制約することによりキュービングコストを低く抑えている。 対照的に、私たちの重要なイノベーションは、推論駆動のmctsベースのルックアヘッドキューブ技術であり、キューブコストを低く保ちながら、効果的なキューブを見つけるためのより深いヒューリスティックな探索を行います。 我々は,最小kochen-specker 問題や ramsey 問題などの組合せ問題に挑戦する march cnc solver と alphamaplesat を広範囲に比較した。 また, カブリング問題に対するMCTSヒューリスティック検索の有効性を検証するためにアブレーション研究を行った。 結果は、並列で2.3倍のスピードアップ(シーケンシャルで最大27倍)がリアルタイムで経過する。

関連論文リスト

• Learning a Prior for Monte Carlo Search by Replaying Solutions to Combinatorial Problems [4.561007128508218]
  本稿では,前者を自動的に計算する手法を提案する。 これは、プレイアウト時に計算コストを伴わない単純で一般的な方法である。 この方法は、ラテンスクエアコンプリート、カクロ、逆RNAフォールディングの3つの難しい問題に適用される。
  論文  参考訳（メタデータ） (2024-01-19T00:22:31Z)
• A Novel Normalized-Cut Solver with Nearest Neighbor Hierarchical Initialization [107.07093621337084]
  正規化カット(N-Cut)は、スペクトルクラスタリングの有名なモデルである。 1)正規化ラプラシア行列の連続スペクトル埋め込みを計算する; 2)$K$-meansまたはスペクトル回転による離散化。 有名な座標降下法に基づく新しいN-Cut解法を提案する。
  論文  参考訳（メタデータ） (2023-11-26T07:11:58Z)
• Multi-block-Single-probe Variance Reduced Estimator for Coupled Compositional Optimization [49.58290066287418]
  構成問題の複雑さを軽減するために,MSVR (Multi-block-probe Variance Reduced) という新しい手法を提案する。 本研究の結果は, 試料の複雑さの順序や強靭性への依存など, 様々な面で先行して改善された。
  論文  参考訳（メタデータ） (2022-07-18T12:03:26Z)
• Supplementing Recurrent Neural Networks with Annealing to Solve Combinatorial Optimization Problems [2.3642391095636484]
  本稿では,実世界の最適化問題に対するアプローチとして,変分古典アニール (VCA) を用いる可能性を示す。 以上の結果から, VCA は相対誤差の点で, 平均1桁以上の限界でアニーリング (SA) を平均的に上回ることがわかった。 ベストケースシナリオでは、SAが最適解を見つけられなかった場合、VCAは優れた代替手段として機能する、と結論付けます。
  論文  参考訳（メタデータ） (2022-07-17T14:33:17Z)
• QAOA-in-QAOA: solving large-scale MaxCut problems on small quantum machines [81.4597482536073]
  量子近似最適化アルゴリズム(QAOAs)は、量子マシンのパワーを利用し、断熱進化の精神を継承する。 量子マシンを用いて任意の大規模MaxCut問題を解くためにQAOA-in-QAOA(textQAOA2$)を提案する。 提案手法は,大規模最適化問題におけるQAOAsの能力を高めるために,他の高度な戦略にシームレスに組み込むことができる。
  論文  参考訳（メタデータ） (2022-05-24T03:49:10Z)
• The Machine Learning for Combinatorial Optimization Competition (ML4CO): Results and Insights [59.93939636422896]
  ML4COは、キーコンポーネントを置き換えることで最先端の最適化問題を解決することを目的としている。 このコンペティションでは、最高の実現可能なソリューションを見つけること、最も厳密な最適性証明書を生成すること、適切なルーティング設定を提供すること、という3つの課題があった。
  論文  参考訳（メタデータ） (2022-03-04T17:06:00Z)
• 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)
• Self-Supervision is All You Need for Solving Rubik's Cube [0.0]
  この研究は、ルービックキューブで表される、あらかじめ定義されたゴールで問題を解決するためのシンプルで効率的なディープラーニング手法を導入する。 このような問題に対して、目標状態から分岐するランダムスクランブル上でディープニューラルネットワークをトレーニングすることは、ほぼ最適解を達成するのに十分であることを示す。
  論文  参考訳（メタデータ） (2021-06-06T15:38:50Z)
• Incomplete MaxSAT Approaches for Combinatorial Testing [0.0]
  本稿では,最小長の制約付き混合被覆アレイを構築するためのSAT(Satifiability)に基づくアプローチを提案する。 この問題はシステム障害検出のためのコンビネータテストの中心である。
  論文  参考訳（メタデータ） (2021-05-26T14:00:56Z)
• ISTA-NAS: Efficient and Consistent Neural Architecture Search by Sparse Coding [86.40042104698792]
  スパース符号問題としてニューラルアーキテクチャ探索を定式化する。 実験では、CIFAR-10の2段階法では、検索にわずか0.05GPUしか必要としない。 本手法は,CIFAR-10とImageNetの両方において,評価時間のみのコストで最先端のパフォーマンスを実現する。
  論文  参考訳（メタデータ） (2020-10-13T04:34:24Z)

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

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