# Extracting Problem Structure with LLMs for Optimized SAT Local Search

arXiv: https://arxiv.org/abs/2501.14630 · HTML: https://mlsanity.com/paper/2501.14630/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 24 Jan 2025.

## Built on by (most cited first, 2 of 2)

- [Discovering heuristics in a complex SAT solver with large language models](https://mlsanity.com/paper/2507.22876/) (2025)
- [Text2Model: Modeling Copilots for Text-to-Model Translation](https://mlsanity.com/paper/2604.12955/) (2026)

## Abstract (arXiv)

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.