Fair and Adventurous Enumeration of Quantifier Instantiations

TL;DR

This paper explores different strategies for ordering quantifier instantiations in SMT solvers, balancing fairness and adventurousness, and introduces techniques to discard irrelevant instantiations, improving solver performance.

Contribution

It introduces new ordering strategies for quantifier instantiations and techniques for discarding irrelevant tuples, enhancing SMT solver efficiency and flexibility.

Findings

Strategies impact solver performance significantly

Fair and adventurous enumeration balances exploration and fairness

Implemented techniques improve efficiency in cvc5 SMT solver

Abstract

SMT solvers generally tackle quantifiers by instantiating their variables with tuples of terms from the ground part of the formula. Recent enumerative approaches for quantifier instantiation consider tuples of terms in some heuristic order. This paper studies different strategies to order such tuples and their impact on performance. We decouple the ordering problem into two parts. First is the order of the sequence of terms to consider for each quantified variable, and second is the order of the instantiation tuples themselves. While the most and least preferred tuples, i.e. those with all variables assigned to the most or least preferred terms, are clear, the combinations in between allow flexibility in an implementation. We look at principled strategies of complete enumeration, where some strategies are more fair, meaning they treat all the variables the same but some strategies may be more adventurous, meaning that they may venture further down the preference list. We further describe new techniques for discarding irrelevant instantiations which are crucial for the performance of these strategies in practice. These strategies are implemented in the SMT solver cvc5, where they contribute to the diversification of the solver's configuration space, as shown by our experimental results.