AutoSAT: Automatically Optimize SAT Solvers via Large Language Models

要約

競合駆動節学習 (CDCL) は、充足可能性問題 (SAT) を解決するための主流のフレームワークであり、CDCL ソルバーは通常、パフォーマンスに大きな影響を与えるさまざまなヒューリスティックに依存します。
MiniSat や Kissat などの最新の CDCL ソルバーは、通常、複数のヒューリスティックを組み込み、単純なルールに従って使用するものを選択するため、実際に微調整するには多大な時間と専門家の努力が必要です。
大規模言語モデル (LLM) の普及により、この問題に対処する潜在的な解決策が提供されます。
ただし、CDCL ソルバーを最初から生成することは、SAT ソルバーの複雑さとコンテキストの量により効果的ではありません。
代わりに、既存の CDCL ソルバーに基づいて、事前定義されたモジュラー検索空間でヒューリスティックを自動的に最適化するフレームワークである AutoSAT を提案します。
ハイパーパラメーターの調整とオペレーターの選択に重点を置いた既存の自動アルゴリズム設計アプローチとは異なり、AutoSAT は新しい効率的なヒューリスティックを生成できます。
LLM を使用して SAT ソルバーを最適化するこの最初の試みでは、グリーディ ヒル クライマーや (1+1) 進化的アルゴリズムなどのいくつかの戦略を採用して、LLM がより良いヒューリスティックを検索できるように導きます。
実験結果は、LLM が一般に CDCL ソルバーのパフォーマンスを向上できることを示しています。
AutoSAT の実現は、12 データセット中 9 で MiniSat を上回り、4 つのデータセットでは最先端のハイブリッド ソルバー Kissat をも上回ります。

要約(オリジナル)

Conflict-Driven Clause Learning (CDCL) is the mainstream framework for solving the Satisfiability problem (SAT), and CDCL solvers typically rely on various heuristics, which have a significant impact on their performance. Modern CDCL solvers, such as MiniSat and Kissat, commonly incorporate several heuristics and select one to use according to simple rules, requiring significant time and expert effort to fine-tune in practice. The pervasion of Large Language Models (LLMs) provides a potential solution to address this issue. However, generating a CDCL solver from scratch is not effective due to the complexity and context volume of SAT solvers. Instead, we propose AutoSAT, a framework that automatically optimizes heuristics in a pre-defined modular search space based on existing CDCL solvers. Unlike existing automated algorithm design approaches focusing on hyperparameter tuning and operator selection, AutoSAT can generate new efficient heuristics. In this first attempt at optimizing SAT solvers using LLMs, several strategies including the greedy hill climber and (1+1) Evolutionary Algorithm are employed to guide LLMs to search for better heuristics. Experimental results demonstrate that LLMs can generally enhance the performance of CDCL solvers. A realization of AutoSAT outperforms MiniSat on 9 out of 12 datasets and even surpasses the state-of-the-art hybrid solver Kissat on 4 datasets.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google