Bridging LLMs and SAT Solving: Automated Evolution of High-Performance Heuristics

1 Introduction

The Boolean Satisfiability Problem (SAT) was the first problem proven to be NP-complete and remains a cornerstone of computer science and logic [Cook, 1971]. Beyond its theoretical significance, SAT solving has become a critical industrial technology with applications spanning hardware and software verification, artificial intelligence, automated planning, and bioinformatics [Vizel et al., 2015;

Marques-Silva, 2008], thanks to the continuous development of SAT solvers over several decades, making the SAT formalism a highly competitive generic approach for solving complex real-world problems [Biere et al., 2021].

However, this success has led to a performance plateau: Modern solvers have become so sophisticated and finely tuned that achieving further significant improvements is increasingly difficult. Historically, manual SAT solver optimization has been a grueling process, requiring deep domain expertise, years of trial-and-error, and exhaustive experimental validation. For a human research team, designing an optimization to solve a few additional instances in a SAT competition benchmark often represents years of dedicated effort.

The emergence of Large Language Models (LLMs) offers a potential escape from this human-expert bottleneck. Unlike traditional heuristic design, which relies on intuition, LLMs can leverage complex patterns learned from vast datasets to generate novel, and sometimes counter-intuitive, algorithmic strategies [Naveed et al., 2025]. While AutoSAT [Sun et al., 2024] was the first framework to utilize LLMs for SAT policy optimization, its scope was limited. By targeting a relatively simple solver (easySAT [Chen and Zhang, 2022]) and utilizing unorganized requests for function improvements, AutoSAT lacked the deep optimization and structural diversification necessary to improve highly optimized solvers like Kissat MAB [Biere et al., 2020; Cherif et al., 2021].

In this paper, we propose AESAT (Auto-Evolving SAT solving), a novel memetic framework designed to automatically evolve SAT solver heuristics using LLMs. AESAT bridges the gap between neural generation and symbolic reasoning by:

1. Synergizing Individual and Evolutionary Search: It organizes LLM requests through a combination of local refinement and global evolutionary exploration.
2. Self-Optimizing Prompts: It employs a prompting mechanism that evolves based on historical performance data to maximize the LLM's generative potential.

The efficacy of our approach is demonstrated by AEKissat-MAB, a solver optimized via AESAT that won the main track of the 2025 International SAT Competition by a wide margin. This victory marks a historic milestone: the first time an LLM-enhanced solver has dominated this prestigious and rigorous competition. By providing a low-cost, automated alternative to manual engineering, AESAT offers a scalable path for optimizing solvers for SAT and other hard combinatorial problems, representing a paradigm shift in how we design reasoning algorithms.

The remainder of this paper is organized as follows: Section 2 reviews related works. Section 3 details the AESAT framework and its five core functions. Section 4 presents the application of AESAT to Kissat MAB, including a comparative analysis between LLM-generated and human-expert heuristics. Section 5 provides a comprehensive empirical analysis, and Section 6 concludes the paper.

2 RelatedWorks

As LLMs demonstrate increasing proficiency in structural reasoning and code generation, they are being used for combinatorial optimization as heuristic generators [Da Ros et al., 2025]. This shift allows researchers to treat strategy design as a language modeling task [Ye et al., 2024]. Current research in this domain can be broadly categorized into general optimization frameworks and SAT-specific applications.

2.1 LLM-Based Evolutionary Optimization

Several frameworks have pioneered the integration of LLMs into evolutionary loops. FunSearch [Romera-Paredes et al., 2024] demonstrated that LLMs can generate and evaluate code within an evolutionary framework to achieve breakthrough discoveries in combinatorial mathematics. Similarly, EvoPrompt [Guo et al., 2024] utilizes evolutionary algorithms to optimize the prompt templates, ensuring precise and structured LLM outputs. In the domain of traditional combinatorial tasks, LMEA [Liu et al., 2024b] couples an LLM with a genetic algorithm to serve as an evolution engine, automatically discovering efficient rules for the Traveling Salesman Problem. These works establish the feasibility of LLMs in structured search tasks but often focus on problems with simpler constraints than modern SAT solving.

2.2 LLMs in SAT Solving

