Extracting Problem Structure with LLMs for Optimized SAT Local Search

Abstract

Encoding combinatorial problems in terms of propositional satisfiability (SAT) enables utilization of highly efficient SAT solvers for combinatorial search. Local search preprocess ing accelerates the SAT solver’s search by providing high quality starting points, a technique implemented in several modern SAT solvers. However, existing preprocessing meth ods employ generic strategies that fail to exploit the structural patterns inherent in problem encodings. This position paper proposes a novel paradigm wherein Large Language Models (LLMs) analyze problem encoding implementations to syn thesize specialized preprocessing algorithms. The LLMs ex amine Python-based code to identify structural patterns, en abling the automatic generation of encoding-specific local search procedures. These procedures operate across all in stances sharing the same encoding scheme rather than requir ing instance-specific customization. Our preliminary empir ical evaluation demonstrates effective automated algorithm synthesis for structure-aware SAT preprocessing, serving as a foundation for similar approaches across multiple domains of combinatorial optimization.