論文の概要: Learning Splitting Heuristics for Parallel String Solvers

• arxiv url: http://arxiv.org/abs/2606.20656v1
• Date: Tue, 09 Jun 2026 04:48:58 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-30 20:34:42.47049
• Title: Learning Splitting Heuristics for Parallel String Solvers
• Title（参考訳）: 並列文字列解に対する分割的ヒューリスティックス学習
• Abstract要約: 本稿では,分割を自動的に生成するデータ駆動方式を提案する。 我々は、入力式の特徴とソルバ実行からの動的データを用いて、分割原子を学習タスクとして選択する問題の枠組みを定式化した。 本手法は2つの一般的な文字列ソルバであるZ3seqとZ3str4に実装し,解法数と平均解時間において,学習者が手作業で設計したものよりも優れていることを示す。
• 参考スコア（独自算出の注目度）: 3.22853198951198
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: String constraint solvers are crucial for reasoning about string-manipulating programs. However, many practical string constraints are undecidable, and real-world applications often present complex constraints that challenge current solvers. The rise of multi-core architectures offers an opportunity for parallel solving. A key parallel solving method is \emph{cube-and-conquer}, in which the quality of splitting heuristics is critical to effectively dividing the search space. Unfortunately, manually designing the heuristics is labor-intensive, and handcrafted heuristics are often sub-optimal. This paper introduces a data-driven approach to automatically generating splitting heuristics. We frame the problem of selecting a splitting atom as a learning task, using features from input formulas and dynamic data from solver execution. We implement this approach in two popular string solvers, Z3seq and Z3str4, demonstrating that the learned heuristics outperform manually designed ones in the number of solved formulas and the average solving time.
• Abstract（参考訳）: 文字列操作プログラムの推論には文字列制約解決器が不可欠である。 しかし、多くの実用的な文字列制約は決定不可能であり、現実のアプリケーションはしばしば現在の解法に挑戦する複雑な制約を提示する。 マルチコアアーキテクチャの台頭は、並列解決の機会を提供する。 鍵となる並列解法は \emph{cube-and-conquer} であり、分割ヒューリスティックの質が探索空間を効果的に分割するために重要である。 残念ながら、手動でヒューリスティックを設計するのは労働集約的であり、手作りヒューリスティックはしばしば準最適である。 本稿では,分割ヒューリスティックを自動生成するデータ駆動手法を提案する。 我々は、入力式の特徴とソルバ実行からの動的データを用いて、分割原子を学習タスクとして選択する問題の枠組みを定式化した。 本手法は2つの一般的な文字列解法であるZ3seqとZ3str4に実装し、学習されたヒューリスティックスが解数と平均解時間において手作業で設計したものよりも優れていることを示す。

関連論文リスト

• A Greedy PDE Router for Blending Neural Operators and Classical Methods [24.752048932494827]
  最適なハイブリッド反復解法が設計され、各イテレーションにおいて、ソルバのアンサンブルからソルバが選択され、それらの相補的な強みを利用する。 最適解に対する定数要素を保証するためには、欲求選択戦略が望ましいが、各ステップにおける真のエラーの知識が必要である。 本稿では,解法選択に対するグリージーアプローチを効率的に模倣する近似グリージールータを提案する。
  論文  参考訳（メタデータ） (2025-09-29T14:02:27Z)
• Agentic-R1: Distilled Dual-Strategy Reasoning [58.73951532294446]
  現在のロングチェーン・オブ・ソート(ロングCoT)モデルは数学的推論において優れているが、遅くてエラーを起こしやすい自然言語トレースに依存している。 複数の教師の補完的推論戦略を統合された学生モデルに蒸留する微調整フレームワークであるDualDistillを導入する。 本手法は,計算集約型ベンチマークと標準ベンチマークの両方を含むタスクの精度を向上する。
  論文  参考訳（メタデータ） (2025-07-08T06:35:16Z)