Due to the extreme complexity and delicate internal dependencies of modern SAT solvers, LLM-driven improvements have only emerged very recently. AutoSAT [Sun et al., 2024] was the first framework to apply LLMs to SAT policy optimization. Using the EasySAT solver [Chen and Zhang, 2022] as a baseline, AutoSAT employed two strategies: Greedy Hill Climbing (GHC), which modifies functions sequentially, and an Evolutionary Algorithm (EA) that modifies multiple functions simultaneously. However, AutoSAT's approach has two primary limitations. First, if an LLM-generated modification fails initially, it is discarded without the fine-tuning necessary to unlock its potential-a critical flaw when dealing with highly optimized solvers where raw ideas require precise calibration. Second, its EA approach lacks a crossover operation due to its single-parent structure, limiting diversification.

Following the 2025 SAT Competition, SATLUTION [Yu et al., 2025] introduced an evolution framework that utilizes an LLM agent to combine the strengths of five state-of-theart baseline solvers. While SATLUTION reports impressive speedups over 2025 competition winners, it remains a humanin-the-loop system, requiring manual guidance for high-level search strategies. Furthermore, its resource intensity is substantial, requiring over 20,000 USD in computational costs and resulting in nearly 65,000 lines of code changes.

3 The AESAT Framework

We introduce AESAT (Auto-Evolving SAT solving), a lightweight framework designed to automatically refine and optimize a target heuristic function F within a modern SAT solver A. AESAT addresses the conventional "fine-tuning" bottleneck through a self-optimized prompting mechanism, and introduces a novel multi-parent evolutionary structure that fosters robust algorithmic diversification. To effectively coordinate and exploit these diverse strategies, the framework is built upon a Mixture-of-Experts (MoE) architecture [Wu et al., 2024; Chan et al., 2024]. Crucially, AESAT achieves these capabilities while maintaining significantly lower computational overhead and greater architectural simplicity than existing LLM-agent architectures.

This section details the underlying MoE architecture alongside the five core algorithms that govern AESAT.

3.1 Mixture-of-Experts (MoE) Architecture

The integration of the MoE architecture is grounded in the insight that no single large language model (LLM) excels uniformly across all optimization tasks. By deploying specialized models at distinct phases of the pipeline, AESAT maximizes the comparative advantages of diverse LLMs at distinct phases of the pipeline. Specifically, the framework orchestrates the heuristic optimization process by decomposing it into three specialized, synergistic roles:

Idea Generation (GPT-4.5): It leverages cross-domain knowledge to propose novel algorithmic concepts and diversify the search space.

Code Implementation in local optimization (Claude 3.7):

Known for high fidelity in structured code generation, it ensures that natural language concepts are translated into robust, compilable, and convention-adherent C code.

Idea Analysis and Code Implementation (DeepSeek-R1):

It utilizes superior logical reasoning and chain-ofthought capabilities to perform feasibility assessments and pattern recognition on failed or successful heuristics. It also generates C code for combining the strengths of two functions in a crossover operation.

3.2 Algorithmic Overview

AESAT explores the space of heuristic variants to optimize the target function F within a solver A. This orchestration is formalized in Algorithm 1. The framework takes as input the baseline function F , the solver A, a set of adaptive guidelines (tips), and a training set of SAT instances I. It outputs a synthesized function t∗ designed to replace F in A, maximizing solving performance as quantified by the Penalized

Algorithm 1 The AESAT Framework

Input: heuristic function F requiring optimization, SAT solver A, a set of tips, a set of training SAT instances I Parameters: populationSize

Output: an improved function t∗ and a set of adaptive tips

• 1: Call GPT with prompt: You are an expert SAT Solver Researcher. Analyze solver A and the existing heuristic F. Generate populationSize novel heuristic functions to replace F in A. Each generation must strictly adhere to the constraints defined in tips. The final output, set T , must contain populationSize individuals, each consisting of a formal natural language description
• 2: for each function t ∈ T do
• 3: t′ ← LocalOptimization(t, A, tips, I)
• 4: T ← (T \ {t}) ∪ {t′ }
• 5: end for
• 6: (t∗ , tips) ←EvolutionaryUpdate(T,A, F, tips, I)
• 7: return (t∗ , tips)

Average Runtime (PAR2) score 1 . We denote the PAR2 score of solver A executing a modified heuristic t on the dataset as PAR2(A, t), where a lower score indicates superior performance.

AESAT begins by calling GPT to generate populationSize functions to replace F in A, each represented in an individual. At this stage, the functions are described in formal natural language and no code is generated. Then AESAT performs local optimization for each function, and evolutionary exploration for diversification, described in the following subsections. Note that since each individual should be evaluated on the training set, an iteration in local optimization or evolutionary exploration takes much more time than in a classical memetic algorithm.

