Learn to Unlearn

Modern SAT solvers following the conflict-driven clause learning (CDCL) paradigm [21] or related algorithms [28], reduce the search space by learning clauses that boost propagation power. Thanks to solver efficiency and hardware advances, they can now learn many more clauses and solve much larger instances. However, these clauses (also called “no-goods” [28]) gradually slow down the solver because the efficiency of most algorithms depends on the size of their data structures. Furthermore, retaining every clause turns CDCL into an algorithm requiring exponential space, similar to reverting from DPLL [6] to DP [7]. Thus, reducing the number of clauses by unlearning is crucial for good performance. In this paper, we revisit established clause unlearning strategies and evaluate their impact on our state-of-the-art SAT solver Kissat [4], winner of all tracks of the SAT Competition 2024.

Several research efforts have tried to mitigate this problem. Already in 1993, in parallel to the seminal work on CDCL [24], Ginsberg [12] presented a polynomial space variant of conflict-driven no-good learning, which he later adapted in 2015 to allow arbitrary restarts [13] without losing completeness. However, state-of-the-art solvers have not adopted this approach.

On the practical side, various unlearning schemes have been proposed: keeping clauses up to a fixed size [8], using relevance-based criteria [20], combining different approaches [24, 14, 18] and more. In our experiments, we revisit size-based unlearning in particular. More recently, CDCL solvers have started to predict the future usefulness of a clause by measuring either how often it is used (its activity) [9, 14] or how recently it has been used (its age) [15, 11, 14] during conflict analysis. This information is then used to rank clauses for retention or deletion. The seminal Glucose [1] introduced the new ranking scheme literal block distance (LBD) and, more importantly, the idea of keeping specific (glue) clauses unconditionally.

We highlight the importance of clause unlearning in our first experiment (Section 3), where we evaluate Kissat without any unlearning (a configuration previously studied by Chanseok Oh [23]) as well as periodically unlearning all learned clauses. The experiment shows that keeping all clauses degrades performance on all instance types. Interestingly, while periodic unlearning of all clauses yields nearly state-of-the-art performance on satisfiable instances, it significantly harms performance on unsatisfiable ones.

Our second experiment (Section 4) revisits the favored approach of MiniSat [9], where clause activity is used to decide which clauses to unlearn. In this scheme, a clause’s activity increases each time it is used to derive a new clause, while unused clauses are penalized. In our experiments, the performance of Kissat with activity-based unlearning is unsatisfactory.

In 2009, Glucose [1] introduced a new usefulness criterion based on the propagation power of clauses, approximated by LBD (the number of different decision levels in a clause when it is learned or propagates). While MiniSat ranks clauses based on activity and unlearns a fixed percentage, Glucose sorts clauses into two tiers and unconditionally keeps the lower-tier (critical) clauses. Our experiments in Section 5 confirm that retaining only critical clauses is more important than the difference between using clause size or LBD as the ranking metric. Similar findings regarding the indifference between ranking schemes have also been observed in a related experiment [10] focusing on combinatorial benchmarks.

In 2019, a machine-learning-based approach was used to analyze clause usefulness, which we revisit in Section 6. In that work, the usefulness of a clause was estimated by generating proofs, reconstructing dependencies, and classifying core clauses as useful. Soos et al. [27] identified, that clauses which have been used to derive a new clause since the last unlearning round should be kept. This effectively reduces clause activity to a single binary indicator. While this metric alone performs poorly, combining it with other criteria consistently improves solver performance. In fact, such a combination is one of our best configurations and achieves performance similar to the base version of Kissat while being much easier to implement.

Finally, in Section 7, we discuss the state-of-the-art and Kissat. Since Kissat uses LBD as a key metric for estimating a clause’s usefulness, we analyze the actual distribution of LBDs in used clauses. While the distribution usually shows peaks that match our definition of critical clauses, some instances have a minimal LBD far above our critical threshold. We address this by proposing a new dynamic tier system with adaptive thresholds to identify critical clauses, though this scheme does not improve performance.

We refer the reader to the corresponding chapter of the Handbook of satisfiability [21] for an introduction to conflict-driven clause learning (CDCL), i.e., CDCL applies unit propagation after decisions, finds conflicts and then learns new clauses to change the focus of the search, interleaved with restarts, inprocessing [19], as well as unlearning, the focus of this paper.

In Alg. 1 we show pseudo-code for the implementation of unlearn, which is called periodically from the CDCL loop according to some unlearning schedule. Clauses are only removed during unlearning, so even unlearn-all keeps clauses for some time: it only throws away all learned clauses in each unlearning round. In this paper, we vary different parts of this Alg. 1. Changes and their effects are outlined in the respective sections below.

As initial starting point of our investigations we used the competition version of the award-winning SAT solver Kissat [4] from the SAT Competition 2024. It won all main-tracks of this most recent competition and thus is considered the state-of-the-art. In order to reduce influence on and by other heuristics while varying aspects of unlearning, we have simplified the competition version in two ways. First, we let Kissat restart before unlearning clauses, as otherwise, the solver is forced to keep clauses which are used as reasons for assigned variables. Second, we fix the fraction of removed clauses to be the same for the entire run of the solver, specifically 75%. In the competition version it slowly increases from 60% to 90%. The resulting base version is the actual starting point for the other variants considered.

