Quantified formulas pose a significant challenge for Satisfiability Modulo Theories (SMT) solvers due to their inherent undecidability. Existing instantiation techniques, such as e-matching, syntax-guided, model-based, conflict-based, and enumerative methods, often complement each other. This paper introduces a novel instantiation approach that dynamically learns from these techniques during solving. By treating observed instantiations as samples from a latent language, we use probabilistic context-free grammars to generate new, similar terms. Our method not only mimics successful past instantiations but also explores diversity by optionally inverting learned term probabilities, aiming to balance exploitation and exploration in quantifier reasoning.
The idea of probabilistic grammars can be simplified even further. Let’s say that the constant appears frequently under the function symbol , then () should also be a likely term in our language. Probgen 5: 6: 7: 8: 9: 10: 11: Algorithm 1 Make Term Input: - range type, - term depth, initially 0 Output: term of type Using: Symbols( ) - symbols constructing terms of type
Depth - maximum allowed term depth Pick() - pick one symbol out of according to the selection method
Arity() - the arity of symbols 1: function MakeTerm(, = 0) 2: ← Symbols( ) 3: if ≥ Depth then 4: ← { ∈ | is a constant} ← Pick() if is a constant then return
← return (1, . . . , ) else for all 0 < ≤ Arity() do
MakeTerm( , + 1) where is the type of the -th argument of However, this suggests a diferent question. If the new terms are generated according to the ones that were already used in the past, will they be useful? Should we not rather do the opposite, i.e., generate diferent terms ? Efectively, this means inverting the probabilities when generating new terms for instantiation.
Basic understanding of SMT [
Probabilistic grammars [
Full-fledged learning of PCFG is likely to be to expensive for our purposes and we take a Markov-like approach instead. New ground terms are generated recursively, as a tree, and the probability of a symbol being generated in a node is determined by the frequency of in the instantiations so far.
Terms are generated recursively in a straightforward fashion with fixed maximum depth using function MakeTerm in Algorithm 1. The function MakeTerm( ) generates a term of type by selecting a term head symbols and recursively generating argument terms, possibly resorting to constants to limit the depth of generated terms. The head symbol is always picked from the set Symbols( ) which contains all symbols of type encountered in the terms generated by other instantiation modules. The maximum allowed term depth is controlled by parameter Depth. With Depth = 0, the algorithm generates constants only.
The key point of the algorithm is the selection of the term head symbol using the function Pick. Naturally, there is a lot of flexibility in this choice, and that is where our statistical approach comes into play. We implement three diferent selection methods. The first one, denoted random, selects a symbol uniformly at random, independent of any symbol statistics. The next method, weights, maintains a statistic for each symbol , counting the number of times occurs in terms generated by other instantiation techniques. These counts are interpreted as probabilistic weights, and the head symbol is then sampled from a categorical distribution derived from them. In practice, this means treating the weights as proportional intervals on a number line, generating a random number in the range from 0 to the total weight sum, and selecting the symbol corresponding to the interval in which the number falls. The third and final selection method we experiment with is paths, which extends weights by taking term positions into account. It maintains separate weight vectors for each term position, where a position is determined by the list of symbols occurring above the term in the syntax tree. For example, the position of both and in ((, )) is given by the path (, ). Since the weight vectors for paths can be quite sparse and contain only few symbols of the given type, we additionally consider all other compatible symbols with the default weight 1 at each position.
The above symbol selection methods weights and paths generates terms mimicking terms generated by other instantiation modules. In order to introduce diversity and generate diferent terms, we introduce additional parameter Flip. Its value is the probability under which the weights should be inverted, setting all weights to 1/ instead of . This probability is applied in every call to function Pick. Hence diferent calls to Pick within one call to MakeTerm can work with diferent weights.
The final parameter we introduce to our probabilistic instantiation module concerns when the module is activated. In cvc5, several efort levels are defined for instantiation modules. These modules are tried sequentially, with the efort level increasing if no lemma is produced at the current level. The currently implemented efort levels in cvc5, in order of increasing efort, are conflict , standard, model, and last call. Conflict-based instantiation modules are tried first ( conflict ), followed by heuristic instantiation modules (standard, e.g., e-matching), then model-based techniques (model), and finally full efort instantiation (last call) are launched.
We follow the behavior of the enumerative instantiation modules and introduce a parameter Effort, which supports two values: lastcall and interleave. With lastcall, our probabilistic instantiation module is executed only at the last call efort level, that is, when no module has produced a lemma at a lower efort. With interleave, instantiations are performed already at the standard efort level, meaning the module runs more frequently than with lastcall.
We evaluate1 our approach on a benchmark from SMT-LIB [
Effort
Pick Depth
Flip ∈ {lastcall, interleave} ∈ {random, weights, paths} ∈ {0, 1, 2, 3, 4} ∈ {0.0, 0.2, 0.5, 0.8, 1.0} 1On a server with two AMD EPYC 7513 32-Core processors @ 3680 MHz and with 514 GB RAM. Effort lastcall interleave Pick random weights paths random weights paths Depth total ref (+/-) total ref (+/-) total ref (+/-) total ref (+/-) total ref (+/-) total ref (+/-) 0 3523 +499/-53 3497 +477/-57 3445 +427/-59 3575 +571/-73 3570 +571/-78 3498 +497/-76 1 3293 +270/-54 3245 +230/-62 3273 +247/-51 3309 +321/-89 3284 +300/-93 3327 +349/-99 2 3221 +195/-51 3231 +215/-61 3220 +190/-47 3242 +259/-94 3239 +256/-94 3211 +235/-101 3 3220 +193/-50 3192 +182/-67 3219 +188/-46 3276 +290/-91 3171 +211/-117 3230 +256/-103 4 3212 +197/-62 3181 +169/-65 3215 +184/-46 3236 +258/-99 3161 +206/-122 3228 +255/-104 Since the parameter Flip is applicable only when Pick is either weights or paths, we obtain altogether 110 diferent strategies. We evaluate all of them with a 10 second time limit per strategy and problem. Our probabilistic instantiation module is launched together with the default cvc5 setting which uses e-matching and conflict-based quantifier instantiation (cbqi). The instantiation terms introduced by these two default modules are intercepted and used to collect symbol statistics utilized by our weights and paths symbol selection functions. The set of asserted quantifiers is randomly shufled in each round. This is because we terminate the instantiation round after a first successfully generated lemma.
We always generate 20 terms for each encountered type and remove duplicates if necessary. Within one instantiation round, only one set of terms is generated for every encountered type, that is, for every type of a ∀-bound variable from asserted quantifiers. This gives us a non-zero probability that variables of the same type will be instantiated by the same term. A new set of terms is generated in the next instantiation round.
The results for diferent values of Depth with Flip fixed to 0.0 are depicted in Figure 2. This allows us to evaluate the efect of various term depths. For each strategy we present three numbers: (1) the total number of solved problems (column total), and (2-3) the number of solutions gained (+) and lost (− ) on the baseline reference strategy (columns ref ). As the baseline strategy we consider cvc5 with the default option setting. The reference strategy solves 3,077 problems. To ease orientation, the best value in each column is highlighted and the best values within the table are additionally underlined. We can draw several observations from Figure 2: 1. All strategies significantly outperform the reference strategy, which solves 3,077 problems. 2. In every case, increasing the maximum term depth leads to a decline in performance. The best results are achieved when instantiating with constants only (Depth = 0), likely due to the reduced complexity of the term space at lower depths. 3. Strategies using the interleave efort, where our instantiation module is invoked more frequently, tend to perform better than those using lastcall. This suggests that there is a potential advantage in our approach. 4. Each strategy both solves some problems that the reference does not (ref+) and fails on some that the reference does solve (ref-). The lastcall strategies lose fewer solutions because the probabilistic instantiation is applied less frequently, resulting in behavior closer to the reference. The fewest losses occur with the paths variants at higher term depths, where the generated terms more closely resemble those of the reference strategy. 5. There appears to be no significant advantage of probabilistic generation over random term generation in this case. Since the depth is fixed to 0, the paths variant does not fully benefit from using diferent weight vectors for diferent positions. Moreover, the weights variant instantiates using all constants from the other instantiation modules, guided by probabilities based on their occurrence counts. In contrast, paths in this case only tracks statistics for constants that appear at the top level while all other constants are assigned a default weight of 1.
In the next Figure 3 we fix Depth to 0 and we evaluate various values for Flip. Higher values force our module to generate terms more diferent than term used by default instantiation modules. The table Effort interleave standard standard standard interleave standard interleave standard interleave interleave interleave standard interleave interleave standard standard standard standard standard interleave strategy parameters
Depth Pick 0 weights 0 weights 0 weights 0 random 0 paths 0 paths 0 weights 0 weights 0 weights 0 random 0 paths 3 random 0 weights 0 weights 0 paths 0 weights 1 paths 0 paths 1 random 0 paths Effort Pick format is the same as in Figure 2 with the exception that the random case is omitted since the Flip parameter does not efect it. The line for Flip = 0 has the same values as in the line Depth = 0 in the previous figure.
The best results are obtained with the weights variant using the interleave efort and Flip = 0.5. This strategy solves 3,613 problems and produces 612 new solutions compared to the baseline. Overall, we observe that better performance is achieved when Flip is strictly greater than 0.0, suggesting that occasionally generating complementary terms is beneficial. By tuning the Flip parameter, we outperform the random term generation results shown in Figure 2.
The final experiment in this work aims to evaluate the mutual complementarity of the tested strategies. A greedy cover sequence is constructed from all evaluated strategies. The sequence is initialized by selecting the most efective individual strategy, and the problems it solves are marked. At each subsequent step, the strategy that solves the largest number of remaining unsolved problems is selected. This process is repeated iteratively. In this way, the greedy cover reveals strategies that complement one another.
The first 20 strategies in the greedy cover are presented in Figure 4. The first four columns specify the strategy parameters, while the next four columns summarize their performance within the greedy cover. The column solves shows the number of problems each strategy solves individually. The remaining columns reflect each strategy’s contribution to the overall portfolio performance. The column +new indicates how many additional problems the strategy contributes to the portfolio. The column total gives the cumulative number of problems solved by the portfolio up to that point, computed as the sum of +new and the previous row’s total. Finally, the column adds expresses +new as a percentage of the current portfolio size.
We observe that the two most complementary strategies switch the efort mode from interleave to standard and use diferent values for Flip. Since the second strategy contributes 3.90% to the portfolio, this indicates a meaningful level of complementarity among the strategies. Furthermore, we observe that the majority of strategies use a term depth of 0, meaning they instantiate using constants only. This suggests that the strategies not shown in Figure 2 and Figure 3, specifically those with Depth > 0 and Flip > 0.0, do not yield any significant improvement.
We have presented preliminary experiments on the probabilistic generation of instantiation terms for quantified formulas in cvc5. The results indicate potential in our approach, as we were able to improve upon the reference baseline strategy. The best performance was achieved by strategies that generate terms complementary to those produced by other instantiation techniques. This highlights the importance of diversity in instantiation strategies and suggests that probabilistic generation can efectively fill gaps left by more deterministic methods. Leveraging this complementarity may be key to further improving solver performance on quantified benchmarks. In contrast, guided generation of more complex or deeper terms has not yet proven to be efective.
Future work will focus on improving the guided generation of complex terms. Given the exponential growth of the instantiation term space, an efective reduction of the search space is essential. One possible direction is to employ a learning-based approach to guide term generation. We would like to refine the interaction between probabilistic instantiation and existing instantiation techniques, exploring how to better coordinate or prioritize between them during solving. Additionally, we plan to investigate adaptive mechanisms that adjust term generation parameters dynamically based on solver progress or formula structure. Another direction is to explore richer probabilistic models, beyond simple frequency-based grammars, that can better capture structural patterns in useful instantiations. Finally, we intend to evaluate our approach on broader and more diverse benchmarks to better understand its strengths and limitations in diferent theory combinations.
This work is supported by the Czech MEYS under the ERC CZ project no. LL1902 POSTMAN, and by the European Union under the project ROBOPROX (reg. no. CZ.02.01.01/00/22_008/0004590), and by the RICAIP project that has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No 857306.
During the preparation of this work, the authors used ChatGPT in order to: Grammar and spelling check, Paraphrase and reword. After using this tool, the authors reviewed and edited the content as needed and take full responsibility for the publication’s content.