3.3 Local Optimization and Individual Refinement

Unlike classical memetic algorithms that rely on stochastic local search, AESAT employs Algorithm 2 (LocalOptimization) for individual refinement, which is more costly, because each individual needs to be evaluated on the training set. For an input function t, AESAT generates nbNeighbors variants through slight modifications, using the ancestral lineage and historical performance data to guide these modifications. The best variant is kept for the next iteration. This ensures that the search does not discard promising ideas prematurely, but instead fine-tunes them toward local optima.

3.4 Evolutionary Exploration and Selection

After individual refinement, Algorithm 3 (EvolutionaryUpdate) performs global exploration through a structured crossover. The DeepSeek-R1 identifies the most promising pairs (s1, s2) and synthesizes their strengths into a hybrid function t. To manage population health, AESAT employs

1 Consistent with International SAT Competitions, the PAR2 score of a solver on a set of instances is defined as the sum of runtimes for all solved instances plus twice the timeout threshold (2 × timeout) for any unsolved instances

Algorithm 2 LocalOptimization

Input: heuristic function t, solver A, set of tips tips, set of SAT instances I

Parameters: localOptimLimit, nbNeighbors, timeOut

Output: an improved heuristic function t

• 1: for i = 1 to localOptimLimit do
• 2: for j = 1 to nbNeighbors do
• 3: Call GPT with prompt: As a SAT solver researcher, read solver A and its base heuristic function t. Considering the ancestral lineage of t and adhering to guidelines in tips, generate a variant tj by applying slight modifications
• 4: Call Claude to generate the complete compliant C code implementation for tj according to its formal language description created by GPT
• 5: Run solver Awith tj for each instance in I, stopped by timeOut
• 6: Compute par2(A, tj) and record t as parent of tj
• 7: end for
• 8: t ← argmins∈{t1,...,tnbNeighbors} par2(A, s)
• 9: t ← UpdateHistory(t)
• 10: end for
• 11: return t

a heuristic fitness function q(t) that balances performance, innovation, and stochastic diversity:

where inn(t) is an innovation score assigned by the DeepSeek-R1 expert and r ∈ [0, 1) is a random perturbation to prevent premature convergence. The population is pruned by removing individuals below the median q(t) score while strictly preserving the global best in terms of PAR2.

This evolutionary process is repeated as long as T contains more than two individuals. When T converges to only two individuals, it returns the best function found so far.

3.5 Adaptive Meta-Learning

Whenever a function either enters or is generated by the evolutionary exploration phase (Algorithm 3), AESAT invokes DeepSeek-R1 to evaluate its performance against the Kissat4.0.2 MAB baseline via Algorithm 4. Guided by these performance insights, the framework triggers the PromptSelfOptimize mechanism (Algorithm 5) every roundSize iterations within the EvolutionaryUpdate loop. This metaanalysis of the ancestral lineage identifies recurring failure modes and suboptimal logic patterns, enabling the framework to refine its own tips (system prompt).

Through this self-correction, the systemmasters the metaprocess of "learning how to learn," progressively steering the evolution of the heuristics toward more promising directions.

4 Case Study: Optimizing the Branching Heuristic Selection for Kissat 4.0.2

Kissat is a highly optimized SAT solver [Biere et al., 2020] that constitutes the basis of most SAT solvers in recent SAT

Algorithm 3 EvolutionaryUpdate

Input: set of heuristic functions T, solver A, original function F requiring optimization, set of tips tips, set of SAT instances I

Parameters: roundSize, 0 < α, β, γ ≤ 1 such that α+β +γ = 1, timeOut in seconds

Output: An improved heuristic function t and tips