Throughout this paper, all experiments are conducted with the 400 problems from the SAT Competition 2024, following The SAT Practitioner’s Manifesto [5] and solved on the bwForCluster Helix with AMD Milan EPYC 7513 CPUs, a memory limit of $16\mathrm{GB}$ per solver run and a time limit of $5000\mathrm{s}$. We consistently present results as cumulative distribution functions (CDFs), where the $x$-axis gives the time and the $y$-axis shows the number of solved problems (400 total for the entire benchmark set or 200 total when only UNSAT or SAT).

We first evaluate the configurations unlearn-all and no-unlearn which periodically unlearn all and never unlearn any clauses, respectively. We observe an interesting effect: unlearning all clauses is only very modestly harmful on satisfiable instances (Fig. 2(b)). It appears sufficient to guess a model to solve those instances and learned clauses only seem to be instrumental to locally guide the solver towards this model, and should be unlearned fast. However, unlearn-all is detrimental to solving unsatisfiable instances (Fig. 2(a)).

Keeping all clauses (no-unlearn) reduces Kissat’s performance for both classes, but is not as harmful on unsatisfiable instances as expected. It further has a negative impact on memory usage of course as for no-unlearn accumulated memory usage goes from $167\mathrm{GB}$ to $240\mathrm{GB}$. On the other hand, the number of conflicts on the 96 shared solved unsatisfiable instances of the no-unlearn configuration is reduced to 0.7 the number of conflicts in the base configuration and goes up for unlearn-all by more than factor of 10. Chanseok Oh [23] reached similar conclusions for unlearn-all.

In general, we obverse that configurations retaining more clauses perform better on unsatisfiable instances and worse on satisfiable instances, while unlearning more clauses tends to improve performance on satisfiable instances but hinders solving unsatisfiable instances. This might be exploited if the expected result for a particular instance is known.

The solver MiniSat [9] implements a common strategy for clause retention: A clause’s activity – reflecting how often it contributes to conflict analysis – determines its usefulness. Each time a clause participates in deriving a learned clause, its activity increases; new clauses get the current global clause activity increment. The global clause activity increments grows exponentially with each conflict (penalizing unused clauses), and when values become too large, scores are rescaled. This is akin to the (E)VSIDS heuristic [22, 9] for variables. Although alternative metrics like propagation counts have been explored, activity-based heuristics perform best. This aligns with Simon’s observation [25] that roughly 90% of propagations are unused, indicating resolved clauses in conflict analysis drive the search.

We implemented an activity branch on top of the base branch (one of 42 for this study [16]) to test how well activity predicts clause usefulness in Kissat. It keeps the aggressive scheduling used in all experiments but modifies the unlearn function (see Alg. 1): the target fraction is set to 50% as in MiniSat, but the used flag and critical metrics are ignored.

Figure 3 shows that activity-based unlearning performs worse than our baseline. On satisfiable instances (Fig. 2(b)) its performance mirrors unlearn-all, on unsatisfiable instances (Fig. 2(a)) it resembles no-unlearn. Since satisfiable instances gain little from learned clauses, activity-based unlearning gives mixed results and is a weak predictor by modern standards.

In 2009, Audemard and Simon [1] introduced two key modifications to MiniSat, resulting in Glucose. These include the LBD score and a policy of always retaining high-quality (LBD $\le$ 2) clauses – termed glue clauses by the authors, but called critical here to avoid confusion. These changes enabled more aggressive restarts and unlearning by keeping fewer clauses. This yields a 2-tier system: top-ranked clauses (tier 1) are always retained; others (tier 2) are ranked and selectively unlearned.

The term “LBD” has two definitions. In [1], it counts the number of decision levels in a learned clause before backjumping. Later work [3, 2] updates LBD upon propagation, based on levels after backjumping (one less than the original). To reconcile this, Glucose adds 1 to updated scores, while Kissat adopts the propagating definition, calling it “glue” in code.

We evaluate LBD and critical clause ideas independently (Fig. 4). One set of experiments compares different critical thresholds (Alg. 1, line 7) across target fractions using rank (line 10); another uses clause size instead. Although the average size/LBD ranged from $2.05$ to $2.15$, we expected glue <= 5 to behave like size <= 10 – but it did not.

Still, surprisingly, LBD and size are nearly interchangeable. Retaining clauses up to size 10 yields the best results, while rank configurations trail the best critical ones. This suggests that setting an appropriate critical threshold suffices to identify valuable clauses, whereas rank tends to retain more unhelpful ones, hurting performance.

We also evaluated combinations of critical and rank (Fig. 5) by enabling both lines 7 and line 10 in Alg. 1. Since critical clauses are always retained, we reverted to the default unlearn target of $f=75\%$. This significantly improved performance for lower thresholds, such as lbd <= 2, lbd <= 3 or size <= 6, with smaller gains for the higher size <= 10 threshold.

