LoMax: LLM‐Driven Local Code Optimization for MaxSAT Solvers

Abstract

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 +31$$ +31 $$ additional instances (average runtime 13.11 s →$$ \to $$ 14.27 s) on 553 unweighted instances and +23$$ +23 $$ additional solved instances (average runtime 11.67 s →$$ \to $$ 10.76 s) on 571 weighted instances, both under a uniform 100‐second timeout; OpenWBO solves +12$$ +12 $$ additional instances ( −8.9%$$ -8.9\% $$ 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.