• 1: i ← 0
• 2: while T contains more than two functions do
• 3: Call DeepSeek-R1 with prompt: As a SAT solver researcher, perform crossover operations on the set T. For every pair of (s1, s2) in T deemed most promising based on their characteristics, analysis, and ancestral lineage, generate a new function t. The goal is to combine strengths while mitigating weaknesses. The output t must include complete compliant C code, strictly adhering to tips. Avoid exhaustive pairwise combinations.
• 4: for each new function t combining s1 and s2 given by DeepSeek-R1 do
• 5: RunAwith t for each instance in I, stopped by timeOut
• 6: Compute par2(A, t), and record s1 and s2 as parent1 and parent2 of t, respectively
• 7: T ← T ∪ {t}
• 8: t ← UpdateHistory(t)
• 9: end for
• 10: Call DeepSeek-R1 with prompt: For every heuristic t ∈ T , calculate its innovation score inn(t) by analyzing its description, C code and differences with other functions in T, and calculate the fitness score q(t) using Equation (1).
• 11: tbest ← argmint∈T par2(A, t)
• 12: Remove all t ∈ T such that q(t) is smaller than or equal to the median q in T
• 13: T ←T ∪ {tbest}
• 14: i ← i + 1
• 15: if i mod roundSize = 0 then
• 16: tips ← PromptSelfOptimize(tbest, tips)
• 17: end if
• 18: end while
• 19: tbest ← argmint∈T par2(A, t)
• 20: return (tbest, tips)

competitions. It frequently restarts its search. Each restart develops a binary search tree and can use a different branching heuristic for this. Cherif et al. [2021] integrated a function called restart MAB (Multi-Armed Bandits) into Kissat to select a branching heuristic among VSIDS [Moskewicz et al., 2001] and CHB [Liang et al., 2016] in the stable mode. The resulted solver is called Kissat MAB and won the 2021 SAT competition with a large margin.

This section first presents the restart MAB function, and then describes in details a real evolutionary trajectory produced by AESAT when optimizing it, so that the reader can visualize how AESAT's operations parallel or diverge from those a human expert would perform to achieve similar evo-

Algorithm 4 UpdateHistory

Input: heuristic function t

Output: heuristic function t

• 1: Call DeepSeek-R1 with prompt: Perform a detailed comparative analysis of heuristic t against its baseline. This analysis must encompass differences in their natural language descriptions, C code, and par2 scores. Based on this comparison, record a concise explanation in t, detailing the reason for t's observed performance improvement or degradation relative to Kissat4.0.2 MAB.
• 2: return t

Algorithm 5 PromptSelfOptimize

Input: heuristic function t, set of tips tips

Output: set of optimized tips

• 1: Call DeepSeek-R1 with prompt: As a system feedback mechanism, analyze heuristic t and perform a detailed comparison against its entire ancestral lineage across four criteria: natural language description, C code, par2 score, and existing performance analysis. Based on identified failures, errors, or suboptimal design choices, update the document tips to prevent the recurrence of the same issues or incorrect design directions in all future generations.
• 2: return tips

lutions of heuristics.

4.1 Function Restart MAB

Consider a restart R using the branching heuristic h. The restart MAB function assigns it a reward. Let #decisions denote the number of internal nodes in the tree developed by R, and #conflicts denote the number of leaves. We use below a reward for R defined in [Liu et al., 2024a]:

For each heuristic h ∈ {VSIDS, CHB}, let nh denote the number of restarts using h, and ¯ r(h) denote the average reward obtained across the nh restarts using h. After ntotal = nV SIDS + nCHB restarts, the restart MAB function defines the score of h using the Upper Confidence Bound (UCB) strategy as follows:

UCB(h) contains two terms: the exploitation term ¯ r(h) and the exploration term √ 4×ln(ntotal) nh , called xpr1(h) in the sequel. The restart MAB function returns the heuristic with the highest UCB score, that will be used in the next restart. So, optimizing restart MAB is equivalent to optimizing the UCB function. Note that xpr1(h) penalizes the heuristic with high nh.

We integrate the above restart MAB function into Kissat 4.0.2 2 to create our baseline Kissat4.0.2 MAB, where Kissat 4.0.2 is a successor of Kissat 4.0.0 [Biere et al., 2024], the winner of the 2024 SAT competition with a wide margin. Then, we task AESAT with evolving the UCB function to improve the performance of Kissat4.0.2 MAB on a benchmark set I of 60 instances randomly selected from the 2024 SAT Competition.

In the sequel, each new UCB function, as well as intermediate terms, will be defined in an equation, and an equation can use the functions defined in previous equations. The performance of a new UCB function is defined to be the performance of Kissat4.0.2 MAB using this UCB function instead of Equation (3), measured by the PAR2 score.

4.2 Evolutionary Trajectory of Heuristic Discovery

As previously described, AESAT evolves heuristics through a local optimization stage followed by an evolutionary stage. This subsection illustrates this two-stage process as applied to the restart MAB function, followed by an adaptive metalearning.

