論文の概要: Tactix: Towards a Programmable Strategy Interface for Flexible SAT Solving

• arxiv url: http://arxiv.org/abs/2610.24369v1
• Date: Sat, 17 Oct 2026 01:47:55 GMT
• ステータス: 情報取得中
• システム内更新日: 2026-10-20 11:58:51.950402
• Title: Tactix: Towards a Programmable Strategy Interface for Flexible SAT Solving
• Title（参考訳）: Tactix: フレキシブルSAT解決のためのプログラム可能な戦略インターフェースを目指す
• Abstract要約: 本稿では,証明ルールと解法をきれいに分離した証明生成シーケンシャルCDCLソルバであるTactixを提案する。 Tactixは2024-2026年のSATコンペティションのベンチマークで最先端のソルバを上回っている。 また、Tactixを支えるAI支援開発プロセスの自己学習についても紹介する。
• 参考スコア（独自算出の注目度）: 10.658660845987393
• License:
• Abstract: Modern SAT solvers combine a rich repertoire of proof rules with sophisticated strategies that determine when and how to apply them. Often, the internal implementations are tightly coupled to particular strategies, making it inconvenient to define new strategies without changing solver internals. We present Tactix, a proof-producing sequential CDCL solver that incorporates a wide range of techniques in state-of-the-art solvers with a clean separation of proof rules from solving strategies. This separation enables a public interface through which users can invoke particular techniques, observe their effects, and program a wide range of solving strategies. The default strategy of Tactix is programmable over this interface and outperforms state-of-the-art solvers on benchmarks from the 2024--2026 SAT Competitions. We also use the interface to develop novel strategies tailored to challenging benchmarks from two application domains, which led to performance gains over strong baselines. We intend Tactix to serve as an infrastructure for designing and evaluating novel solving strategies. Finally, we also present a self-study of the AI-assisted development process behind Tactix.
• Abstract（参考訳）: 現代のSATソルバは、証明規則の豊富なレパートリーと、いつ、どのように適用するかを決定する洗練された戦略を組み合わせる。 多くの場合、内部実装は特定の戦略と密結合しており、解決者の内部を変更することなく新しい戦略を定義することは不便である。 本稿では,証明ルールと解法をきれいに分離し,最先端の解法に幅広いテクニックを取り入れた,証明生成シーケンシャルCDCL解法であるTactixを提案する。 この分離により、ユーザが特定のテクニックを実行し、その効果を観察し、幅広い問題解決戦略をプログラムできる公開インターフェースが実現される。 Tactixのデフォルトの戦略は、このインターフェイス上でプログラム可能であり、2024-2026年のSATコンペティションのベンチマークで最先端のソルバを上回っている。 また、このインターフェースを使用して、2つのアプリケーションドメインからのベンチマークに挑戦する新しい戦略を開発しました。 私たちは、新しい問題解決戦略を設計し評価するための基盤として、Tactixを機能させるつもりです。 最後に、Tactixを支えるAI支援開発プロセスの自己学習についても紹介する。

関連論文リスト

• Parallelism Strategy Chaining for Fast Training Convergence [12.463381960118852]
  本稿では,オンライン戦略連鎖を導入した新しいトレーニング手法を提案する。 ConAは、計算スループットと勾配統計から構築された代理メトリックを使用して、トレーニング中の候補戦略をランク付けする。 GPT-3 1.3B,BERT-Large,Llama-3.2-1Bによる評価では,CONAは最先端手法よりも1.4-9.6倍高速である。
  論文  参考訳（メタデータ） (2026-09-07T08:55:14Z)
• Strategy Executability in Mathematical Reasoning: Leveraging Human-Model Differences for Effective Guidance [86.46794021499511]
  戦略利用と戦略実行可能性の間には、これまで未定のギャップがある。 SSR(Selective Strategy Retrieval)は,実行可能性を明確にモデル化するテストタイムフレームワークである。 SSRは、直接解決、文脈内学習、単一ソースガイダンスよりも信頼性が高く一貫した改善をもたらす。
  論文  参考訳（メタデータ） (2026-02-26T03:34:23Z)
• CONCUR: A Framework for Continual Constrained and Unconstrained Routing [79.85419373937765]
  AIタスクは複雑さが異なり、異なる計算戦略で対処するのが最善である。 これまでのほとんどのメソッドは、すべての戦略で単一のモデルをトレーニングすることで、ルーティングフレームワークを構築していました。 制約付きルーティングと制約なしルーティングの両方をサポートする連続的なルーティングフレームワークであるCONCURを提案する。
  論文  参考訳（メタデータ） (2025-12-10T07:30:13Z)
• Experience-Guided Adaptation of Inference-Time Reasoning Strategies [49.954515048847874]
  Experience-Guided Reasoner (EGuR) は蓄積された経験に基づいて推論時に調整された戦略を生成する。 EGuRは最強のベースラインに対して最大14%の精度向上を実現し、計算コストを最大111倍に削減する。
  論文  参考訳（メタデータ） (2025-11-14T17:45:28Z)
• Plan before Solving: Problem-Aware Strategy Routing for Mathematical Reasoning with LLMs [49.995906301946]
  既存の手法は通常、数学的推論を行うためにLLM(Large Language Models)をガイドするための固定戦略を利用する。 分析の結果,単一戦略は問題固有の要件に適応できず,有効性と効率性のトレードオフを見落としていることが明らかとなった。 本稿では,PRISM(Planning and Routing through Instance-Specific Modeling)を提案する。
  論文  参考訳（メタデータ） (2025-09-29T07:22:41Z)
• Counterfactual Strategies for Markov Decision Processes [3.42834279186368]
  マルコフ決定過程(MDP)に対する反実的戦略を導入する。 MDP実行中、戦略はどのアクションが次に実行されるかを決定する。 限界以下の確率を減少させるために、初期戦略に対する最小限の変更を識別する。
  論文  参考訳（メタデータ） (2025-05-14T14:07:27Z)
• Strategy-Augmented Planning for Large Language Models via Opponent Exploitation [11.840105106884543]
  LLMエージェントの攻撃的利用能力を大幅に向上させる2段階戦略拡張計画(SAP)フレームワークを提案する。 オフラインの段階では、明示的な戦略空間を構築し、その後戦略評価ネットワーク(SEN)をトレーニングするための戦略アウトカムペアデータを収集する。 オンラインフェーズでは、SAPは相手の戦略を動的に認識し、よく訓練されたSEN上で最良のレスポンス戦略を探索することにより、それらを強引に活用する。
  論文  参考訳（メタデータ） (2025-05-13T11:41:10Z)
• REX: Rapid Exploration and eXploitation for AI Agents [103.68453326880456]
  本稿では、REXと呼ばれるAIエージェントのための高速探索およびeXploitationのための改良されたアプローチを提案する。 REXは追加の報酬層を導入し、アッパー信頼境界(UCB)スコアに似た概念を統合し、より堅牢で効率的なAIエージェントのパフォーマンスをもたらす。
  論文  参考訳（メタデータ） (2023-07-18T04:26:33Z)

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

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