LoMax: LLM-Driven Local Code Optimization for MaxSAT Solvers

The Maximum Satisfiability (MaxSAT) problem is a fundamental combinatorial optimization task, and state-of-the-art solvers rely on decades of expert-engineered heuristics and low-level micro-optimizations to achieve competitive performance. While recent Large Language Model (LLM)-driven approaches (e.g., FunSearch, SATLUTION) have shown promise in algorithmic design and global solver evolution, they either focus on high-level algorithmic sketches or large-scale code restructuring, leaving the potential of purely local, correctness-validated code optimization for industrial MaxSAT solvers largely underexplored in prior MaxSAT-focused studies. This paper presents LoMax, a plug-and-play framework that leverages an LLM to perform local code optimization for MaxSAT solvers. Without any human-written heuristics or instance-specific domain-specific templates (The prompts contain general MaxSAT domain knowledge but no instance-specific or benchmark-specific optimization templates), LoMax iteratively (i) ranks source files, (ii) scores individual functions, (iii) optimizes the highest-scoring function body, (iv) performs a fast sanity evaluation on a small instance set, and (v) validates it on full exact-unweighted and exact-weighted benchmarks. Experiments on two state-of-the-art solvers (UWrMaxSat-SCIP-MaxPre and OpenWBO) show consistent improvements: UWrMaxSat-SCIP-MaxPre solves (Formula presented.) additional instances (average runtime 13.11 s (Formula presented.) 14.27 s) on 553 unweighted instances and (Formula presented.) additional solved instances (average runtime 11.67 s (Formula presented.) 10.76 s) on 571 weighted instances, both under a uniform 100-second timeout; OpenWBO solves (Formula presented.) additional instances ((Formula presented.) average time) on 553 unweighted instances, providing empirical evidence that LLM-driven local code rewriting can improve the performance of industrial MaxSAT solvers in the evaluated settings.