DynamicSAT: Dynamic Configuration Tuning for SAT Solving

The Boolean Satisfiability (SAT) problem is a fundamental problem in computer science and logic, which involves determining whether a given propositional formula is satisfiable. Specifically, the SAT problem is defined over a propositional formula in Conjunctive Normal Form (CNF). Let $X$ be a set of propositional variables. A literal $l$ is either a variable $x\in X$ or its negation $\neg x$. The clause $C_i$ is defined as the disjuction of literals and CNF formula $F$ is a conjunction of $m$ clauses.

Solving the SAT problem is formulated as determining whether there exists an assignment $A=l_1,l_2,\mathrm{\dots },l_n$ that leads the formula $F$ to evaluate to logic-1 (i.e., $F$ is satisfied). If no such assignment exists, the formula $F$ is said to be unsatisfiable.

Modern Boolean Satisfability solvers primarily rely on Conflict-Driven Clause-Learning (CDCL) as their core algorithm [28], supplemented by various heuristics to efficiently address this NP-hard problem. In a CDCL solver, the problem instance is represented in Conjunctive Normal Form (CNF), which consists of a conjunction of clauses, where each clause is a disjunction of literals.

Over the past decades, numerous solving heuristics have been developed to accelerate the systematic exploration of potential solutions while leveraging learned conflicts to prune the search space. For example, clause vivification [23] reduces the search space by simplifying clauses through partial resolution, effectively strengthening constraints to eliminate redundancies. Chronological backtracking [32] revisits decisions in the reverse chronological order, avoiding expensive backtracking to arbitrary points in the decision tree. Besides, restart strategy [12] periodically restart the search process to escape local minima and improve convergence on hard instances. While these heuristics and their corresponding configuration parameters significantly enhance solver performance, determining the optimal configuration before or during SAT solving remains a critical challenge.

Currently, SAT solvers employ a range of parameterized heuristics, with solver performance on a given instance being highly dependent on the choice of parameters [18]. Identifying an optimal parameter configuration for specific instances is critical to improving performance. One representative approach focuses on determining the best configuration for a set of CNF instances from a training set [17, 2, 16]. These methods often use diverse search strategies, such as iterated local search [17], genetic algorithms [2], and model-based optimization [16], to optimize configurations for a given set of instances. However, this search process requires time-intensive trials to evaluate configuration candidates, making these methods inefficient for application on a per-instance basis.

For instances with intrinsic differences, solving them under distinct configurations is generally more effective than using a single configuration across all instances. Instance-specific algorithm configuration (ISAC) [20] addresses this by clustering CNF instances based on their features using g-means clustering. Each cluster, composed of similar CNFs, then applies a search-based configuration strategy to identify optimal parameter settings. When encountering a new instance, ISAC assigns it to the nearest cluster and applies that cluster’s configuration to the instance. Malitsky et al. [27] further enhance ISAC by introducing adaptive clustering, allowing the model to adjust clusters as new instances are added.

While these approaches have demonstrated performance gains by selecting appropriate parameters for individual instances, they do not address the dynamic changes that occur throughout the SAT solving process. As the characteristics of a CNF evolve during solving, the most effective strategy may also shift [7].

The Multi-Armed Bandit (MAB) problem [21] is a fundamental framework in reinforcement learning and decision-making under uncertainty. It models scenarios where an agent iteratively selects actions (termed “arms”, $A=\{a_1,a_2,\mathrm{\dots },a_T\}$) to maximize cumulative rewards $\sum r_t(a_t)$ while balancing exploration (gathering information about under-tested arms) and exploitation (leveraging known high-reward arms). Common approaches to solving MAB problems include algorithms such as $ϵ$-greedy, Upper Confidence Bound (UCB), and Thompson Sampling. These methods estimate the expected reward for each arm while efficiently managing the exploration-exploitation trade-off. For instance, UCB selects arms based on an optimistic estimate of their potential, while Thompson Sampling uses Bayesian inference to sample actions according to their probability of being optimal.

Since there is no explicit functional relationship between maximizing total expected reward and the selection of arms, MAB is particularly well-suited for addressing black-box optimization problems. This makes MAB-based approaches highly effective for dynamically adjusting configurations or strategies during the solving process, where accurately modeling the reward function is challenging. Previous work, such as Kissat-MAB [7], employs MAB to dynamically select between two state-of-the-art SAT solving heuristics: Variable State Independent Decaying Sum (VSIDS) and the Conflict History-Based (CHB) branching heuristic. Similarly, [24] formulates the decision of whether or not to trigger a solver reset as a MAB problem. However, these approaches focus narrowly on optimizing specific configurations rather than providing a generalized framework for handling arbitrary heuristics with minimal engineering effort.