In 2019, Soos et al. [27] and, more recently, Yang et al. [29] applied machine learning techniques to identify effective criteria for clause usefulness. Their approach involved running the solver without performing any clause unlearning while logging detailed statistical data for each learned clause. Subsequently, a proof checker trimmed the proof and extracted resolution chains using a heuristic that favored reusing existing clauses over introducing new ones during derivation. Their analysis confirms that the LBD is an important predictor of a clause’s usefulness – with LBD slightly outperforming clause size – and demonstrated that a clause’s recent use in deriving a conflict is a strong estimator of its future utility.

Various solvers, including CaDiCaL, implement a used flag for clauses, set during conflict analysis and reset during unlearning (cf. Alg. 1). In essence, the used flag reduces clause activity to a single bit recording whether the clause was used since the last unlearning. It is very similar to the second chance algorithm or clock algorithm [26] used in page replacement policies, as it gives the clause a second chance to be useful before unlearning.

We combine this used flag with each of the configurations from the previous sections and compare the difference in the solved instances when retaining all used clauses (+ used) versus the configuration without used flag (Tab. 6). Subsequently, we refer to these configurations as “<configuration>+used”. Keeping only used clauses performs slightly better than activity-based unlearning, showing that it is indeed a useful abstraction (Fig. 9). However, it still performs worse than the baseline. The full potential of the used flag is only realized in conjunction with other unlearning methods: it consistently improves each configuration’s performance. Hence, used clauses are important, but less so than critical clauses.

The used flag inspired us to give clauses one more chance, namely a third chance. When clauses are used, we set used to 2 and decrement it during unlearning. We consider the clause for deletion only when we reach zero. This in essence simulates a three-tier system [23], but in our experiments does not yield any improvements (see Fig. 9 in the appendix).

Another interesting question is how to update the used flag during inprocessing. We recommend not updating the used flag during forward subsumption, as doing so resulted in significant performance degradation in CaDiCaL. Specifically, in version 1.9.4 we altered the policy for updating the used flag on successfully strengthened learned clauses – changing it from granting a second chance to providing a third chance. This modification led to a severe performance regression in incremental solving, and was reverted in CaDiCaL 1.9.5.

In order to link LBD to usefulness, we further recorded the LBD of all clauses used during conflict analysis on all benchmarks from the SAT Competition 2024. Note that Kissat runs a portfolio of two modes; focused mode (many restarts, shallow exploration of the search space), and stable mode (few restarts, and deep exploration of the search space with long assignments). Chanseok Oh [23] calls these modes “UNSAT” and “SAT” modes. Due to these different search characteristics, we recorded LBD statistics for both modes separately.

We show 4 representative instances from the SAT Competition 2024 in Fig. 7. The most common LBD distribution shows a sharp peak at very low LBD values, followed by a steep decline. However, some problem families exhibit a broader distribution, or the peak is shifted to much higher LBD values. In certain cases, there are no used clauses with low LBDs at all. As a result, no critical clauses would be retained unconditionally. In such situations, unconditionally keeping used clauses (and ranking) helps to compensate for this issue.

The skewed LBD distributions motivated us to replace the static tier limit for identifying critical clauses with a dynamic approach based on either LBD or size. Specifically, we set the threshold so that 50% of all clauses used since the beginning fall below this limit.

We also observed some instances where most learned clauses have an LBD of 1. In such cases, using a tier threshold of LBD 2 – typically seen as very good – would actually be problematic, as it would prevent those clauses from ever being unlearned.

The dynamic unlearning scheme (Fig. 8) does not achieve the same performance as the static schemes, suggesting that the usefulness of critical clauses comes from the absolute size or LBD, and not the comparatively low size or LBD. The performance of dynamic configurations is similar to the non-dynamic configurations on satisfiable instances but notably worse on unsatisfiable instances. This, surprisingly, indicates that the in the dynamic configurations too few useful clauses are kept.

The used flag of the previous experiment also improves dynamic configurations. Further, size and LBD in combination with dynamic tier limit computation perform similarly. Nonetheless, the dynamic configurations together with the used flag still perform worse. While we see as usual that the used flag improves the performance and that size is similar to LBD, the resulting configuration is still worse than the version where we keep all clauses of size 10. We have observed during earlier runs on SAT Competition 2023 bencharks that there were more outliers for the glue distributions compared to SAT Competition 2024 benchmarks. We leave the investigation of this observation as future work.

We investigated which unlearning schemes are useful for the state-of-the-art SAT solver Kissat on SAT Competition 2024 instances. Our results show that, overall, activity performs the worst. Furthermore, while the difference between LBD and size based ranking is limited, it is important to keep either low LBD or low size clauses unconditionally, as well as used clauses, which consistently gives a boost for all our considered unlearning strategies. A vaild configuration which could replace the current strategy in Kissat could therefore be critical@size <= 6 + rank@size = 75% + used. Probably the most striking result is that frequently unlearning all clauses completely is in essence not harmful for solving satisfiable instances.

As future work it would be interesting to understand whether these findings can be extended to other SAT solvers and persist on other benchmark sets, as the diversity of solved instances for the strategies is perhaps limited by the benchmark set (the virtual best solves 351 instances, only 22 more than the single best strategy).