Extracting Problem Structure with LLMs for Optimized SAT Local Search
This work addresses a domain-specific bottleneck in SAT solving by providing an incremental improvement to preprocessing techniques for researchers and practitioners in automated reasoning.
The paper tackles the problem of improving SAT solver performance by developing a method that uses Large Language Models to analyze Python-based encoding code and automatically generate specialized local search algorithms for preprocessing, resulting in faster solving times compared to baseline systems.
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.