In this work, we model configuration tuning as a MAB problem and propose a general reward and action formulation that supports a wide range of heuristic configuration parameters. This approach offers a versatile solution for dynamically optimizing SAT solver performance while minimizing the need for extensive engineering effort.

The Boolean Satisfiability (SAT) problem can be defined defined over a propositional formula in conjunctive normal form (CNF). Let the initial CNF instance be denoted as Eq (1), where $C$ represents a clause, and $m$ is the number of clauses. We denote the CNF formula at variable decision step $t$ as $F_t$ and the initial CNF is $F_0$. During the execution of a Conflict-Driven Clause Learning (CDCL) SAT solver, the CNF formula evolves dynamically due to unit propagation and clause learning, clause elimination mechanisms.

Given the structural divergence quantified by $sim(F_t,F_0)$, the initial configuration ${\mathrm{\Omega }}_0$ becomes suboptimal for $F_t$. We formalize on-the-fly parameter tuning as a decision-making problem where the action is how to adjust the parameters and the goal is to reduing solving time. To achieve this, we adopt the MAB algorithm to dynamically optimize solver behavior.

Figure 2 demonstrates the proposed MAB-based solving process, where the initial problem instance is denoted as $F_0$ and the sampled intermediate instances are $F_1,F_2,F_3,\mathrm{\dots }$. When the dynamic changes in the CNF instance meet a predefined trigger condition $\mathrm{\Delta }\Vert F\Vert \ge \theta$ (see Section 3.3.1), the MAB-based configuration tuning process is initiated, consisting of three stages: Sampling, Decision, and Free (see Section 3.4). The DynamicSAT serves as a plug-in within the SAT solver and repeats iteratively until the solver terminates to reduce solving time.

We opt for Upper Confidence Bound (UCB) algorithm [1] to implement our MAB-based configuration tuning. For each arm $a$, there are the following relevant parameters:

• $\mathrm{■}$

  $N(a)$ represents the number of times arm $a$ is selected in the previous of evaluations.

