This work attempts to choose quantifiers to instantiate based on a feedback from the SMT solver. This tackles the challenge that if a problem contains many quantifier expressions, it eventually gets flooded by too many generated ground terms. Therefore, we instantiate only some of the quantifiers but the question is, which are the useful ones? The SMT solver is modeled as a multi-armed bandit, where each quantifier is a lever producing a positive reward if an instantiation of the quantifier was useful. The issue is that we do not know whether an instantiation was useful or not until the given problem instance is actually proven (and then it's too late). In this paper we explore several heuristics that attempt to assess the usefulness of quantifier instantiations.
Most approaches instantiate quantifiers gradually, meaning, the new instantiations are added
after testing that the old ones do not already yield a contradiction in the ground solver. In this
work, we propose to use dynamic machine-learning-based heuristic to decide which quantifiers
should be instantiated during solving. We model the problem as multi-armed bandits (MAB),
which is one of the simplest form of reinforcement learning [
The overall setup is shown in Figure 1. Quantifiers are instantiated in a loop that terminates if the ground solver determines that the ground part is unsatisfiable. Our guidance picks the set of quantifiers to be instantiated in each round. This guidance is based on feedback obtained from the ground solver.
Input formula
SMT solver
Ground assignment
Instantiation Ground solver
ML advice Instances
Feedback satisfiable unsatisfiable or infinite loop
In this paper, we only consider the simplest strategy for picking the ground terms that we
instantiate with: the enumerative instantiation [
In the standard MAB setting, only one lever is pulled at a time. This is not desirable in our setting, because this could cause an unwieldy number of instantiation rounds. Therefore we always pick a set of quantifiers (levers) to instantiate in each round. This is always done based on some score assigned to each quantifier, where the score is calculated from the observations made so far (Section 3). There are multiple ways of how one could use such scores. In our experiments, we use a simple strategy where the top percent of quantifiers is selected in each round, where is a fixed parameter.
The objective is to assign to each quantifier a score that determines how likely that quantifier is to be instantiated. This score combines two components. The first component estimates how useful the quantifier has been in the past. The second component pushes the search towards quantifiers that have been underused so far. This falls within the well-known paradigm in reinforcement learning: exploration versus exploitation.
The current implementation uses as a source of usefulness of a quantifier two values obtained from the SAT solver, namely dificulty and activity measures. Both of these sources provide an integer statistic for each quantifier, with values evolving in time. We further normalize the values, dividing them by the number of current quantifier instantiations. Hence we obtain the utility per quantifier instance. We use these values to estimate usefulness of quantifiers and to guide quantifier instantiation.
In our implementation, dificulty is mapping from formulas (those from input or lemmas generated during solving) to natural numbers, where a formula with higher dificulty contributes more towards a proof of unsatisfiability. This measure is incrementally updated during the course of SMT solving. In particular, when a theory solver generates a conflict clause or lemma , we compute the literals ℓ that are propositionally entailed by the negation of (e.g., the negation of all literals in a clause), call this set ilits( ). For each such ℓ, we increment the dificulty measure of the (oldest) formula such that the negation of ℓ is in ilits( ). We subsequently track this dificulty measure on the generated lemma . Notice that quantifier instantiation lemmas ⇒ [⃗ ↦→ ⃗ ] increment dificulty on the oldest formula that implies . The dificulty measure of the lemma itself will be incremented whenever literals in the instantiated body of the quantified formula participate in further conflicts and lemmas. Similarly, we measure activity, which tracks how many times a formula participated in propositional propagation.
As a basic estimate of the quantifier quality, we train a simple linear regression model to obtain reasonable weights and for the linear combination of normalized activity (nact) and normalized dificulty ( ndif ):
· nact + · ndif .
As training data, we collect statistics of the values of nact and ndif from runs on several thousand problems evaluated with 60 seconds time limit. The statistics contain the values of nact and ndif for each quantifier in every instantiation round, thusly recording the progress of the values in time. The quantifiers whose instantiations were needed to solve the problem are marked as positive, other quantifiers as negative. From this training data, we train a linear regression classifier. The linear regression training yielded the coeficients = 0.04 and = 0.1 and these shall be used for the experimental evaluation in Section 4. The prediction computed by the linear formula can be directly used as the quality estimate, or it can be used as a reward in the MAB setting as follows.
To include the exploration factor we use the upper confidence bound (UCB) formula, where the quality () of the quantifier at time step (quantifier selection round) is defined as () = () + √︃ log() () with () is the mean reward for the quantifier so far, and () is the number of times was selected for instantiation up to this point. As rewards, we use predictions of quantifier qualities obtained from the linear model described above. Finally, is the confidence value controlling the level of exploration with respect to exploitation. The idea behind UCB is that the quality is primarily governed by the reward. The second summand will be higher for the quantifiers that were less often selected in the previous instantiation rounds (quantifiers with smaller ()). Hence the quality of unselected quantifiers keeps increasing and they will eventually become selected in some future round. How fast this happens is controlled by the parameter where higher values favor exploration.
The above-presented ideas were implemented in the SMT solver cvc5 [
The default technique where all available quantifiers are instantiated in each round is used as the baseline. To assess the performance of our techniques for quantifier selection, we evaluate several random selection strategies. In each strategy, % of randomly selected quantifiers is instantiated with ranging from 10%, 20%, up to 90%. Apart from these control strategies, we evaluate our linear model from Section 3 where the quality of each quantifier is computed as a linear combination of two utility values nact and ndif . The linear model is evaluated in two modes, namely, with and without the use of the UCB formula. As with the random strategies, we evaluate several variants with diferent selection ratios , selecting % of the quantifier with the highest quality. In the case of the UCB formula, additional confidence coeficient is required to control the level of exploration. We evaluate several values for between 0.001 and 10.
The ML approach performs well in short timeouts. With the timeout of 1 s the baseline strategy, which instantiates all available quantifiers, solved 1107 problems. The worst of the random selection strategies for = 10% solved 1016 problems, and the best one for = 50% already outperformed the baseline with 1171 solved problems. The linear model scored slightly higher with 1186 problems, in particular, its best variant with = 50%. The UCB formula led to an almost identical performance with 1190 solved problems, namely, its variant with = 80% and = 3. Our techniques perform slightly better than the random selection. The two random strategies solved 1212 problems together, while the two ML strategies solved 1264.
The experiment progress is depicted in Figure 2, where the graphs show the number of problems solvable by each of the strategies in time . Both graphs use the baseline strategy as the reference. The left graph compares the baseline to the random selection, while the right graph compares it to the best ML-based selection technique, namely the linear model with the UCB formula. We see that the line for random 10% performs more poorly than the baseline. On the other hand, the random 50% line stays above the baseline up till ∼ 60 s. The experiment shows the versions with and without the UCB formula to be of comparable performance. The right graph, which compares our best ML selection method with best random selection, supports our previous observation that the ML selection slightly outperforms the random one. The ML approach stays above the baseline up till ∼ 100 s. The methods are slightly complementary, the version without UCB adds 6.4% to the problems solved by the UCB version.
While our strategies outperform the random selection, the improvement is rather small. This is further supported by Figure 3, which compares the strategies in a scatter plot. For each solved problem , a point is plotted at the position (1, 2) where is the runtime of strategy on problem . In both graphs, 1 is the baseline strategy, while 2 is the random selection of 50% in the left graph and the linear model with UCB on the right. Hence the points below the diagonal designate the runtime improvement, that is, problems solved faster than the baseline. For the ML approach we observe a cluster of points below the diagonal with time below 10 s. For larger times we observe both improvement and worsening of performance.
In this extended abstract we report on our initial experiments that attempt to estimate the
usefulness of quantifiers during search. This contrasts with standard machine learning techniques
that learn from one problem to another (cf. [
The experiments suggest that a guided quantifier selection can lead to a runtime improvement and hence to more problems solved with very short timeouts. It seems, however, that the improvement over the baseline strategy is decreasing with increasing time limits. In our future research, we plan to investigate whether an improvement over higher time limits can be achieved with more advanced methods for quantifier selection. In particular, we plan to investigate other metrics for the usefulness of quantifiers.
The results were supported by the Ministry of Education, Youth and Sports within the dedicated program ERC CZ under the project POSTMAN no. LL1902, the European Regional Development Fund under the Czech project AI&Reasoning no. CZ.02.1.01/0.0/0.0/15_003/0000466, and Amazon Research Awards. This article is part of the RICAIP project that has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No 857306.