Local Refinement

To begin, AESAT feeds the source code of Kissat4.0.2 MAB and specially restart MAB to LLMs, and calls GPT to generate 20 (populationSize) restart MAB functions, each with a different UCB definition. After this, Algorithm 2 is called to optimize locally each of the 20 functions.

For example, the seventh function t7 introduces hysteresis by temporarily boosting the UCB score of a newly selected heuristic h to prevent rapid and unstable switching. The first cycle of local optimization of t7 in Algorithm 2 begins by calling GPT and Claude to generate three variants of t7, of which t7.1 boosts UCB(h) by a factor of 1.2:

In variant t7.3, the boost is not a factor, but a fixed bonus a = 0.05 × ntotal :

All the three variants are evaluated on I and t7.1 is found to be the best. The next cycle of local optimization begins by calling LLMs to generate three variants of t7.1, among which t7.1.2 boosts UCB(h) for the next three successive restarts after h is switched on, its value being multiplied by 1.2, 1.1 and 1.05, respectively, similar to Equation (4). After evaluation, it is found to be the best variant among the three variants.

The next cycle identifies t7.1.2.2 to be the best among three variants of t7.1.2, which boosts UCB(h) by a factor f = 1.5×

2 https://github.com/arminbiere/kissat

0.85k , if h is just used for k consecutive restarts. This is the final function returned by optimizing t7.

The same local optimization process is applied to functions t11 and t13, where t11 divides the raw reward of heuristic h by a value depending on nh, and t13 uses an entropy-guided selection mechanism that prefers the heuristic with higher reward variance when its UCB score is not too bad, favoring uncertain but high-potential options.

After several cycles, an optimized variant t11.3.3.2 for t11 is identified. It uses the same second term xpr1 in the right as in Equation (3), but a normalized reward rn:

