論文の概要: Smart Cubing for Graph Search: A Comparative Study

• arxiv url: http://arxiv.org/abs/2501.17201v1
• Date: Mon, 27 Jan 2025 22:15:54 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-01-30 15:54:05.154923
• Title: Smart Cubing for Graph Search: A Comparative Study
• Title（参考訳）: グラフ検索のためのスマートキューブ : 比較研究
• Authors: Markus Kirchweger, Hai Xia, Tomáš Peitl, Stefan Szeider,
• Abstract要約: 立方体とコンカヤによる並列解法はSATソルバをハードインスタンスに拡張するための重要な方法である。 キューブ・アンド・コンカーは純粋なSAT問題に対して成功したが、SATソルバへの応用はプロパゲータによって拡張され、ユニークな課題が提示される。 本研究では, SATモジュロ対称性(SMS)を用いて, 対称性を破るプロパゲータが等方性グラフを除去する制約を学習することで探索空間を減少させる問題について検討する。
• 参考スコア（独自算出の注目度）: 15.989407883187962
• License:
• Abstract: Parallel solving via cube-and-conquer is a key method for scaling SAT solvers to hard instances. While cube-and-conquer has proven successful for pure SAT problems, notably the Pythagorean triples conjecture, its application to SAT solvers extended with propagators presents unique challenges, as these propagators learn constraints dynamically during the search. We study this problem using SAT Modulo Symmetries (SMS) as our primary test case, where a symmetry-breaking propagator reduces the search space by learning constraints that eliminate isomorphic graphs. Through extensive experimentation comprising over 10,000 CPU hours, we systematically evaluate different cube-and-conquer variants on three well-studied combinatorial problems. Our methodology combines prerun phases to collect learned constraints, various cubing strategies, and parameter tuning via algorithm configuration and LLM-generated design suggestions. The comprehensive empirical evaluation provides new insights into effective cubing strategies for propagator-based SAT solving, with our best method achieving speedups of 2-3x from improved cubing and parameter tuning, providing an additional 1.5-2x improvement on harder instances.
• Abstract（参考訳）: 立方体とコンカヤによる並列解法はSATソルバをハードインスタンスに拡張するための重要な方法である。 キューブ・アンド・コンカーは純粋なSAT問題、特にピタゴラス三重項予想において成功したが、プロパゲータで拡張されたSATソルバへの応用は、探索中に制約を動的に学習するので、ユニークな課題を提示する。 本研究では, SATモジュロ対称性(SMS)を用いて, 対称性を破るプロパゲータが等方性グラフを除去する制約を学習することで探索空間を減少させる問題について検討する。 1万時間以上のCPU時間からなる広範囲な実験を通じて、よく研究された3つの組合せ問題に対して、異なる立方体とコンカヤの変種を体系的に評価した。 提案手法は,学習した制約,様々なキューブ戦略,アルゴリズム構成によるパラメータチューニング,LLMによる設計提案の事前実行フェーズを組み合わせる。 包括的経験的評価は、プロパゲータベースのSAT解決のための効果的なキュウティング戦略に関する新たな洞察を提供するとともに、より複雑なインスタンスに対して1.5～2倍の改善をもたらすため、キュウティングとパラメータチューニングの改善から2～3倍のスピードアップを達成する最良の方法である。

関連論文リスト

• Deeply Optimizing the SAT Solver for the IC3 Algorithm [0.23749905164931204]
  観測結果に基づいて,IC3におけるSATソルバの最適化について述べる。 バイナリヒープをバケットに置き換えて、一定時間操作を実現しています。 我々はこれらの最適化を統合した新しい軽量CDCL SATソルバであるGipSATを開発した。
  論文  参考訳（メタデータ） (2025-01-24T12:40:43Z)
• torchmSAT: A GPU-Accelerated Approximation To The Maximum Satisfiability Problem [1.5850859526672516]
  最大満足度問題(MaxSAT)の解を近似できる単一の微分可能関数を導出する。 我々は,我々の微分可能な関数をモデル化する新しいニューラルネットワークアーキテクチャを提案し,バックプロパゲーションを用いてMaxSATを段階的に解く。
  論文  参考訳（メタデータ） (2024-02-06T02:33:00Z)
• AlphaMapleSAT: An MCTS-based Cube-and-Conquer SAT Solver for Hard Combinatorial Problems [13.450216199781671]
  本稿では,新しいモンテカルロ木探索法であるAlphaMapleSATを紹介する。 対照的に、我々の重要な革新は、演能的に駆動されるMCTSベースのルックアヘッドキューブ技術であり、効率的な立方体を見つけるためにより深い探索を行う。
  論文  参考訳（メタデータ） (2024-01-24T19:37:10Z)
• Machine Learning for SAT: Restricted Heuristics and New Graph Representations [0.8870188183999854]
  SATは、自動スケジューリングを含む多くのアプリケーションにおいて、基本的なNP完全問題である。 大きなインスタンスを解決するためには、SATソルバは、例えばDPLLとCDCLソルバの分岐変数を選択するなど、ブールアンに依存する必要がある。 我々は、訓練されたMLモデルでいくつかの初期ステップを行い、古典的なランタイムに制御をリリースする戦略を提案する。
  論文  参考訳（メタデータ） (2023-07-18T10:46:28Z)
• A hybrid Quantum proposal to deal with 3-SAT problem [75.38606213726906]
  本稿では,3SAT問題を解くためのハイブリッド量子コンピューティング戦略について述べる。 この近似の性能は、量子コンピューティングの観点から3-SATを扱う際に、一連の代表的なシナリオで検証されている。
  論文  参考訳（メタデータ） (2023-06-07T12:19:22Z)
• Multi-block-Single-probe Variance Reduced Estimator for Coupled Compositional Optimization [49.58290066287418]
  構成問題の複雑さを軽減するために,MSVR (Multi-block-probe Variance Reduced) という新しい手法を提案する。 本研究の結果は, 試料の複雑さの順序や強靭性への依存など, 様々な面で先行して改善された。
  論文  参考訳（メタデータ） (2022-07-18T12:03:26Z)
• On a class of geodesically convex optimization problems solved via Euclidean MM methods [50.428784381385164]
  ユークリッド凸化関数の違いは、統計学と機械学習の異なるタイプの問題の違いとして記述できることを示す。 最終的に、より広い範囲、より広い範囲の作業を支援するのです。
  論文  参考訳（メタデータ） (2022-06-22T23:57:40Z)
• 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)

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

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