We explain in detail how we reimplemented vivification in our award winning solvers and then, focusing on Kissat, report on experiments on an interesting scalable factoring benchmark suite which helped us to find and remove a subtle performance regression in the vivification code. While SAT solvers spend most of their time running the conflict-driven clause learning (CDCL) procedure [1], all winners of the SAT Competition since 2014 interleave this “search” procedure with other procedures globally transforming the formula, i.e., techniques collectively referred to as inprocessing [2]. They aim either to simplify the formula in ways that CDCL cannot or help it to run faster. There are diferent types of inprocessing techniques. Some like variable elimination [ 3] and variable addition [4] do not preserve models, but only equisatisfiability (requiring models to be fixed). Other techniques reduce duplicated information over variables, like equivalent literal substitution (ELS) [5]. Finally, many diferent techniques remove duplicated information within clauses, including subsumption or self-subsuming resolution. They are based on combining two clauses, either to show that one subsumes the other or to generate a shorter subsuming clause by resolving the two clauses. The focus of this work is one of the key inprocessing techniques, referred to as distillation [6], which also has been independently discovered and described as vivification [7]. We adopt the term “vivification” for this paper, in line with more recent literature [8, 9]. This technique generalizes self-subsuming resolution by utilizing multiple clauses to produce a shorter subsuming clause, rather than just resolving two. The process leverages the optimized unit propagation component of a SAT solver. In particular it is useful to simplify and remove learned “glue clauses” [10] which otherwise are kept indefinitely. The vivification algorithm must diferentiate among various scenarios involving the detection of subsumed clauses, their deletion, or their strengthening (aka. shrinking). We discuss how vivification has been implemented in our solvers, Kissat [11], since 2023, and in CaDiCaL (part of version 2.2-rc2) both with respect to how exactly clauses are “vivified” and vivification is scheduled. While working on a new scalable family of benchmarks factoring (Sec. 3), based on proving that no factorization of a prime number is possible, we observed an interesting performance regression in Kissat. After quite some debugging efort, we noticed that fewer clauses were deleted, which we then traced down to keeping more clauses during vivification. This lead to a solver slowdown accumulating over time, yielding much worse performance on these remarkable benchmarks.
In this paper, we discuss our new vivification algorithm implemented in both CaDiCaL and Kissat
and how it is scheduled. A major diference to our original vivification implementation in CaDiCaL [
Our experiments (Sec. 6) show that considerable run-time variation can be observed for diferent choices of removing or keeping a redundant clause during vivification. We also show that vivification candidates are frequently subsumed. Still, the most common case of successful vivification are shorter clauses as well as removing clauses due to finding an implied literal. Finally, we show that ticks-based scheduling and limiting vivification efort is efective across diferent benchmarks.
For background on SAT, we refer to the Handbook of Satisfiability [
Given a candidate clause the idea of vivification [
As in CDCL (actually as in DPLL already), if a conflict is found with the decisions ¬ℓ1, ¬ℓ2, . . . , ¬ℓ, we know that the clause := ℓ1 ∨ ℓ2 ∨ · · · ∨ ℓ is entailed by the formula. Therefore, it can be used to strengthen the candidate clause as follows: • if the clause is a strict subset of , then subsumes , so we can strengthen the candidate clause by simply replacing with the shorter clause (also called “shrinking” ); • similarly, if the negation of one literal of is propagated instead before being assigned as decision, we can remove it from , i.e., also strengthening the candidate clause; • otherwise, if a literal ℓ of is propagated positively, then ℓ is implied, we assume that the propagation power of is covered by others, it is redundant and can be removed.
Vivification had minor impact in 2007 and 2008, when it was originally described, but started to
shine in 2017 [
Vivification was subsequently implemented in various solvers including Glucose (in the version that
entered the 2018 SAT Competition as the first and currently only inprocessing technique implemented
in Glucose [
We created a new set of unsatisfiable benchmarks based on factoring prime numbers available at
https://github.com/m-fleury/sat-factoring-generator. For a fixed prime number (represented by a bit
vector of an appropriate bitwidth), we assert that there are two numbers (greater than one) whose
product generates said prime number (Alg. 1). We then simply use Bitwuzla [
Algorithm 1: Generating SMT Formula create-benchmarks (lower-bitwidth, upper-bitwidth, primes-per-bitwidth) for current-bitwidth from lower-bitwidth to higher-bitwidth low = (1 << current-bitwidth) // “<<” = bit-shifting high = (1 << (current-bitwidth + 1)) increment = (high - low) / primes-per-bitwidth for from 1 to primes-per-bitwidth lower-limit = (1 << current-bitwidth) + increment * ( - 1) upper-limit = (1 << current-bitwidth) + increment * prime = find-smallest-prime-between (lower-limit, upper-limit) if prime generate-factoring-smt (prime, current-bitwidth)
// (non-random) uniform distribution
To obtain a benchmark set scaling in size and dificulty to solve, we generate a fixed number of primes for each bitwidth (primes-per-bitwidth), uniformly distributed in the entire range which can be expressed by this number of bits, forcing the most-significant bit to true (Alg. 2). To our surprise (see Fig. 1), this actually created a remarkable family of unsatisfiable benchmarks scaling very nicely: the runtime increases slowly and predictably, and it is easy to produce more benchmarks by increasing the number of generated instances for each bitwidth, as well as harder benchmarks with larger bit-width.
We attempted to produce scalable satisfiable benchmarks too by taking as starting point the product
of two prime numbers (prime numbers that are close to each other). However, the generated problems
turned out to be too easy (even for large numbers). A related benchmark set of satisfiable instances was
evaluated in [
There are three major questions when implementing vivification: • How often to vivify? • Which clauses should be vivified? • In which order should the literals of a clause be assumed? We answer these questions on an abstract level and dive into some additional details below. The next Section 5 provides concrete pseudo-code with a more detailed discussion, high-lighting specific s d n o c e s n i e m it g n il v o s 0 1 5 implementation aspects. Ultimately the reader is invited to explore the actual implementation in Kissat or CaDiCaL (available for instance on GitHub1).
How often? How often vivification should be scheduled could be considered to be part of the “black art” of SAT solver design. In CaDiCaL and Kissat, probing (including vivification) is scheduled in increasing ( log ) conflict intervals. The duration of running one vivification round during probing inprocessing is limited by the number of “ticks” taken during propagation while vivifying in relation to the number of ticks consumed by CDCL search since the last time vivification was run. Ticks refer to an estimation of memory access and are used as a deterministic proxy to actual time. For instance visiting a clause during propagation counts as one tick. Ticks correlate well with running time, but still allow fully deterministic behavior of the solver. Limiting time spent in vivification is necessary, as unbounded vivification until completion is too costly on most instances.
Which clauses? Li et al. [
Li et al. [
Initially we vivified first tier-3, followed by tier-2, tier-1 and finally irredundant clauses. The argument was that vivification might remove redundant clauses and potentially promote shrunken clauses to a smaller tier, e.g., larger clauses from tier-2 could be shrunken to size 3 and thus become part of tier-1. It seemed natural to schedule them again immediately during the same vivification round.
However, in practice there are usually fewer tier-1 than tier-2 followed by tier-3 clauses and many more irredundant clauses. If vivification completes vivification of one tier with fewer clauses it is beneficial to use the remaining vivification ticks budget for the next tier with more clauses. Otherwise the ticks budget is wasted. As consequence of this argument, our latest version of vivification first vivifies tier-1, then tier-2, followed by tier-3 clauses, and finally irredundant clauses. 1https://github.com/arminbiere/kissat/blob/master/src/vivify.c and https://github.com/arminbiere/cadical/blob/rel-2.2.0-rc2/src/vivify.cpp What order? Finally, the question remains in which order the decisions should be picked, when vivifying a candidate clause. Instead of choosing a heuristic based on the best expected result, CaDiCaL and Kissat build an implicit prefix tree (or trie) of the clauses, which allows us to reuse decisions and propagations over diferent candidate clauses, i.e., we do not necessarily backtrack between vivification of two candidates. The order of decisions follows the prefix tree, maximizing reusability (throughput).
In fact, this simulates the trie-data-structure in distillation [
Further, sorting the candidate stack lexicographically (also with respect to literal occurrence – taking into account separately positive and negative occurrences of variables) would maximize reusability, however this can be too costly. Instead, we can only consider the first literal (or first two literals in CaDiCaL) in each clause for sorting the stack, which allows us to use the faster radix sort (faster compared to C++’s default stable std::stable_sort).
Our experiments show, that building a prefix tree saves roughly 30% of decisions (median for both the factoring benchmarks as well as the SAT Competition 2024 benchmarks is 33%). This also saves propagations and makes it possible to vivify many more clauses within the same ticks budget. Further discussion. A minor subtlety is that the propagation of vivification should ignore the candidate clause but should still update it to make sure that the watched literals invariants are valid. Otherwise, propagations might be missed for subsequent clauses. Similarly, if the candidate clause was propagating, the solver cannot reuse the last decision level (without loosing propagations). Not doing so does not lead to issues in the subsequent CDCL loops, because at the end of vivification, the solver backtracks to decision level zero, implicitly restoring watch invariants of the ignored clauses.
To reiterate on sorting candidate clauses, it is of course important that sorting is fast. Considering only one or two literals gives big speed-ups. However, one also looses certain potential advantages compared to sorting lexicographically as was done in CaDiCaL previously. Actually the Kissat version considered in the experiments uses a mixed strategy of lexicographic sorting for redundant clauses, i.e., tier-1, tier-2, and tier-3 clauses, and sorting irredundant clauses with respect to a single most occurring literal in a clause (the considered fixed number of literals is a compile-time parameter). Storing these one or two literals separately has another advantage: we keep the clauses watched without reordering it, leading to hopefully good watches and no very long watch lists which you would need if you put literals appearing the most often first.
It is important to use a stable sorting algorithm for determinism and debugging (which is substantially slower than default non-stable algorithms). When sorting with respect to the complete prefix tree, uniquely determining the position of each clause, it is possible to use a non-stable algorithm. The only issue in this regard is if the same clause occurs multiple times. This however can be detected cheaply and solved by removing one of them (vivifyflush option in CaDiCaL, activated by default).
It is also possible to detect subsumed clauses during candidate sorting: when comparing clauses with a shared prefix and one clause is identical to that shared prefix the longer clause is subsumed by the shorter. This technique requires sorting each individual clause first and updating watches accordingly. We did not see any performance improvements in CaDiCaL due to employing this subsumption technique.
Other solvers use diferent sorting scheme: For instance Glucose 4.2.1 [
Algorithm 3: Main vivification inprocessing algorithm scheduled from CDCL loop. vivify-tier (CNF , CNF , ticks-budget) // update subset of clauses in original CNF in place limit = ticksstats + ticks-budget // global variable “ticksstats” updated during propagation sort literals in clauses ∈ by number of occurrences (more occurrences first) let 1 be the sub-set of clauses of which were not tried during vivification last time let 2 = ∖1 // new clauses or clauses already tried last time sort 1 and separately 2 lexicographically w.r.t. literal occurrences (more first) // decision level set to zero at this point for all clauses in the sequence 1, 2 sorted as in line 5 as long ticksstats < limit if vivify-clause ( , ) then increment vivifiedstats backtrack to decision level zero if ticksstats > limit return 0 // incomplete – remember untried clauses return limit − ticksstats // return unused ticks budget – no untried clauses remembered
Algorithm 4: Vivifying one “tier” of clauses under a given ticks budget.
The revisited vivification algorithm vivify in Alg. 3 is called in Kissat from the probing inprocessing
procedure, after clausal congruence closure [
The ticks-budget computed at (line 1 in Alg. 3) is then split (line 2-4) into a fixed fraction for each of the tiers (according to run-time options). We hand over any remaining-ticks of the budget to the next tier, with vivification of irredundant clauses last (line 9), as it is usually the most costly tier to run vivification until completion (at least initially, for bigger formulas). The four calls to vivify-tier in Alg. 3 (line 6-9) consider only specific tier clauses as candidates to vivify as second argument. We formally also give a reference to the global formula as argument, to emphasize that Boolean constraint propagation (unit-resolution) is always performed on the whole formula (line 12 in Alg. 5).
The vivify-tier function is shown in Alg. 4. It first, as already discussed in the previous Sect. 4, determines a total ticks limit on propagation efort for all considered candidate clauses , based on the given budget (line 1). Then all candidates have their literals sorted by the number of occurrences (line 2) in order to subsequently (line 5) allow sorting the clauses lexicographically w.r.t. the literal occurrences. Before the candidates are split into two sets 1 and 2 (line 3-4) prioritizing left-over vivify-clause (CNF , clause ) // update and in place mark as having been tried // puts it in 2 next time let = ℓ1 ∨ · · · ∨ ℓ sorted by number of occurrences (more occurrences first) ifnd maximal such that ℓ is assigned to false at decision level for all < // reuse trail if > 0 and decision level larger than − 1 backtrack to decision level − 1 add − 1 to both probesstats and reusedstats // reused decisions / probes literal implied = ⊥, clause conflict = ⊥ // initialize both to be undefined denoted as “ ⊥” for = . . . as long conflict = ⊥ // and implied = ⊥ if ℓ is assigned to false continue if ℓ is assigned to true then implied = ℓ and break increase decision level and assign ℓ to false, increment probesstats // temporarily disable propagation over , i.e., is simply skipped during propagation conflict = propagate ( , ) // update global assignment and ticksstats // now we have either implied ̸= ⊥, conflict ̸= ⊥, or is falsified by the current assignment (subsuming, learned, irredundant) = vivify-analyze (, conflict, implied) if subsuming ̸= ⊥ remove from , increment subsumedstats and return true // . . . and need to make “subsuming” irredundant if it was redundant but not if |learned| < || // actually “learned ⊂ ” as it is a decision learned clause
replace in by learned, increment shrunkenstats and return true if implied ̸= ⊥ and redundant // regression version “without-implied” would only return false but the “default” version has: remove from , increment impliedstats and return true conflicting = conflict ̸= ⊥ ∨ implied ̸= ⊥ if conflicting and irredundant as well as analysis resolved only irredundant clauses remove from , increment asymmetricstats and return true if implied ̸= ⊥ and vivify-instantiate ( , , ℓ) // falsified at decision level
remove ℓ from , increment instantiatedstats and return true return false
candidates not tried last time vivification was run. This prioritization makes sure that all clauses of a tier are vivified in a round-robin fashion, i.e., clauses are tried at least once before being attempted to be vivified again. Note, that this scheme of vivification by tiers in combination with separate but fixed relative ticks budgets allows to complete vivification of tiers with fewer clauses earlier and more often.
Alg. 5 gives a high-level overview on our revisited clause vivification algorithm vivify-clause for vivifying a single candidate clause. It maintains a global assignment that is not reset between diferent candidates, i.e., subsequent calls to this function. Instead it reuses the trail as much as possible, in order to reduce the number of necessary propagations to vivify the candidate.
The propagation procedure called at line 12 ignores the candidate clause given as argument and further updates the global ticksstats statistics counter. It approximates non-local cache line access, similar to Knuth’s “mems” statistics (counting the number of pointer dereferences instead). Counting ticks is only an approximation and the result of profiling runs and inspecting the code, i.e., the programmer adds instructions which increase the ticks counter whenever the program reaches a point, where a non-local memory access is expected. Access to the same cache line (e.g., propagating many virtual binary clauses for the same literal) is counted only once. Even though less automatic to implement, ticks are more precise than mems, i.e., correlate better with actual running time.
The function vivify-analyze (line 13) is a standard conflict analysis routine, similar to “analyze-final” in MiniSat. It returns a decision-only learned clause, which is a subset of the negations of decisions, that lead to the given conflict, derive the implied literal or (if both are undefined) to falsify the given candidate clause. It further checks on-the-fly whether any of the resolved clauses subsumes the candidate clause. In this case it aborts the analysis and returns the subsuming clause. Otherwise it returns the learned clause and determines whether all resolved clauses in deriving the learned clause are irredundant.
The function vivify-instantiate (line 24) originates from a CaDiCaL hack CaDiCaL _vivinst [
What is missing in the high-level description of Alg. 5 is when (if at all) and to which level to backtrack to after shrinking a clause and successful instantiation. If the procedure fails but a conflict was deduced we might need additional backtracking too, as well as explicitly reestablish clause-watching invariants for the candidate clause (as it was skipped during propagation). Further note, that sorting literals within clauses during scheduling in vivify-tier (line 2 in Alg. 4) as well as during candidate clause vivification in vivify-clause (line 2 in Alg. 5) should be done on copies of the clauses in separate data-structures to keep watch-invariants intact (or as alternatives either reestablish them before propagation or use an approximate short list of literals only – cf. Sect. 4).
The procedure has 5 positive cases in which a candidate clause is vivifiedstats (line 7 in Alg. 4) and thus the candidate clause is shrunken (replaced by a strict subset of literals) or removed. These correspond to incrementing in Alg. 5 the statistics counters subsumedstats (line 15), shrunkenstats (line 17), impliedstats (line 20), asymmetricstats (line 23) and instantiatedstats (line 25) with returning true. Otherwise the procedure fails returning false (line 26) and keeps the candidate as is. The next section evaluates how often these cases occur in practice (cf. Fig. 6 and 7).
We ran Kissat version sc2024 as submitted to the SAT Competition 2024 on all 400 problems of the SAT Competitions 2023 and 2024 and our 750 factoring benchmarks using the bwForCluster Helix with AMD Milan EPYC 7513 CPUs and a time limit of 5000 seconds. More precisely we used four configurations of Kissat: the default configuration, matching the description in Fig. 5 (including removing implied literal candidates - keeping line 18-20 in Alg. 5 as is); versus the keep-implied configuration which keeps implied clauses (returning false at line-20 in Alg. 5 without removing the candidate); the discard-both configuration (replacing the condition “ implied ̸= ⊥” with “implied ̸= ⊥ ∨ conflict ̸= ⊥” at line-18 in Alg. 5 which, if triggered, not only removes clauses with an implied literal but also conflicting candidate clauses); finally the no-vivify configuration which disables vivification completely.
On the 400 problems of the SAT Competitions 2023 and 2024 (Figures 2 and 3), the performance does not difer much, but the default version performs best. Interestingly, it seems that completely deactivating vivification does not make much of a diference on these instances anyhow. However, on our factoring benchmarks the diference between the configurations is important (Fig. 4). For these benchmarks, the discard-both configuration performs slightly better than the default configuration.
In an intermediate version of Kissat we accidentally introduced the keep-implied variant, probably, as it might appear that implied literal candidates should be treated the same way as conflicting candidates. Note, that the diference only becomes relevant if a redundant clause candidate is not subsumed nor shrunken during vivification (we reach line 18 in Alg. 3 and a literal is implied or we found a conflict). These factoring benchmarks however revealed, that these two cases should be diferentiated.
On competition benchmarks keeping conflicting but discarding implied literal candidates works best (default), while for the factoring benchmarks, discarding implied literal candidates is a must (default vs. keep-implied even though discard-both is even better). After we observed this regression empirically, ifnding the root cause was rather dificult. Only after realizing that the regression version would keep for long running benchmarks many more learned clauses, it became clear that we should search for code where clauses are removed in one version and kept in the other. Furthermore, it was the first time we observed such an almost linear line in a run-time scatter-plot of SAT solvers (cf. Fig. 5, right plot).
To give more insight into the impact of vivification and how often specific cases of Alg. 5 occur we have extracted statistics for the default configuration. Figure 6 shows the ratio and amount of time the solver spends in vivification with respect to search and overall time on the factoring benchmarks. These quantities scale very nicely on this benchmark set, as is evidenced by the fact that we can sort by just one criterion, always plotting the same benchmark in one cross-section. Looking at the vivification statistics (cf. end of Sect. 5), the percentages between the diferent cases are almost constant, only asymmetricstats seems to tail of for the harder instances. The impliedstats clauses make out almost 40% of all positive vivified clauses, explaining the regression we can observe in the previous plots. These statistics on the SAT Competition 2024 benchmarks vary more but similar trends can be observed (Fig. 8, 9). A diference overall seems to be the number of subsumed clausesstats, which is similar to shrunkenstats and impliedstats on these instances, compared to about half for the factoring benchmarks.
We gave a deep dive into technical details of the implementation of our latest version of vivification in our SAT solvers Kissat and CaDiCaL. Beside explaining the novel feature of on-the-fly subsumption we further reported on an interesting performance regression we observed due to a subtle diference of two versions of vivification, difering only in the choice of removing a vivification candidate with an implied literal or not. Keeping them lead to a regression. It was detected on a new set of factoring benchmark which by itself is quite remarkable as it yields very smooth run-time scaling behavior. Our experiments reveal that all the considered special cases during vivification do occur in practice, but most frequently, successfully vivified clauses are either shrunken, subsumed or have an implied literal, while successful instantiation or asymmetric literal elimination in irredundant clauses occurs rarely. 0 0 3 400 instances (100%) 297 instances (74%) s d n o c e s 0 0 0 5 f o it m li 297 default 291 discard−both 290 keep−implied 288 no−vivify 325 instances (81%) 0 1000 2000 3000 4000 5000 0 2 3 0 0 3 0 8 2 0 6 2 0 5 7 0 0 7 0 5 6 0 0 6
0 1000 2000 3000 4000 5000 Figure 4: Performance of various Kissat configuration on our new 750 factoring benchmarks described in Sect. 3. Again axis follow the common practice how results of the SAT competition are presented (as in Fig. 2+3 too).
This work was supported in part by the state of Baden-Württemberg through bwHPC, the German Research Foundation (DFG) through grant INST 35/1597-1 FUGG, and by a gift from Intel Corporation.
The authors partially used Mistral AI with a "fix typos" prompt for grammar and spell-checking. After using that tool, the authors reviewed and edited content as needed and take full responsibility for the publication’s content. 325 default 324 discard−both 320 no−vivify 319 keep−implied 750 discard−both 750 default 750 keep−implied 712 no−vivify satisfiable unsatisfiable unsatisfiable linear regression ) s d n o c e s n i e m it( lt u a f e d 0 0 0 5 0 0 0 4 0 0 0 3 0 0 0 2 0 0 0 5 0 8 0 6 0 4 0 2 0 0 0 1 0 8 0 6 0 4 0 2 0 100 150 200 250 300 0 0 1 0 8 0 6 0 4 0 2 0 0 4 0 2 0 0