where rn is normalized by considering the average numbers of internal tree nodes and leaves, avg10h(#decisions) and avg10h(#conflicts), respectively, in the 10 previous restarts using h. Concretely:

And t13.1.2.1, a locally optimized variant of t13, is also obtained:

where var(r(h)) is the variance of r(h) (see Section 4.3).

Evolutionary Exploration

After locally optimizing each individual, AESAT performs evolutionary update by calling Algorithm 3 to combine promising individuals. The combining of UCB7.1.2.2 and UCB13.1.2.1 gives

(10)

where ¯ rw(h) = ¯ r(h) × w with w = 1.0 + e-0.01×ntotal × var(r(h)) borrowed fromUCB13.1.2.1, ¯ rwf (h) = ¯ rw(h) ×f , with f = 1.5 × 0.85k borrowed from UCB7.1.2.2(h).

With a q score 0.63, UCB7+13 yields a 6.83% improvement of the PAR2 score relative to the baseline Kissat4.0.2 MAB. According to DeepSeek-R1, this improvement is achieved by combining variance-aware reward adjustment with decaybased exploration control in the UCB selection, enhancing the balance between exploitation and exploration for heuristic switching.

In this case study, UCB7+13 is the first function generated by LLMs that achieves an improvement relative to Kissat4.0.2 MAB, all previous functions being worse. For example, UCB13.1.2.1 results in a 30.46% degradation in the PAR2 score relative to the baseline. According to DeepSeek-R1, this degradation occurs because the entropyguided mechanism excessively prioritizes exploration by incorporating variance into UCB scores, causing suboptimal heuristic selection when scores are close and disrupting the exploitation-exploration balance.

UCB7+13 is then combined with UCB11.3.3.2 to give UCB7+13+11.

The computation of ¯ rnpwb(h) and ¯ rnpwbfs(h) is done in several steps. In the first step, let recentAVG5h denote the average of rn(h) in the last 5 restarts using h and oldAVG5h the average of rn(h) in the 5 restarts using h just before the last 5 restarts using h. A trend factor ph = 1.0 + 0.3 × (recentAVG5h - oldAVG5h)/oldAVG5h is added:

Let wn(h) = (1.0 + e-0.01×ntotal × var(rn(h))), similar as in UCB7+13.

Let recentAVG3h denote the average of rn(h) in the last three restarts using h and bh = 1.0 + 0.2 × (recentAVG3h - ¯ rnpw(h))/¯ rnpw(h) be a bonus computed using the last three restarts using h. We have

Finally, let f = 1.5 × 0.85k as in UCB7.1.2.2(h) and UCB7+13, and s = 1.0 + 0.1 × ln(k + 1). We have

With a q score 0.73, UCB7+13+11, although complex, yields a 12.26% improvement w.r.t. Kissat4.0.2 MAB on I.

Adaptive Meta-Learning

After a round, AESAT calls DeepSeek-R1 to optimize the tips by analyzing the performance reasons of all individuals so far. For example, the following tips are added:

• Do not attempt to excessively adjust exploration rate parameters to avoid performance instability
• Deeply attempt dynamic reward function optimizations, especially adjustments based on the number of conflicts
• Avoid complex implementations; focus on simple, effective modifications
• Thoroughly test strategies that combine learning rates and rewards

4.3 Observations: LLMLogic vs. Human Intuition

The most significant finding of this case study is that AESAT discovered algorithmic strategies that diverge fundamentally from human expert intuitions. We highlight three counterintuitive implementations:

The Average-Subtraction RollingWindow: UCB7+13+11 needs to compute the average of k last rewards r. For this, it computes a rolling sum. A human usually computes this rolling sum by removing the oldest reward and adding the new one (Snew = Sold - rn-k + rnew). However, UCB7+13+11 subtracts the average of the current window before adding the new value. This sounds as a self-correcting normalization factor that prevents reward saturation in long-running solver instances.

Unorthodox Variance Computation: When computing the variance var(r) of a reward r, a human would use the Welford method. However, the computation of var(r) by LLMs is very hard to understand and interpret in UCB7+11+13. Let d be an intermediate value initialized to the first reward r1, and m denote the number of rewards so far. When a new reward rm+1 arrives, LLMs update d to

Let ¯ r denote the average of rewards so far, LLMs calls Equation (17) the variance var(r) of r:

Multi-Tiered Trend Analysis: Human experts rarely implement nested trend factors (ph, bh) due to the extreme difficulty of manual tuning. AESAT successfully balanced these overlapping feedback loops, which LLMs analyzes as "optimizing the balance between historical stability and rapid adaptation."

Note that LLMs use standard identifiers such as variance or rollingSum within the generated C code, even when the underlying logic is fundamentally different. Without the granular focus provided by AESAT, these subtle but powerful deviations from classical arithmetic would likely remain hidden. Indeed, such insights would be significantly more difficult to uncover if AESAT were tasked with optimizing a solver's global architecture rather than its localized functions. By constraining the LLM's creative search to discrete components, AESAT allows human experts to audit, identify, and eventually adopt these novel machine-logic strategies.

4.4 Discussion: AESAT vs AutoSAT

In frameworks like AutoSAT [Sun et al., 2024], the 20 initial functions generated in this study would have been discarded because they performed worse than the baseline. However, through its memetic architecture, AESAT recognized the latent potential in these worse functions. By applying LocalOptimization to refine the factors (like the boost factor f) and EvolutionaryUpdate to cross-pollinate ideas (like combining t7 and t13), AESAT navigated a fitness landscape that is inaccessible to simple hill-climbing or single-parent approaches.

5 Experiments

This section provides a rigorous quantitative evaluation of AESAT. We first demonstrate its ability to discover high performance SAT solvers across multiple competition datasets, by evaluating four functions it generated. Then, we present an ablation study to isolate the impact of different components of AESAT and the impact of the counter-intuitive heuristics discovered by the LLMs.

Benchmark Datasets: We evaluate AESAT using the official datasets from the SAT Competitions 2022-2025. Each year's dataset comprises 400 instances originating from diverse industrial and theoretical domains.

Experimental Setup: All experiments were conducted on a server equipped with an AMD EPYC 9654 processor unless otherwise stated. The training set comprise 60 instances randomly selected from the SAT Competition 2024 dataset. The parameters were initialized as follows: populationSize = 20, roundSize = 5, localOptimLimit = 5, nbNeighbors = 3, timeOut = 5000s as in the SAT competitions, α = 0.4, β = 0.4, γ = 0.2. The source code of AESAT and Kissat4.0.2 MAB with all tested UCB functions, as well as the set of 60 training instances, are available in the supplementary materials 3 .

5.1 Four Functions Generated by AESAT

Each call to AESAT returns a new function in 30-40 hours for roughly 0.50 USD, representing a significant cost reduction over the 20,000 USD SATLUTION [Yu et al., 2025]. Furthermore, 46% of the UCB functions surpassing the baseline on training set I maintained their superiority on the full datasets.

To demonstrate the framework's versatility, we evaluate the following four functions returned by AESAT. The first three provide optimized implementations of the UCB selection logic in restart MAB, as illustrated in Section 4.2. The fourth replaces kissat bump score increment, demonstrating that AESAT's capabilities extend to various components of the solver.

UCB7+13+11: Defined in Equation (11).

UCBsc2025: Defined in Equation (18), where r(h) is defined by Equation (2), m is a momentum coefficient initialized to 1. Let {R1, . . . ,R10} be set of the 10 last restarts, hi (1 ≤ i ≤ 10) be the heuristic used in restart Ri, avg10(¯ r) = 1 10 ∑10 i=1 ¯ r(hi). After a restart using h, if ¯ r(h) > avg10(¯ r), m is updated to m × 1.1, otherwise m is updated to m × 0.9.

UCBxpr2: Defined in Equation (19), where xpr2 is defined in Equation (20).

BumpInc: In the VSIDS heuristic, each variable's score is initialized to 0. Following every conflict, the scores of involved variables are incremented by a value, scinc, which starts at 1 and is progressively scaled by a factor of 1 1-decay , where decay is a fixed constant in the baseline Kissat 4.0.2. The kissat bump score increment function governs the evolution of this scinc value.

3 https://github.com/FSQH-dh/AESAT

AESAT was applied to optimize this component in Kissat 4.0.2, yielding a new implementation of kissat bump score increment defined in Equations (21)-(23). The resulting solver is called BumpInc.

Let scinc denote the current score increment value also starts at 1, d0 denote the original decay of Kissat4.0.2, MAX SCORE the upper bound of the VSIDS score, and ratio = scinc/MAX SCORE. The dynamic decay ddyn is defined as:

(21)

Then, a compensation-adjusted growth factor g is defined in Eq. (22) to replace the original constant factor 1 1-decay .

Finally, the new score increment scincnew is calculated in Eq. (23) using g after every conflict.

Note that the new factor g is adaptive, allowing to increase scinc more rapidly when it is small, while the original factor 1 1-decay is a fixed constant.

Table 1 shows the standard performance metrics as in SAT competitions: the number of (ALL, SAT, UNSAT) instances solved by Kissat4.0.2 MAB with UCB7+13+11, UCBsc2025, UCBxpr2, and Kissat4.0.2 with BumpInc, respectively, instead of the original heuristic functions, and their mean PAR2 score, against the baselines Kissat4.0.2 MAB (Base MAB in the table) and Kissat4.0.2. The first three functions globally perform better than the baselines. The fourth function BumpInc solves more unsatisfiable instances than the baselines. Especially, Kissat4.0.2 MAB with UCBsc2025 is the solver AE-Kissat-MAB that won the main track and the SAT track of the 2025 SAT competition with a wide margin. Additionally, Kissat4.0.2 with BumpInc is the solver AE-KissatBump that won the bronze medal in the UNSAT track of the 2025 SAT Competition, solving more unsatisfiable instances than Kissat-public, the newest version of Kissat participating in the competition and winning the silver medal in the main track (SAT+UNSAT).

5.2 Ablation Study

We first present ablation studies to isolate the performance impact of each AESAT component. Recognizing that AESAT frequently identifies strategies at odds with expert intuition, we also perform a comparative analysis to characterize the differences between LLM-synthesized search logic and conventional human logic.

Note: The experiment in Figure 1 was conducted on the complete SAT Competition 2024 dataset (400 instances) using a different server configuration from Table 1. The experiments in Figure 2 and in Figure 3 were conducted on the training set I of 60 instances described in the Experimental Setup. All experiments in this ablation study are performed by optimizing the MAB function.

Effectiveness of PromptSelfOptimize. To evaluate the contribution of the PromptSelfOptimize mechanism (Algorithm 5), we track the performance of 93 UCB functions returned across successive runs of AESAT. Figure 1 shows the number of instances solved by each returned function on the 2024 dataset, with the baseline Kissat4.0.2 MAB solving 318 instances. A linear regression line is fitted using ordinary least squares (OLS), and it exhibits a positive slope, indicating that the later runs of AESAT tend to discover better performing heuristic functions. This upward trend is attributed to the PromptSelfOptimize mechanism, which periodically refines the prompt guidelines (tips) based on historical successes and failures, effectively steering the LLM's search toward more fruitful algorithmic directions over time.

Effectiveness of EvolutionaryUpdate. To isolate the impact of the crossover operation within EvolutionaryUpdate (Algorithm 3), we analyze how locally refined functions are transformed into hybrid variants. Figure 2 contrasts the bestperforming locally optimized function against the top hybrid function for each execution of AESAT on the training set I, illustrating their relative improvements over the baseline. Notably, 82% of the best locally optimized functions already surpass the baseline, validating the standalone efficacy of LocalOptimization. Crucially, in 64% of the runs, the best hybrid function further improves upon its locally optimized counterpart, with the peak global hybrid yielding a 36.6% improvement relative to the baseline. This trend confirms that EvolutionaryUpdate introduces vital optimization and diversification beyond what local refinement alone can achieve.

PromptSelfOptimize Effectiveness

Effectiveness of LocalOptimization. To isolate the contribution of LocalOptimization (Algorithm 2), we evaluate an ablated variant of AESAT that bypasses the local refinement phase entirely: 20 initial ideas are generated and, postevaluation, immediately passed to the EvolutionaryUpdate stage. Figure 3 illustrates the results across 35 independent runs of this variant on the training set I. Without LocalOptimization, only 28.6% of the best initial ideas outperform the baseline-a stark contrast to the 82% success rate observed in the full pipeline (Figure 2). Despite this initial deficit, EvolutionaryUpdate successfully generates hybrid functions that improve upon the best initial seed in 82.9% of the runs, underscoring its robust complementary efficacy. However, omitting local refinement caps the maximum global improvement relative to the baseline at just 25.8%, compared to the 36.6% global improvement achieved when LocalOptimization primes the evolutionary search (Figure 2).

Comparative Ablation: LLM Logic vs. Human Intuition. As the case study in Section 4 suggests that AESAT discovers strategies fundamentally different from human intuition, we conduct a comparative ablation study on UCB7+13+11. By replacing the machine logic observed in Section 4.3 with usual human-expert implementations, we aim to determine whether these counter-intuitive discoveries provide a measurable performance advantage over traditional heuristics.

UCBrolling7+13+11 : The rolling sum of rewards in the last k restarts is done as usually, i.e., when a new reward arrives, subtract the oldest reward and add the new one.

UCBvar7+13+11 : The variance of rewards is computed using the Welford method.

UCBrecency7+13+11 : The last recent performance bonus bh is discarded.

The results shown in Table 2 on the 2025 dataset are striking: reverting to human practices for variance, rolling sums and trend analysis degrades performance significantly. In fact, using standard human implementation methods for these specific components caused the solver to perform worse than the LLM version (e.g., PAR2 increasing from 1884 to 2379). This suggests that the LLM-discovered heuristics are not just faster, but capture subtle search-space dynamics that standard arithmetic fails to address.

6 Conclusion

In this paper, we introduced AESAT, a multi-agent, autoevolving framework designed to optimize the delicate and complex heuristics of modern SAT solvers. By a memetic evolutionary loop, AESAT moves beyond traditional blackbox algorithm configuration, enabling the discovery of entirely new and efficient algorithmic logic. The ablation study shows that every component of AESAT contributes to the performance of AESAT.

Our empirical evaluation demonstrates that AESAT can achieve quickly significant performance gains that could require years of effort from human teams to obtain. More crucially, our analysis reveals that AESAT achieves these results by evolving machine logic that often contradicts human intuition. From the average-subtraction rolling sum to unorthodox variance estimations, AESAT successfully explores a design space that has remained largely untapped by human experts. The success of UCBsc2025 and BumpInc in the 2025 SAT Competition serves as a definitive validation of this approach.

AESAT represents a paradigm shift from manual tuning to automated discovery, ensuring that even complex, multilayered ideas-which are traditionally prone to failure during initial implementation-can be refined into competitive heuristics. This reduces the barrier to entry for developing high-performance solvers.

Acknowledgments

This work was partially supported by National Natural Science Foundation of China (NSFC) under Grant 62402164 and by the French National Research Agency (ANR) under the Chair MASSAL'IA (ANR-19-CHIA-0013-01), cofunded by the French electricity distribution network operator Enedis. It was granted access to HPC resources of "Plateforme MatriCS" within University of Picardie Jules Verne, co-funded by the European Union with the European Regional Development Fund (FEDER) and the HautsDe-France Regional Council. And it was supported by the Hubei provincial key laboratory of green intelligent computing power network, China.