Extracting Problem Structure with LLMs for Optimized SAT Local Search

要約

ローカル検索前処理は、高品質の開始点を提供することで競合駆動節学習 (CDCL) ソルバーを高速化し、最新の SAT ソルバーはこの技術を前処理ステップに組み込んでいます。
ただし、これらのツールは、問題の構造パターンを見逃している基本的な戦略に依存しています。
大規模言語モデル (LLM) を適用して Python ベースのエンコード コードを分析する方法を紹介します。
これにより、問題が SAT に変換される過程における隠された構造パターンが明らかになります。
私たちの方法は、これらのパターンを見つけてそれらを使用して強力な初期割り当てを作成する、特殊なローカル検索アルゴリズムを自動的に生成します。
これは、同じエンコード タイプの問題が発生した場合に機能します。
私たちのテストでは、ベースラインの前処理システムと比較して、より速い解決時間を達成するという有望な結果が示されています。

要約(オリジナル)

Local search preprocessing makes Conflict-Driven Clause Learning (CDCL) solvers faster by providing high-quality starting points and modern SAT solvers have incorporated this technique into their preprocessing steps. However, these tools rely on basic strategies that miss the structural patterns in problems. We present a method that applies Large Language Models (LLMs) to analyze Python-based encoding code. This reveals hidden structural patterns in how problems convert into SAT. Our method automatically generates specialized local search algorithms that find these patterns and use them to create strong initial assignments. This works for any problem instance from the same encoding type. Our tests show encouraging results, achieving faster solving times compared to baseline preprocessing systems.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google