Extracting Problem Structure with LLMs for Optimized SAT Local Search

These tools apply basic strategies that work well for random problems but miss critical patterns in structured instances. SAT encodings of real problems contain inherited patterns from graph layouts, data connections, and domain-specific rules. The transformation to Conjunctive Normal Form (CNF) obscures these patterns. Current local search methods skip these structures in favor of general approaches. This paper addresses these limitations by introducing a framework that leverages LLMs to generate local search strategies tailored to encoding structures, enabling solvers to take advantage of these patterns for improved performance. Our research addresses three questions: 1. How can LLMs analyze PySAT [Ignatiev et al., 2024] code to interpret how problem structure translates to SAT clauses? 2. How can we create local search strategies that recognize and exploit these encoding patterns?