論文の概要: Advancing Local Search in SMT-NRA with MCSAT Integration

• arxiv url: http://arxiv.org/abs/2507.00557v1
• Date: Tue, 01 Jul 2025 08:27:29 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-07-03 14:22:59.53895
• Title: Advancing Local Search in SMT-NRA with MCSAT Integration
• Title（参考訳）: SMT-NRAにおけるMCSAT統合による局所探索の高速化
• Authors: Tianyi Ding, Haokun Li, Xinpeng Ni, Bican Xia, Tianqi Zhao,
• Abstract要約: SMT-NRA(Satifiability Modulo the Theory of Real Arithmetic、略してSMT-NRA)の局所探索を進めた。 そこで我々は,SMT-NRAの局所探索法において,2d$-cell-jumpと呼ばれる2次元セルジャンプを導入し,鍵操作,セルジャンプを一般化した。 本研究では, 探索効率を向上させるために, 満足度計算フレームワークを構成するモデルを組み込んだ拡張ローカル検索フレームワークemph$2d$-LSを提案する。
• 参考スコア（独自算出の注目度）: 1.9897939373302893
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: In this paper, we advance local search for Satisfiability Modulo the Theory of Nonlinear Real Arithmetic (SMT-NRA for short). First, we introduce a two-dimensional cell-jump move, called \emph{$2d$-cell-jump}, generalizing the key operation, cell-jump, of the local search method for SMT-NRA. Then, we propose an extended local search framework, named \emph{$2d$-LS} (following the local search framework, LS, for SMT-NRA), integrating the model constructing satisfiability calculus (MCSAT) framework to improve search efficiency. To further improve the efficiency of MCSAT, we implement a recently proposed technique called \emph{sample-cell projection operator} for MCSAT, which is well suited for CDCL-style search in the real domain and helps guide the search away from conflicting states. Finally, we design a hybrid framework for SMT-NRA combining MCSAT, $2d$-LS and OpenCAD, to improve search efficiency through information exchange. The experimental results demonstrate improvements in local search performance, highlighting the effectiveness of the proposed methods.
• Abstract（参考訳）: 本稿では,SMT-NRA(Satifiability Modulo the Theory of Non Real Arithmetic, 略してSMT-NRA)を局所的に探索する。 まず,SMT-NRAの局所探索法のキー操作であるセルジャンプを一般化した2次元セルジャンプ(emph{$2d$-cell-jump})を導入する。 そこで我々は,探索効率を向上させるために,MCSATフレームワークを構成するモデルを統合する,拡張された局所探索フレームワークであるemph{$2d$-LS}(ローカル探索フレームワークLSをSMT-NRAに置き換える)を提案する。 MCSAT の効率をさらに向上するため,近年提案されている MCSAT の 'emph{sample-cell projection operator} という手法を実装した。 最後に,MCSAT,2d$-LS,OpenCADを組み合わせたSMT-NRAのハイブリッドフレームワークを設計し,情報交換による検索効率の向上を図る。 実験の結果,局所探索性能が向上し,提案手法の有効性が示された。

関連論文リスト

• LLM-First Search: Self-Guided Exploration of the Solution Space [29.780554400938335]
  大規模言語モデル(LLM)は、テスト時間計算の増加による推論と計画の大幅な改善を示している。 我々は,新しいTextitLLM Self-Guided Search法である textbfLLM-First Search (LFS) を提案する。
  論文  参考訳（メタデータ） (2025-06-05T16:27:49Z)
• LLM Program Optimization via Retrieval Augmented Search [71.40092732256252]
  提案手法は,提案手法によって最適化されたビーム探索を行う検索アルゴリズムであるRetrieval Augmented Search (RAS) である。 我々は、RASが従来の最先端のブラックボックス適応戦略よりも1.8$times$パフォーマンスが高いことを示す。 また、トレーニング例を「アトミックな編集」に分解することで、解釈可能性を向上させるAEGISと呼ばれる手法を提案する。
  論文  参考訳（メタデータ） (2025-01-31T06:34:47Z)
• LLaMA-Berry: Pairwise Optimization for O1-like Olympiad-Level Mathematical Reasoning [56.273799410256075]
  このフレームワークはMonte Carlo Tree Search (MCTS)と反復的なSelf-Refineを組み合わせて推論パスを最適化する。 このフレームワークは、一般的なベンチマークと高度なベンチマークでテストされており、探索効率と問題解決能力の点で優れた性能を示している。
  論文  参考訳（メタデータ） (2024-10-03T18:12:29Z)
• Trochoid Search Optimization [0.0]
  TSOアルゴリズムは、トロコイドに固有の同時翻訳運動と回転運動のユニークな組み合わせを用いる。 実験的検証により、TSOアルゴリズムは様々なベンチマーク関数に対して顕著な性能を示す。
  論文  参考訳（メタデータ） (2023-12-21T06:02:27Z)
• Improved Monte Carlo tree search formulation with multiple root nodes for discrete sizing optimization of truss structures [1.0923877073891446]
  本稿では,改良モンテカルロ木探索法(IMCTS)を用いた新しい強化学習アルゴリズムを提案する。 複数のルートノードを持つIMCTSには、更新プロセス、最高の報酬、加速技術、端末条件が含まれる。 これらの数値的な例は、エージェントが計算コストの低い最適解を見つけ、安定して最適な設計をし、多目的構造最適化や大規模構造に適していることを示している。
  論文  参考訳（メタデータ） (2023-09-12T08:29:53Z)
• Learning Regions of Interest for Bayesian Optimization with Adaptive Level-Set Estimation [84.0621253654014]
  本稿では,高信頼領域を適応的にフィルタするBALLETというフレームワークを提案する。 理論的には、BALLETは探索空間を効率的に縮小することができ、標準BOよりも厳密な後悔を示すことができる。
  論文  参考訳（メタデータ） (2023-07-25T09:45:47Z)
• Efficient Non-Parametric Optimizer Search for Diverse Tasks [93.64739408827604]
  興味のあるタスクを直接検索できる,スケーラブルで汎用的なフレームワークを初めて提示する。 基礎となる数学表現の自然木構造に着想を得て、空間を超木に再配置する。 我々は,モンテカルロ法を木探索に適用し,レジェクションサンプリングと等価形状検出を備える。
  論文  参考訳（メタデータ） (2022-09-27T17:51:31Z)
• Learning Space Partitions for Path Planning [54.475949279050596]
  PlaLaMは2次元ナビゲーションタスクにおける既存の経路計画手法よりも優れており、特に難解な局所最適化の存在下では優れている。 これらは高マルチモーダルな実世界のタスクに移行し、コンパイラフェーズでは最大245%、分子設計では最大0.4の強いベースラインを0-1スケールで上回ります。
  論文  参考訳（メタデータ） (2021-06-19T18:06:11Z)
• Memetic Search for Vehicle Routing with Simultaneous Pickup-Delivery and Time Windows [31.512563458410963]
  本稿では,この問題を解決するために,局所探索を効率的に行うメメティックアルゴリズム(MATE)を提案する。 MATEは最先端のアルゴリズムをすべて上回り、特に12インスタンス(合計65インスタンス)でよく知られた新しいソリューションを見つける。
  論文  参考訳（メタデータ） (2020-11-12T12:06:11Z)

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

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