• $\mathrm{■}$

  $𝔼(a)=\frac{\sum r(a)}{\mathrm{\#}a}$ represents the expected reward of arm $a$ over the previous of evaluations, where $\mathrm{\#}a$ is the total number of arm $a_k$ selected.

The confidence upper bound for each action can be expressed as Eq. (11), where $i$ is accumulated times of MAB decision in the current configuration tuning iteration until now.

The UCB algorithm selects the arm that maximizes the value on the right side of the above formula as the current action, and reduces its uncertainty as the number of selections increases, balancing exploration and exploitation.

In DynamicSAT, we divide each configuration tuning iteration into three stages: Sampling, Decision and Free, as shown in Algorithm 1. This approach ensures a balance between exploration and exploitation while maintaining computational efficiency and flexibility. We define the hyperparameters $\theta$ represents the formula change threshold, $d$ is the intervals of MAB decision making and $\mu$ is the sampling frequency. In the default setting, we assign $\mu =1000$, $\theta =30\%$ and $d=100$, which are explored in Section 4.2.

Once the trigger condition satisfied (Line 3), the MAB process initiates exploration by dynamically selecting actions through random sampling (Line 18). For each action $a_i$, the reward $r(a_i)$ is collected according to Eq. (10) (Line 14) and expected value $𝔼(a_i)$ is iteratively updated (Line 15). This stage prioritizes exploration to gather sufficient data for the current intermediate instance, ensuring the policy avoids premature convergence to suboptimal configurations.

Then, once exploration concludes (no_sampling=0), the algorithm shifts to exploitation. Here, the updated policy guides the selection of action arms to maximize the reward, using UCB value (Line 26, Eq. (11)). Configuration parameters $\mathrm{\Omega }$ are adjusted based on the arm with the highest UCB value.

After both sampling and decision, the MAB-based process is disabled (Line 29). The solver keeps the current optimal configuration until the next trigger condition is met. Besides, the UCB value of each action is cleared before the next iteration.

Our DynamicSAT can be seamlessly integrated into the modern SAT solvers with minimal engineering effort, while also supporting configuration tuning for arbitrary heuristics. We opt for Kissat-4.0.0 (Kissat-sc24), the winner of SAT Competition 2024 [4] as the baseline solver. To demonstrate the effectiveness of DynamicSAT, we introduce specific variants (named DSAT-[heuristic]) that integrate with the baseline solver and allow for the dynamic tuning of multiple heuristic options. For instance, the variant named DSAT-chrono refers to the solver where the options related to chronological backtracking [32] are dynamically tunable during runtime. Specifically, the baseline solver provide two options: –chrono and –chronolevels.

In our MAB setting, sampling occurs at intervals of every $p$ decision rounds, with the decision phase triggered when the number of processed clauses reaches $\theta$ of the total clauses in the original CNFs. For each MAB iteration, DynamicSAT conducts sampling for $s$ times before making decisions based on the UCB value. To ensure consistency, we use the same random seed across all experiments, eliminating the effect of randomness. All experiments are conducted on an Intel(R) Xeon(R) CPU E7-8860 v4 @ 2.20GHz with 128GB memory. The timeout is set to 5,000 seconds of CPU time.

We test the effectiveness of DynamicSAT on the 2024 SAT Competition Benchmark [19] and evaluate using three metrics.

• $\mathrm{■}$

  Problem Solved (#Solved): The number of problem instances that can be solved within time limit. A higher value indicates better solver performance.

• $\mathrm{■}$

  Solving Time of Solvable Instance (Time): The average runtime for successfully solved instances by baseline solver, which investigate whether DynamicSAT negatively impacts the performance on these relative easy instances. A lower value indicates better solver performance.

• $\mathrm{■}$

  Average Par2 Score (Par2): The Par2 score sums the solving time for successfully solved instances and applies a penalty of twice the time limit for instances that timeout. In our experiments, we report the average Par2 score. A lower Par2 score indicates better solver performance.

DynamicSAT’s performance hinges on three critical hyperparameters: the initial sampling frequency ($\mu$), the clause change threshold ($\theta$), and the decision interval ($d$). We analyze their impact using DSAT-chrono on the the benchmark, with results summarized in Table 1. All experiments fix two hyperparameters while varying the third, with results summarized in Table 1.

To quantify the impact of integrating DynamicSAT on various in-processing heuristics¹¹1We do not adjust the pre-processing heuristics (e.g., fastel and lucky), as they are executed only once before the solving process., we choose 10 heuristic strategies randomly and evaluate the corresponding DynamicSAT variants. The complete list of tunable heuristics and their corresponding options is provided in Table 7 in Appendix A.1. Table 2 compares their performance against the baseline solver on the 2024 SAT Competition Benchmark. It should be noted that the runtime includes DynamicSAT, even though it occupies a small portion of the overall time (see discussion in Appendix A.3). We conclude three observations from the results.

First, the results reveal that all 10 solver variants powered by our proposed DynamicSAT consistently outperform the baseline solver across all metrics. On average, DynamicSAT achieves a 3.63% increase in #Solved (310.90 vs. 300), 32.30% solving time reduction (568.49 vs. 839.70) on solvable instances and 13.42% Par2 reduction (2,709.68 vs. 3,129.77), confirming the robustness of our approach across diverse heuristics. Besides, Figure 3 further illustrates the superiority of DynamicSAT: the curves of all 10 variants rise steadily over time, consistently surpassing the baseline’s plateau.

Second, the most significant improvements arise from heuristics directly interacting with the clause database. Notably, the top-performing variant DSAT-compact solve 5.33% more instances than the baseline, with a 19.23% reduction in Par2 score, demonstrating its superior efficiency and effectiveness. Simiarlly, DSAT-transitive also achieves 5.33% more instances solved. These strategies adaptively prune redundant clauses and simplify implication graphs during critical phases of structural divergence [6]. Since these heuristics are more sensitive to the structural CNF changes, tuning their corresponding parameters ensures optimal configuration.

Third, heuristics focusing on localized variable operations exhibit marginal gains, where DSAT-vivify and DSAT-bump only reduce Par2 score by 3.23% and 6.82%, respectively. Such strategies, which optimize literal-level properties or activity scores, lack systemic alignment with the solver’s evolving state [25, 23]. Their localized impact and insensitivity to structural CNF shifts prevent them from benefiting meaningfully from dynamic adaptation. Moreover, we further analyze that DSAT-vivify performs particularly worse on UNSAT cases, as detailed in Section 4.4.

Therefore, our experiments highlight that DynamicSAT excels when the tunable heuristics interact with global structures but struggles with contextually isolated optimizations. Our DynamicSAT also supports tuning more options with complex interactions, which is considered as the future work and briefly discussed in Appendix A.2.

We investigate the reasons behind the the negative impacts observed with DSAT-vivify in this subsection. To further dissect the efficacy of DynamicSAT, we analyze its performance separately on satisfiable (SAT) and unsatisfiable (UNSAT) instances from the 2024 SAT Competition Benchmark. This distinction is critical, as SAT and UNSAT instances impose fundamentally different demands on solvers: SAT solutions require efficient search space navigation, while UNSAT proofs depend on conflict analysis and clause learning [33].

For satisfiable instances, DynamicSAT variants demonstrate substantial efficiency gains. In Table 3, adjusting heuristics compact achieves 41.89% Par2 reduction, while DSAT-transitive reduces the average solving time by 47.43% compared to the baseline. Although some variants, such as DSAT-bump and DSAT-eliminate, show only minor improvements in the number of solved instances, they remain effective by achieving significant reductions in both Par2 scores and solving time. For example, DSAT-bump does not solve any additional instances but still reduces the Par2 score by 17.24% and the solving time by 26.01%.

In contrast, unsatisfiable instances reveal a more nuanced performance landscape. While most DynamicSAT variants still outperform the baseline, variable-centric heuristics like DSAT-vivify exhibit limited gains, which aligns with the results in Section 4.3. To be specific, the worst-performing variant, DSAT-vivify, solves 1.99% fewer instances than the baseline solver and shows negative gains in solving time and Par2 score, with increases of 1.08% and 5.11%, respectively.

We attribute such limited efficacy to the inherent optimizations on the corresponding heuristic. As reported in the solver specification [4], the optimized and simplified vivification is one of the most significant update appeared in the baseline solver. This suggests that human expertise has largely saturated vivification’s optimization potential, while dynamic tuning it may gain diminish for highly engineered tactics. To further prove our hypothesis, we integrate DynamicSAT into the kissat solver without meticulous optimization on vivification, using the version sc2022-bulky [11] submitted to SAT Competition 2022 (denoted as kissat-sc22). The intergated variant is named as DSAT-vivify-sc22. The following experiments are conducted on the 2024 SAT Competition Benchmark under the same environment and hyperparameters as described earlier.

Table 5 summarizes the results. On the one hand, the variant with DynamicSAT DSAT-vivify-sc22 achieves a 16.68% solving time reduction for solvable instances and a 5.64% reduction in Par2 score across the entire benchmark compared to Kissat-sc22, which highlights the effectiveness of DynamicSAT. On the other hand, the upgrade from Kissat-sc22 to Kissat-sc24 achieves a 2.04% increase in #Solved and a 6.42% reduction in Par2 score. Although DSAT-vivify-sc22, which simply combines DynamicSAT into Kissat-sc22, does not significantly improve #Solved, it achieves a 5.64% Par2 reduction, which is comparable to the improvement seen in Kissat-sc24. Our experimental results underscore the complementary roles of human expertise and automated adaptation in solver design, demonstrating that DynamicSAT can significantly enhance performance even without meticulous heuristic-specific optimization.

We present a breakdown analysis of instance families alongside the corresponding solver variants. Detailed results are provided in Table 8 in the Appendix A.4. Below, we discuss the performance trends observed for representative tuning heuristics.

First, DSAT-backbone and DSAT-transitive are the variants that support dynamic tuning of binary clause–related heuristics. The former focuses on analyzing binary clause backbones, while the latter applies transitive reduction to binary clauses. In families with a high density of binary clauses, such as Hamiltonian, Maxsat, and Miter, these heuristics yield substantial improvements. For instance, in the Hamiltonian family, the baseline solver achieves an average Par2 score of 404.76. DSAT-backbone reduces this score to 243.36 (a 39.88% improvement), and DSAT-transitive further lowers it to 198.25 (a 51.02% improvement). In contrast, DSAT-chrono only achieves an 8.93% Par2 reduction on Hamiltonian instances, and DSAT-eliminate even increases the Par2 score by 70.96%.

Second, for Cryptography instances, the baseline Par2 score is 1,310.32, and most tuning approaches yield marginal or negative improvements – for example, DSAT-chrono worsens performance by 57.13% and DSAT-rephase increases the Par2 score by 9.50%. Surprisingly, DSAT-backbone reduces the Par2 score by 68.39% on this instance family. Although cryptography instances do not present an abundance of explicit binary clauses, many variable relationships can be modeled as equality or inequality conditions that reflect the XOR structure. During the clause learning process, the solver adds numerous binary clauses representing these conditions. By dynamically tuning the backbone heuristic, the solver efficiently identifies and exploits these critical binary relationships, which leads to significant performance gains. This result highlights the adaptive capability of DynamicSAT to tailor tuning strategies to the dynamic properties of the instance family.

Third, our further experiments with a separated analysis across instance families align with the results in Section 4.4, where the variant DSAT-vivify does not significantly outperform the baseline. While DSAT-vivify reduces the Par2 score across most instance families, it struggles with solving Random Circuit, Miter, and Hamiltonian instances. Specifically, it even increases Par2 score on Random Circuit problems by 133.37%.

As a result, most DynamicSAT variants achieve remarkable performance on a broad range of problems. Moreover, our results clearly expose the specific instance families where DynamicSAT variants are less effective. In future work, we aim to refine our heuristics and further adapt the DynamicSAT framework to better address the limitations identified in these challenging instance families.