• FLARE: Faithful Logic-Aided Reasoning and Exploration [47.46564769245296]
  タスク分解を用いて問題空間をトラバースする新しい手法を提案する。 我々はLarge Language Modelsを使ってソリューションを計画し、クエリを事実に軟式化し、論理プログラミングコードを使って述語する。 提案手法は,生成したコードに対する推論プロセスの忠実度を計算し,外部の解法に頼らずにマルチホップ探索のステップを解析する。
  論文  参考訳（メタデータ） (2024-10-14T19:39:11Z)
• Towards a Generic Representation of Combinatorial Problems for Learning-Based Approaches [2.2526069385327316]
  近年,問題解決に学習ベースのアプローチを使うことへの関心が高まっている。 この課題は、対象とする問題を学習アルゴリズムと互換性のある構造に符号化することにある。 既存の多くの研究は、しばしばグラフの形で、テキストトグラフニューラルネットワークの利点を活用するために問題固有の表現を提案している。 本稿では,学習に基づくアプローチにおける問題を完全に包括的に表現することを提唱する。
  論文  参考訳（メタデータ） (2024-03-09T22:28:46Z)
• Faith and Fate: Limits of Transformers on Compositionality [109.79516190693415]
  3つの代表的構成課題にまたがる変圧器大言語モデルの限界について検討する。 これらのタスクは、問題をサブステップに分割し、これらのステップを正確な答えに合成する必要があります。 実験結果から,多段階合成推論を線形化部分グラフマッチングに還元することにより,トランスフォーマーLLMが構成課題を解くことが示唆された。
  論文  参考訳（メタデータ） (2023-05-29T23:24:14Z)
• Learning a Generic Value-Selection Heuristic Inside a Constraint Programming Solver [2.8425837800129696]
  本稿では,制約型プログラミング解法内での値選択に利用できる汎用的な学習手法を提案する。 これは、深いQ-ラーニングアルゴリズム、カスタマイズされた報酬信号、異種グラフニューラルネットワークアーキテクチャの組み合わせによって実現されている。
  論文  参考訳（メタデータ） (2023-01-05T05:13:48Z)
• Sketching as a Tool for Understanding and Accelerating Self-attention for Long Sequences [52.6022911513076]
  トランスフォーマーベースのモデルは、自己アテンションモジュールの二次空間と時間的複雑さのために、長いシーケンスを処理するのに効率的ではない。 我々はLinformerとInformerを提案し、低次元投影と行選択により2次複雑性を線形(モジュラー対数因子)に還元する。 理論的解析に基づいて,Skeinformerを提案することにより,自己注意の促進と,自己注意への行列近似の精度の向上を図ることができる。
  論文  参考訳（メタデータ） (2021-12-10T06:58:05Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
  論文  参考訳（メタデータ） (2021-07-15T04:47:35Z)
• Learning to Schedule Heuristics in Branch-and-Bound [25.79025327341732]
  現実世界のアプリケーションは通常、迅速な意思決定を可能にするために、検索の早い段階で優れたソリューションを見つける必要があります。 正確なMIPソルバにおけるスケジューリングのための最初のデータ駆動フレームワークを提案する。 最先端の学術MIPソルバーのデフォルト設定と比較して、挑戦的なインスタンスのクラスで平均プライマリ積分を最大49%削減することができます。
  論文  参考訳（メタデータ） (2021-03-18T14:49:52Z)
• A Two-stage Framework and Reinforcement Learning-based Optimization Algorithms for Complex Scheduling Problems [54.61091936472494]
  本稿では、強化学習(RL)と従来の運用研究(OR)アルゴリズムを組み合わせた2段階のフレームワークを開発する。 スケジューリング問題は,有限マルコフ決定過程 (MDP) と混合整数計画過程 (mixed-integer programming process) の2段階で解決される。 その結果,本アルゴリズムは,アジャイルな地球観測衛星スケジューリング問題に対して,安定かつ効率的に十分なスケジューリング計画を得ることができた。
  論文  参考訳（メタデータ） (2021-03-10T03:16:12Z)
• Physarum Powered Differentiable Linear Programming Layers and Applications [48.77235931652611]
  一般線形プログラミング問題に対する効率的かつ微分可能な解法を提案する。 本稿では,ビデオセグメンテーションタスクとメタラーニングにおける問題解決手法について述べる。
  論文  参考訳（メタデータ） (2020-04-30T01:50:37Z)

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

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