Das Kapitel vertieft sich in die Erweiterung der modellbasierten Quantifizierungs-Instanziierung durch schnelle Aufzählungstechniken, um die Fähigkeiten von Zufriedenheitsmodulo-Theorien (SMT) zu verbessern. Es stellt eine neue Strategie vor, MBQI-Enum, die syntaxgesteuerte Synthese (SyGuS) mit modellbasierter Quantifizierer-Instanziation (MBQI) kombiniert, um eine breitere Palette von Kandidateninstanziationen zu generieren. Dieser Ansatz nutzt die schnellen Modellfindungsfähigkeiten von MBQI und die vielfältige Termgenerierung von SyGuS und macht ihn besonders effektiv bei der Lösung komplexer, quantifizierter Probleme. Das Kapitel bietet eine detaillierte Erläuterung der zugrunde liegenden Prinzipien, einschließlich Logik höherer Ordnung und SMT mit Quantifizierern, und präsentiert empirische Bewertungen, die beträchtliche Vorteile bei der Lösung von Benchmarks erster und höherer Ordnung zeigen. Die Implementierung von MBQI-Enum im cvc5-Solver zeigt ihre praktische Anwendbarkeit und unterstreicht ihr Potenzial, den Stand der Technik im Bereich SMT-Lösungen voranzutreiben. Das Kapitel behandelt auch verwandte Arbeiten und zukünftige Forschungsrichtungen und bietet Einblicke, wie die vorgeschlagene Strategie weiter verfeinert und erweitert werden kann, um noch schwierigere Probleme zu bewältigen.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
Satisfiability modulo theories (SMT) solvers rely on various quantifier instantiation strategies to support first- and higher-order logic. We introduce MBQI-Enum, an approach that extends model-based quantifier instantiation (MBQI) with syntax-guided synthesis (SyGuS) techniques. Our approach targets first-order theories without well-established quantifier instantiation techniques and higher-order quantifiers that can benefit from instantiations with \(\lambda \)-terms. By incorporating a SyGuS enumerator, our approach generates a broader set of candidate instantiations, including identity functions and terms containing uninterpreted symbols, thereby improving the effectiveness of MBQI.
1 Introduction
Satisfiability modulo theories (SMT) solvers combine a Boolean satisfiability (SAT) solver with decision procedures for interpreted theories. Several SMT solvers, including Bitwuzla [16], Boolector [17], cvc5 [2], veriT [7], and Z3 [15], also support quantifiers via Skolemization and instantiation. With complete instantiation strategies, SMT solvers offer a semidecision procedure for first-order logic with theories. SMT has also been partly extended to higher-order logic [4].
Quantifier instantiation is a technique whereby quantified variables in a formula are instantiated with ground terms until a contradiction is found or all necessary instantiations have been generated. Consider the unsatisfiable axiom \((\forall x.\;\textsf{p}\;x) \mathrel \wedge \lnot \,\textsf{p}\;\textsf{b}\). The SAT solver first finds a model that makes \(\forall x.\;\textsf{p}\;x\) true and \(\textsf{p}\;\textsf{b}\) false, taken as black boxes. Then the quantifier instantiation strategy of the SMT solver might heuristically instantiate x with \(\textsf{a}\), resulting in the formula \((\forall x.\;\textsf{p}\;x) \Longrightarrow \textsf{p}\;\textsf{a}\), which is conjoined with the axiom. Next, the SAT solver finds a new model that also makes \(\textsf{p}\;\textsf{a}\) true. At this point, the instantiation strategy might instantiate x with \(\textsf{b}\), resulting in \((\forall x.\;\textsf{p}\;x) \Longrightarrow \textsf{p}\;\textsf{b}\). Since the SAT solver cannot make \(\textsf{p}\;\textsf{b}\) both true and false at the same time, the axiom conjoined with the two additional formulas is unsatisfiable at the SAT level, meaning that the original axiom is unsatisfiable in the SMT logic.
Anzeige
One successful instantiation strategy is model-based quantifier instantiation (MBQI) [9]. Briefly, it iteratively refines a candidate model constructed from the quantifier-free part of the problem. This model guides the generation of new terms for instantiating quantifiers, reducing the search space. MBQI is complete for certain fragments and tends to generate small models for satisfiable problems. But it also has some limitations: First, MBQI instantiates quantifiers only with terms that denote values in a theory. In particular, it does not consider the problem’s uninterpreted symbols when creating instantiations, leading it to miss some useful instantiations. Second, for higher-order problems, MBQI cannot generate function terms that return an argument, such as the identity \(\lambda x.\; x\).
Another instantiation strategy, which addresses these limitations, is syntax-guided instantiation (SyQI) [18]. This constructs a grammar for each universally quantified variable according to its type and uses enumerated terms derived from the grammar as instantiations. Its main weakness is that although it is model-based like MBQI, it uses a less scalable approach to refining models that centers around syntactic constraints.
In this paper, we propose a new strategy, MBQI-Enum, that combines the strengths of MBQI and SyQI. Specifically, our strategy augments the set of instantiations created from the MBQI model with instantiations generated by a syntax-guided synthesis (SyGuS) grammar. It incorporates uninterpreted symbols gathered from the problem. For higher-order problems, it also considers \(\lambda \)-abstractions as potential instantiations. In this way, we exploit the fast model-finding capabilities of MBQI and the diversity of terms considered by SyQI.
Our work shares some similarities with Preiner et al. [21], but their approach was limited to selected first-order theories and did not handle higher-order logic. Our approach is resolutely pragmatic; it does not aim at completeness, which can be achieved using other instantiation strategies.
Anzeige
As an example where \(\lambda \)-terms are needed, consider the unsatisfiable problem consisting of the axiom \(\forall z.\> \exists x{,}\>y.\; z\; x\; y \not = x\), where z ranges over binary functions. Running cvc5 with strategies such as MBQI and higher-order E-matching [4] leads the solver to give up early. By contrast, with our strategy, cvc5 immediately finds a contradiction based on the substitution \(\{z \mapsto \lambda x{,}\> y.\; x\}\). Indeed, if we instantiate z with \(\lambda x{,}\> y.\; x\) in the axiom and \(\beta \)-reduce, we obtain \(x \not = x\).
We implemented MBQI-Enum in cvc5. Our empirical evaluation finds that the strategy increases the number of solved problems for a benchmark suite consisting of various first-order SMT-LIB files by a noticeable margin. Our approach is especially useful to solve unsatisfiable problems involving theories without well-established quantifier instantiation techniques. We can also report substantial gains on higher-order TPTP benchmarks. The raw evaluation data are publicly available online.1 Our source code, along with instructions for reproducing the experiments, is also available online.2
2 Preliminaries
Our work relies on the following pillars: higher-order logic, SMT with quantifiers, MBQI, and SyQI.
Higher-Order Logic. Monomorphic higher-order logic [1, 10], also called simple type theory [8], generalizes classical first-order logic by allowing quantification over functions. The syntax distinguishes between types and terms. Types \(\tau \) are either base types \(\kappa \) or applications of the function arrow \(\rightarrow \) to two types: \(\tau _1 \rightarrow \tau _2\). The type of Booleans is denoted by \( o \).
The term language is based on Church’s simply typed \(\lambda \)-calculus, where terms t, e are inductively defined as variables w, x, y, z, ..., function symbols \(\textsf{p}\), \(\textsf{f}\), constants \(\textsf{a}\), \(\textsf{b}\), \(\textsf{c}\), term applications \(t \; t'\), and \(\lambda \)-abstractions \(\lambda x. \; t\), where x is the bound variable and t is the body. A variable is free in a term if it is not bound by a \(\lambda \)-abstraction. We let \(\bar{x}\) stand for \(x_1,x_2,\dots ,x_n\), where \(n \ge 1\). Terms are syntactically equal modulo \(\alpha \)-, \(\beta \)-, and \(\eta \)-conversion, meaning, for example, that (\(\lambda x.\;x)\;\textsf{c}\) is equal to \(\textsf{c}\). Throughout this work, we assume that terms are expressed in \(\eta \)-long \(\beta \)-normal form, meaning that \(\eta \)-expansion and \(\beta \)-reduction have been applied exhaustively. The type of a term t is of the form \(\tau _1 \rightarrow \dots \rightarrow \tau _n \rightarrow \tau \), where \(\tau _i\) are the argument types and \(\tau \) is the result type. If \(\tau \) is of type \( o \), which is the distinguished Boolean type, we call t a predicate. A term of type \( o \) is called a formula.
SMT with Quantifiers. Traditionally, SMT solvers work on problems in first-order logic, but they have partly been extended to higher-order logic [4], and in this paper we consider both first- and higher-order problems. SMT solvers that support quantifiers typically do so via a combination of Skolemization and instantiation: Universal quantifiers occurring negatively can be Skolemized; universal quantifiers occurring positively are instantiated heuristically; and existential quantifiers are expressed in terms of \(\forall \) using the equivalence \((\exists x.\;\phi ) \Longleftrightarrow \lnot (\forall x.\>\lnot \phi )\). To simplify the presentation, we will assume that formulas are in a normal form where possibly negated \(\forall \)-quantifiers all appear in a cluster at the top level—e.g., \(\forall x, y.\> \lnot \, \forall z.\; \textsf{p}\; x\; y\; z\).
Let \(\mathcal {T}\) be a theory for a set of interpreted symbols, and let F be the input formula over \(\mathcal {T}\). The goal is to find a model of F or derive a contradiction. If F does not contain quantifiers, the quantifier-free part of the SMT solver searches for a \(\mathcal {T}\)-satisfiable set L of literals that propositionally satisfies F. If such an L exists, F is \(\mathcal {T}\)-satisfiable (i.e., satisfiable with respect to \(\mathcal {T}\)); otherwise, F is \(\mathcal {T}\)-unsatisfiable.
If the formula F contains quantifiers, the quantifier-free solver cannot be directly applied. In the SMT solver’s main loop, presented in Algorithm 1, the SMT solver tries to find a set L of literals whose atoms come from F and that propositionally satisfies F. Briefly, L is partitioned into a set E of ground literals and two sets of quantified literals, \(Q_\textrm{p}\) and \(Q_\textrm{n}\). The ground literals within E must be \(\mathcal {T}\)-satisfiable, \(Q_\textrm{p}\) consists of formulas of the form \(\forall \bar{x}.\> \phi \), and \(Q_\textrm{n}\) consists of formulas of the form \(\lnot \, \forall \bar{x}.\> \phi \). If the solver is unable to find such an L, it concludes that the formula F is \(\mathcal {T}\)-unsatisfiable.
On the other hand, if a set L of literals is found, new lemmas A are generated through the instantiation and Skolemization rounds. The instantiation round generates instantiation lemmas—that is, lemmas of the form \(q_i \Longrightarrow q_i\sigma \)—from the sets \(Q_\textrm{p}\) and E. For each \(q_i \in Q_\textrm{p}\), an instantiation strategy computes substitutions \(\sigma \) for every top-level variable in \(q_i\) mapping them to terms. The Skolemization round generates Skolemization lemmas from the set \(Q_\textrm{n}\)—that is, lemmas of the form \(\lnot q_i \Longrightarrow \lnot q_i\sigma _{j,i}\), where \(\sigma _{j,i}\) instantiates every top-level variable in \(q_i\) with a Skolem constant. (We abuse notation and write \((\forall \bar{x}.\; \phi )\sigma \) to mean \(\phi \sigma \), syntactically conflating quantifier instantiation and substitution.) The lemmas are then added to the original formula F, and the SMT loop is called recursively. On line 12 of Algorithm 1, we assume that the instantiation strategy denoted by \(\textsc {insts} \) is model-sound, meaning that if \(\textsc {insts} \) returns an empty set of substitutions, it indicates that the formula F is \(\mathcal {T}\)-satisfiable.
We now define the instantiation strategy \(\textsc {insts} \) starting with a naive approach. Subsequently, we will introduce more advanced techniques, including MBQI and SyQI, followed by our strategy, MBQI-Enum. These strategies can replace the naive approach to improve the solver’s efficiency.
Definition 2
An instantiation strategy takes as input a set of ground terms E and a quantified formula q of the form \(\forall \bar{x}.\>\phi \), and outputs a set of grounding substitutions \(\{\sigma _1, \dots , \sigma _{m}\}\), where the variables mapped by \(\sigma _i\) are exactly the variables in \(\bar{x}\) for each \(i \in \{1, \dots , m\}\).
Example 3
Let \(\textsf{a} : Int \) and \(\textsf{p} : Int \rightarrow Bool \). Let F be the formula \((\forall y.\>\textsf{p}\;y) \,\wedge \,\lnot \,\textsf{p} \;\textsf{a}\), where \(y : Int \). In the SMT loop, the sets \(E = \{\lnot \,\textsf{p}\;\textsf{a}\}\), \(Q_\textrm{p} = \{\forall y.\>\textsf{p} \;y\}\), and \(Q_\textrm{n} = \emptyset \) are defined. The naive instantiation strategy produces substitutions mapping y to terms from E of the same type as y, as shown below:
The instantiation lemma \((\forall y.\> \textsf{p} \; y) \Longrightarrow \textsf{p} \; \textsf{a}\) is added to F. Now, the quantifier-free solver finds a contradiction.
The most widely used strategy for quantifier instantiation is E-matching [14]. This is a heuristic and typically incomplete technique that chooses substitutions by matching ground terms with patterns. In Example 3, the ground term \(\textsf{p} \;\textsf{a}\) matches \(\textsf{p}\;y\) for substitution \(\{y \mapsto \textsf{a}\}\), and hence this substitution is returned by the strategy. Over the past decade, SMT solvers have been extended with more sophisticated approaches. Conflict-based instantiation [26] is another incomplete technique that attempts to find a single instantiation that would induce a ground conflict, before resorting to E-matching. MBQI [9] is a technique for finding instantiations that refute a candidate model, and is typically run when E-matching saturates. This strategy is also able to answer “\(\mathcal {T}\)-satisfiable” when no such instantiation can be found. Enumerative instantiation [22] is an alternative to MBQI that focuses on finding instantiations over the current set of ground terms that are not entailed in the current context. This has similar properties to MBQI but is more tailored for unsatisfiable instances.
Quantifier instantiation strategies that target specific theories have also been proposed. Counterexample-guided instantiation [24] is complete for specific theories with quantifiers that admit quantifier elimination, such as linear arithmetic and bit vectors. SyQI [18] is a more general purpose strategy that uses syntax-guided synthesis for enumerating instantiations and is effective for theories that otherwise do not have well-established instantiation strategies.
MBQI. MBQI iteratively refines a candidate model M constructed from the quantifier-free part of the problem. As shown in Algorithm 4, the strategy replaces function symbols in the body \(\phi \) of the quantified formula with their interpretation in M. If \(\lnot \,\phi ^M\) is \(\mathcal {T}\)-satisfiable, this means that a model \(M'\) exists, and the strategy returns the substitution \(\{y_1 \mapsto y_1^{M'}{,}\; {\dots ,}\; y_n \mapsto y_n^{M'}\}\), where \(y_i^{M'}\) represents a term denoting the interpretation for the variable \(y_i\) in \(M'\).
Example 5
Let \(\textsf{a} : Int \) and \(\textsf{p} : Int \rightarrow Bool \). Let F be the input formula
where \(y : Int \). In the SMT loop, our set of literals L is partitioned into \(E = \{0 < \textsf{a} < 2{,}\; \lnot \,\textsf{p}\;\textsf{a}\}\), \(Q_\textrm{p} = \{\forall y.\> \textsf{p}\;y\}\), and \(Q_\textrm{n} = \emptyset \). MBQI builds a model M from E—assume \(\textsf{a}^M = 1\) and \(\textsf{p}^M = \lambda x.\;x \not = 1\). (We abuse notation by denoting values using \(\lambda \)-terms.) It then considers the negation of the body of the quantified formula in \(Q_\textrm{p}\) under the interpretation M, which is \(\lnot \,(\lambda x.\;x \not = 1)\;y\), which simplifies to \(y=1\) and has a model \(M'\) where \(y^{M'} = 1\). Thus, MBQI generates the substitution \(\{y \mapsto 1\}\), from which the instantiation lemma \((\forall y.\> \textsf{p}\;y) \Longrightarrow \textsf{p}\;1\) is constructed and added to F. Now, the quantifier-free solver finds a contradiction.
Example 6
Let \(\textsf{f} : Int \rightarrow Int \rightarrow Bool \). Let F be the higher-order formula
where \(x : Int \) and \(y : Int \rightarrow Int \). The set L is partitioned into sets \(E = \emptyset \), \(Q_\textrm{p} = \{\forall x{,}\>y.\;y\;x \not = y\;(\textsf{f}\;x)\}\), and \(Q_\textrm{n} = \emptyset \). MBQI constructs a model M for E such that \(\textsf{f}^M = \lambda z.\;0\). It then considers the negation of the body of the quantified formula in \(Q_\textrm{p}\) under the interpretation M. This is \(\lnot \,y\;x \not = y\;((\lambda z.\;0)\;x)\), which simplifies to \(y\;x = y\;0\) and has a model \(M'\) where \(x^{M'} = 0\) and \(y^{M'} = \lambda z.\;0\). Thus, it generates the substitution \(\{x \mapsto 0{,}\; y \mapsto \lambda z.\;0\}\) based on the candidate model. Now, the quantifier-free solver finds a contradiction. Indeed, if we instantiate x and y with this substitution and \(\beta \)-reduce, we obtain \(0 \not = 0\).
SyQI. SyQI uses SyGuS to choose instantiation terms. It aims to synthesize a term t for a variable x in a given formula \(\forall x.\> \textsf{p}\;x\) such that \(\lnot \,\textsf{p}\;t\) holds. Each quantified variable is associated with a SyGuS grammar. The main advantage of SyQI is that, unlike MBQI, it does not require theory-specific quantifier instantiation procedures. The only parts that depend on the theory are the grammar and the \(\mathcal {T}\)-satisfiability check for the generated instances.
3 The Method
The core idea behind our new instantiation strategy, MBQI-Enum, is to integrate a SyGuS enumerator within MBQI, thereby enabling the generation of a broader set of candidate instantiations for quantified variables.
Instantiation Strategy. Instead of restricting instantiations to ground terms derived from the current MBQI model, our strategy uses a SyGuS grammar to produce additional candidate instantiations. This grammar is not limited to ground terms with the types of the quantified variables; rather, it incorporates uninterpreted symbols gathered from the entire formula. As a result, it generates a more extensive and comprehensive language of terms.
For each quantified variable in a formula, our strategy performs iterative term enumeration. It generates candidate substitutions from the extended grammar and tests each enumerated term within the formula. For each enumerated term, the strategy tries to apply it as an instantiation for the quantified variable. For higher-order problems, it also considers \(\lambda \)-abstractions as candidate instantiations. If the strategy produces a useless instance according to the current model, it continues to the next candidate until a suitable instantiation is found or all possibilities are exhausted.
When none of the candidate instantiations derived from the SyGuS enumeration prove successful, MBQI-Enum reverts to the original MBQI model-derived instantiation. This fallback mechanism ensures that our strategy can in principle solve any problem that MBQI can solve.
Our initial motivation for developing MBQI-Enum was to increase cvc5’s success rate on higher-order problems. Nevertheless, incorporating uninterpreted symbols gathered from the entire formula extends our approach’s applicability to first-order problems using various SMT theories.
Our approach is presented in Algorithm 7. The strategy starts by invoking MBQI to generate a set of initial substitutions \(\mathrm {\Sigma }\), since the goal is to postprocess the substitutions generated by MBQI using a SyGuS enumerator. If \(\mathrm {\Sigma }\) is empty, the strategy immediately returns an empty set, indicating that no valid instantiation could be found. Otherwise, it proceeds by initializing \(\mathrm {\Sigma }\) to contain a single substitution \(\sigma \). Next, it generates additional substitutions by extending the current one using the SyGuS enumerator.
Our strategy then iterates over the quantified variables \(y_i\) in the formula q to instantiate. For each variable, it constructs a grammar \(G_i\) used to guide the enumeration of candidate terms for substituting \(y_i\). The enumeration starts by generating terms from \(G_i\) in a sequential manner. For each term e, the strategy creates a new substitution \(\sigma '\) by mapping \(y_i\) to e in the current substitution \(\sigma \). It then checks whether the negation of the body \(\phi \) under \(\sigma '\) is \(\mathcal {T}\)-satisfiable. This check serves to maintain the invariant that the negation of the body of the quantified formula, after applying the current substitution, remains \(\mathcal {T}\)-satisfiable. In other words, we want to ensure that the generated instantiation refutes the current model (cf. line 6 of Algorithm 4). If it does, \(\sigma \) is updated to \(\sigma '\), and the strategy moves on to the next variable. Once all variables have been considered, the strategy returns the refined substitution \(\sigma \).
Choice of Grammar. Term enumeration is based on a SyGuS grammar. Choosing an appropriate grammar for each quantified variable is crucial for selecting the correct instantiations. Our strategy builds a set S of symbols based on three Boolean options: \( syms\_global \), \( ext\_vars \), and \( syms\_local \). These options specify which symbols from the formula F will be included when constructing the SyGuS grammar.
If no options are enabled, the set S is empty. If \( syms\_global \) is enabled, all function symbols from the entire formula F are contained in S. If \( ext\_vars \) is enabled, S is augmented with bound variables from the formula q that are not yet instantiated. Finally, if \( syms\_local \) is enabled, the set S also contains function symbols specifically from q. Based on these settings, our approach constructs a grammar that generates terms over the symbols in S, while ensuring that these terms are well-typed with respect to the type of \(y_i\).
For higher-order variables, since we use \(\eta \)-long \(\beta \)-normal form, it is sufficient to consider only grammars that generate \(\lambda \)-abstractions. The variables bound by these \(\lambda \)-abstractions are considered terminal symbols of the grammar that generates the abstraction’s body. For example, for a function variable whose arity is n and whose arguments are of the same base type as its return type, we add grammar rules of this form:
$$\begin{aligned} A & :\,\!:= \lambda x_1, \dots , x_n.\; B \\ B & :\,\!:= x_1 \mid \cdots \mid x_n \end{aligned}$$
Moreover, there will be additional rules for B and possibly for some of the grammar’s other nonterminal symbols. This ensures that any \(\lambda \) instantiations are formed by enumerating the body B over the bound variables \(x_1, \dots , x_n\).
Example 8
Let \(\textsf{a}: Int \) and \(\textsf{p} : Int \rightarrow Bool \). Let F be the input formula
where \(y: Int \rightarrow Int \). The set L is partitioned into \(E = \{\textsf{p}\;\textsf{a}\}\), \(Q_\textrm{p} = \{\forall y.\>\lnot \,\textsf{p}\;(y\;\textsf{a})\}\), and \(Q_\textrm{n} = \emptyset \). MBQI generates substitutions such as \(\{y \mapsto \lambda x.\; 0\}\), \(\{y \mapsto \lambda x.\; 1\}\), \(\dots \). As a result, the solver does not terminate. In contrast, MBQI-Enum augments these instantiations based on enumeration. On the first iteration of the SMT loop, MBQI-Enum considers the set \(\mathrm {\Sigma } = \{\{y \mapsto \lambda x.\; 0\}\}\) consisting of the first substitution generated by MBQI. MBQI-Enum first constructs a grammar for y. The set of symbols S is empty. The grammar is
Next, MBQI-Enum enumerates terms derived from the grammar and creates the substitution \(\sigma ' = \{y \mapsto \lambda x.\; x\}\) by updating \(\sigma \) with the enumerated term \(\lambda x.\; x\) from the grammar. The strategy then checks whether the negation of the body of the quantified formula after applying \(\sigma '\) is \(\mathcal {T}\)-satisfiable. Indeed, if we instantiate y with \(\lambda x.\; x\) and \(\beta \)-reduce, we obtain \(\textsf{p}\;\textsf{a}\), which is \(\mathcal {T}\)-satisfiable. The substitution \(\sigma \) is then updated to \(\{y \mapsto \lambda x.\; x\}\) and returned. Back in the SMT loop, the instantiation lemma \((\forall y.\>\lnot \,\textsf{p}\;(y\;\textsf{a}))\Longrightarrow \lnot \,\textsf{p}\;\textsf{a}\) is added to F. Now, the quantifier-free solver finds a contradiction.
The candidate substitutions generated by MBQI-Enum (M) are listed below:
The first column shows the number of the SMT loop iteration. The second column shows the quantified formula q, and the third column shows the set E of ground literals before every iteration. The fourth column shows the possible selection of substitutions of y that are considered with MBQI-Enum, and the fifth column shows the set E after every iteration.
In this example, MBQI-Enum was able to terminate in the first iteration, since it found a substitution for y that immediately leads to a refutation, whereas MBQI considers a repeating pattern of instantiations that leads to a timeout.
Another useful candidate substitution would have been \(\{y \mapsto \lambda x.\;\textsf{a}\}\). MBQI-Enum would have found this substitution as well if it had not terminated after finding \(\{y \mapsto \lambda x.\;x\}\).
In an informal, preliminary evaluation on higher-order TPTP benchmarks, we determined that the most successful configuration enables \( ext\_vars \) and \( syms\_local \) and leaves \( syms\_global \) disabled. The following examples are based on this configuration.
Example 9
Let \(\textsf{p} : Int \rightarrow Bool \) and \(\textsf{f}: Int \rightarrow Int \). Let F be the input formula
where \(y: Int \rightarrow Int \) and \(z: Int \). The set L is partitioned into sets \(E = \emptyset \), \(Q_\textrm{p} = \{\forall y.\> \lnot \,\forall z.\> \lnot \,\textsf{p}\;(y\;z) \vee \textsf{p}\;(\textsf{f}\;z)\}\), and \(Q_\textrm{n} = \emptyset \). MBQI generates substitutions such as \(\{y \mapsto \lambda x.\; 0\}, \{y \mapsto \lambda x.\; 1\}, \dots \), and the solver goes on forever. In contrast, MBQI-Enum adds the first substitution generated by MBQI, \(\{y \mapsto \lambda x.\; 0\}\), to the set \(\mathrm {\Sigma }\) and proceeds to postprocess it. Our strategy first constructs a grammar for y using the function symbols from q. The set of symbols used is \(S = \{\textsf{f}, \textsf{p}\}\). The grammar is
In the first iteration, MBQI-Enum generates the substitution \(\sigma = \{y \mapsto \lambda x.\; x\}\). The instantiation lemma \((\forall y.\>\lnot \,\forall z.\> \lnot \,\textsf{p}\;(y\;z) \vee \textsf{p}\;(\textsf{f}\;z)) \Longrightarrow \lnot \,\forall z.\> \lnot \,\textsf{p}\;z \vee \textsf{p}\;(\textsf{f}\;z)\) is added to F. The set L is now partitioned into \(E = \emptyset \), \(Q_\textrm{p} = \{\forall y.\> \lnot \,\forall z.\> \lnot \,\textsf{p}\;(y\;z) \vee \textsf{p}\;(\textsf{f}\;z)\}\), and \(Q_\textrm{n} = \{\lnot \,\forall z.\> \lnot \,\textsf{p}\;z \vee \textsf{p}\;(\textsf{f}\;z)\}\). Next, the quantifier in \(Q_\textrm{n}\) is Skolemized. The Skolemization lemma \((\lnot \,\forall z.\> \lnot \,\textsf{p}\;z \vee \textsf{p}\;(\textsf{f}\;z)) \Longrightarrow \textsf{p}\;\textsf{sk}_1 \wedge \lnot \,\textsf{p}\;(\textsf{f}\;\textsf{sk}_1)\) is added to F. As a result, the set E is updated to \(\{\textsf{p}\;\textsf{sk}_1, \lnot \,\textsf{p}\;(\textsf{f}\;\textsf{sk}_1)\}\).
In the next iteration, the substitution \(\sigma \) is modified to \(\{y \mapsto \lambda x.\; \textsf{f}\;x\}\), incorporating the enumerated term \(\lambda x.\; \textsf{f}\;x\) from the grammar. The instantiation lemma \((\forall y.\> \lnot \,\forall z.\> \lnot \,\textsf{p}\;(y\;z) \vee \textsf{p}\;(\textsf{f}\;z)) \Longrightarrow \lnot \,\forall z.\> \lnot \,\textsf{p}\;(\textsf{f}\;z) \vee \textsf{p}\;(\textsf{f}\;z)\) is then added to F. After Skolemization, the set E is augmented with \(\{\textsf{p}\;(\textsf{f}\; \textsf{sk}_2), \lnot \,\textsf{p}\;(\textsf{f}\;\textsf{sk}_2)\}\). The quantifier-free solver finds a contradiction. Indeed, if we instantiate y with \(\lambda x.\; \textsf{f}\;x\) in F, \(\beta \)-reduce, and Skolemize z, we obtain \(\textsf{p}\;(\textsf{f}\;\textsf{sk}_2) \wedge \lnot \,\textsf{p}\;(\textsf{f}\;\textsf{sk}_2)\).
The candidate substitutions generated by MBQI-Enum (M) are listed below:
In this example, our strategy terminated in the second iteration, whereas MBQI would lead the solver to time out.
Example 10
In this example, our strategy is run with and without the \( syms\_ \)\( global \) option enabled. Let u be an uninterpreted sort, and let \(\textsf{a}: u\) and \(\textsf{b}: u\). Let F be the input formula
where \(x: (u \rightarrow u) \rightarrow u\), \(y: u \rightarrow u\), and \(z: u \rightarrow u\). The set L is partitioned into \(E = \{\textsf{a}\not =\textsf{b}\}\), \(Q_\textrm{p} = \{\forall x{,}\>y{,}\>z.\; x\;y = x\;z\}\), and \(Q_\textrm{n} = \emptyset \). MBQI-Enum fails to construct a grammar for a variable x, y, or z that has any terms of the same type as the variable. As a result, it cannot generate any substitutions, and the solver gives up early. In contrast, when the \( syms\_global \) option is enabled in MBQI-Enum, function symbols from the entire formula F are used to construct a grammar for each variable x, y, and z. For these variables, the set of symbols is \(\{\textsf{a}, \textsf{b}\}\). The grammar for x follows:
(Since w is of unary function type, we pass an argument corresponding to the nonterminal \(\mathcal {B}\) in the second grammar rule.) The grammar for y and z follows:
Our strategy then enumerates terms derived from the grammar and builds the substitutions \(\{x \mapsto \lambda w.\; w\;\textsf{b}\}, \{y \mapsto \lambda w.\; w\}\), and \(\{z \mapsto \lambda w.\;\textsf{a}\}\). The instantiation lemma \( (\forall x{,}\>y{,}\>z.\> x\;y = x\;z) \Longrightarrow \textsf{b} = \textsf{a} \) is added to F. Now, the quantifier-free solver finds a contradiction. Indeed, if we instantiate x with \(\lambda w.\; w\;\textsf{b}\), y with \(\lambda w.\; w\), and z with \(\lambda w.\;\textsf{a}\) in F and \(\beta \)-reduce, we obtain \(\textsf{a} = \textsf{b} \mathrel \wedge \textsf{a} \not = \textsf{b}\).
The candidate substitutions generated by MBQI-Enum (M) are listed below:
The same information is provided for MBQI-Enum with the option \( syms\_global \) enabled (M\(+\)g) below:
In this example, MBQI-Enum with \( syms\_global \) was able to terminate in the first iteration, since it found a substitution for the quantified variables that leads to a refutation. By contrast, default MBQI-Enum does not terminate since it cannot build any substitutions.
4 Implementation and Heuristics
We implemented MBQI-Enum as an extension of cvc5’s implementation of MBQI. Our strategy is invoked after the current MBQI strategy returns a candidate instantiation (line 3 of Algorithm 7).
For each variable, our algorithm chooses a grammar (line 9) and initializes a term enumeration data structure. Since the choice of the grammar is fixed over the course of solving, the grammar is constructed only once. Our implementation uses the utility for fast SyGuS enumeration described by Reynolds et al. [23] as a black box. Since the grammar for each variable is fixed, we can cache the enumeration and invoke this utility only on line 11 of Algorithm 7, when j is larger than the number of terms we have generated on a previous run, where we notice that a term that was skipped in a previous call to this method may be incorporated into instantiations on later calls.
On line 15 of Algorithm 7, we use cvc5’s ability to call a copy of itself as a subsolver. As an optimization, this satisfiability check can be avoided if the query to check simplifies to “true” or “false.”
5 Evaluation
We extensively evaluated our cvc5 implementation of MBQI-Enum on both higher- and first-order benchmarks.
Setup. As the base configuration, we use the setup that we found to be the most successful in a preliminary evaluation: MBQI-Enum with the options \( ext\_vars \) and \( syms\_local \) enabled by default. We denote this configuration by cvc5[M].
We first compare the performance of the base configuration against traditional instantiation techniques: cvc5[e], which uses enumerative instantiation [22]; cvc5[s], which uses SyQI [18]; cvc5[c], which uses counterexample-guided instantiation [24]; and cvc5[m], which uses MBQI [9].
Additionally, for higher-order problems, we also include a comparison with the state-of-the-art provers Vampire [6] and Zipperposition [28]. For Vampire, we used its portfolio mode, while Zipperposition was run in its so-called “best” mode, since it does not include a portfolio.
Next, we compare the base configuration on first-order benchmarks with three state-of-the-art SMT solvers: Z3 [15], the only SMT solver besides cvc5 that supports all the logics handled by our implementation; Bitwuzla [16], which supports only logics without arithmetic; and Boolector [17], which implements the most closely related approach to ours, counterexample-guided model synthesis [21], but focuses only on the theory of bit vectors.
Finally, we compare the performance of all four MBQI-Enum configurations on both higher-order and first-order problems. In this evaluation, we toggled one option at a time: cvc5[M−x] denotes MBQI-Enum with \( ext\_vars \) disabled, cvc5[M\(-\ell \)] denotes MBQI-Enum with \( syms\_local \) disabled, and cvc5[M\(+\)g] denotes MBQI-Enum with \( syms\_global \) enabled.
We performed all experiments on a system with a 40-core Intel Xeon Silver 4114 processor at 2.20 GHz and with 192 GB of RAM using Debian Bookworm as the operating system. We used a time limit of 60 seconds for each benchmark.
Higher-Order Problems. The higher-order part of the experiments was carried out on monomorphic higher-order problems (TH0) from version 9.0.0 of the TPTP library [27]. The benchmark set consists of 2762 problems. From the 3962 TH0 problems, we excluded 1200 benchmarks that one or more systems could not parse (e.g., because they use arithmetic).
Table 1.
MBQI-Enum vs. other strategies and provers on TPTP TH0 benchmarks
Dummy
The results are summarized in Table 1. In this and the following tables, bold indicates the most successful system. Notably, our approach achieves the highest total count of solved benchmarks, surpassing the nearest competitor by 36 solved problems. Overall, it outperforms all other cvc5 strategies as well as Zipperposition in higher-order logic and solves 87 fewer unsatisfiable problems than Vampire. Our strategy’s advantage over Zipperposition likely stems from using Zipperposition’s “best” mode instead of a portfolio. Remarkably, our strategy manages to solve 129 satisfiable problems, whereas Vampire solves only 6, and Zipperposition none.
Although our approach is based on both MBQI and SyQI, it is considerably stronger than either of those techniques used individually. Specifically, compared with MBQI, which was until now the most successful strategy in cvc5, MBQI-Enum solves an additional 41 problems without any losses. When compared with SyQI, our strategy solves 417 more benchmarks while also incurring no losses.
Table 2 shows the evaluation of the different configurations of MBQI-Enum on higher-order problems. We see that all three options are beneficial, but for \( syms\_global \) the difference is only two problems. (In our preliminary evaluation, we had found \( syms\_global \) to be slightly harmful, which is why we disabled it by default.)
Table 2.
MBQI-Enum configurations on TPTP TH0 benchmarks
Dummy
First-Order Problems. The experiments on first-order problems were conducted on the SMT-LIB benchmarks [5] from April 2024, focusing on logics that support quantifiers. We included logics involving theories such as floating-point arithmetic, linear and nonlinear arithmetic, and bit vectors. Overall, we consider the logics BV (bit vectors), FP (floating-point arithmetic), LIA (linear integer arithmetic), LRA (linear real arithmetic), NIA (nonlinear integer arithmetic), NRA (nonlinear real arithmetic), and their combinations: BVFP, BVFPLRA, and FPLRA. We also incorporate ABV (arrays and bit vectors) and UFBV (uninterpreted functions with bit vectors). In total, our benchmark set consists of 21605 problems.
Table 3.
MBQI-Enum vs. other techniques and solvers on SMT-LIB benchmarks
Dummy
The results, summarized in Table 3, show that our approach performs remarkably well against all other cvc5 configurations, as well as against Boolector, Bitwuzla, and Z3, across all SMT logics. Notably, it achieves the highest total count of benchmarks solved, surpassing the nearest competitor by 597 solved problems. Our strategy solves the most satisfiable problems in ABVFP and NIA and achieves the highest number of unsatisfiable benchmarks solved in FP.
For the evaluated SMT theories, our strategy is a clear improvement over previous instantiation strategies. When compared with MBQI, it successfully solves an additional 701 problems while incurring a loss of 79 problems across all logics. The raw evaluation data also reveals a notable reduction in timeouts, decreasing from 3491 to 2343.
Our strategy also substantially outperforms enumerative instantiation and SyQI across most benchmark categories. Both of these strategies share an enumerative nature. The former relies on evolving ground terms within the current context, while the latter employs a fixed grammar derived from the initial set of terms. Overall, enumerative instantiation and SyQI perform clearly better than MBQI on unsatisfiable benchmarks (\(+442\)), but they underperform on satisfiable benchmarks (\(-805\)). This highlights the need for a hybrid approach that combines model-based and enumerative techniques. Our strategy incorporates the enumerative aspects of SyQI while enhancing the model-based features of MBQI to generate instantiations. This is likely why it outperforms all the mentioned configurations. Our strategy also matches or outperforms counterexample-guided instantiation in most logics. However, in logics such as LRA, counterexample-guided instantiation is expected to perform better due to its specialized handling of such theories.
Compared with Boolector, our strategy outperforms it on both satisfiable and unsatisfiable benchmarks, solving 105 more benchmarks overall. Compared with Bitwuzla and Z3, our approach performs very well across various logics, often closely matching or even surpassing both competitors. Overall, our strategy solves 433 more benchmarks than Bitwuzla and 597 more than Z3 in total. Bitwuzla is generally stronger for satisfiable problems, which is not surprising because MBQI-Enum is primarily designed for deriving contradictions. Z3’s higher success rate for real arithmetic is likely attributable to its well-established instantiation strategies for these theories.
Finally, the evaluation of the various configurations of MBQI-Enum on first-order SMT-LIB benchmarks across different theories is shown in Table 4. We see that most configurations perform similarly; however, MBQI-Enum without the \( syms\_local \) option enabled shows significantly poorer performance.
In summary, our approach is highly effective on first-order SMT-LIB benchmarks, solving the highest number of benchmarks. With refinements tailored to specific logics, we suspect that its performance could be improved further.
Table 4.
MBQI-Enum configurations in SMT-LIB benchmarks
Dummy
6 Related Work
Mainstream approaches for quantifier instantiation in SMT are typically centered around E-matching [14]. Conflict-based instantiation [3, 11, 26] can improve the solver’s ability to answer “\(\mathcal {T}\)-unsatisfiable” by prioritizing instantiations that induce quantifier-free conflicts. As a whole, these techniques are generally incomplete and do not target specific background theories. For satisfiable instances, Ge and de Moura [9] introduced MBQI, which is complete for certain fragments. Finite model finding [25] is a variant of this technique that targets quantified formulas whose domains are small and finite. Approaches for quantified formulas in higher-order logic are discussed by Barbosa et al. [4], but, in contrast to this work, they are based on (higher-order) E-matching.
Other approaches for higher-order logic, notably in Vampire [6] and Zipperposition [28], rely on superposition. Vampire has been initially extended to handle higher-order reasoning using applicative first-order logic with combinators. Since this proved insufficient for problems requiring complex unifiers, its superposition calculus was later enhanced with native \(\lambda \)-abstractions and a depth-bounded version of higher-order unification [6]. As for Zipperposition, it also uses a superposition calculus that directly supports higher-order terms. It tackles the challenge of higher-order unification by using techniques such as pattern unification and heuristics to manage undecidability issues.
Certain background theories admit quantifier elimination, which can be handled using domain-specific instantiation strategies. Specifically, efficient and complete instantiation procedures have been developed for quantified linear arithmetic [24] and quantified bit vectors [19]. These techniques require specific knowledge of the background theory.
Other recent works on quantifier instantiation have pursued enumeration as a pragmatic means for discovering useful instantiations. Reynolds et al. [22] introduced enumerative instantiation as an alternative to MBQI, which primarily focused on first-order logic in the empty theory. This technique has been further studied in more recent works, where more advanced selection strategies are used for instantiations, including those based on machine learning [12, 13, 20].
The closest related works to ours are counterexample-guided model synthesis [21] and SyQI [18], which both focus on enumerative approaches for finding useful instantiations in rich background logics. The former was implemented in the Boolector [17] solver; it was limited to selected first-order theories and did not handle higher-order logic. The latter work can potentially be used for any theory but does not leverage MBQI for guiding the instantiation procedure. Our evaluation shows that our MBQI-Enum strategy generally outperforms SyQI overall.
7 Conclusion
We presented a new strategy, MBQI-Enum, for instantiating quantifiers in SMT solvers. It extends MBQI with the SyGuS enumerator, thereby augmenting the number of instantiations considered at every iteration. The main strength of our strategy is that it combines the fast model-finding capabilities of MBQI and the diversity of terms considered by SyQI. MBQI generates very specific instances; by resorting to a grammar, the terms in our instantiations are more abstract and therefore tend to lead to more useful instances. We implemented the strategy in cvc5 and found that it helps solve many first- and higher-order problems from SMT-LIB and TPTP for which cvc5 previously either timed out or gave up early.
Several aspects of our approach present opportunities for future work. First, we could improve performance by enhancing the quantifier-free solver to better integrate with our instantiation approach. Moreover, although our instantiation technique is designed to be generic, we could tailor it to individual SMT logics. Finally, we could develop more sophisticated instantiation strategies for higher-order logic. By designing methods that can more intelligently navigate the space of enumerated terms, we should be able to improve the solver’s ability to handle complex higher-order problems.
Acknowledgments
We thank the anonymous reviewers for their helpful comments. We also thank Pascal Fontaine and Mark Summerfield, who provided many comments on earlier drafts.
This research was cofunded by the European Union (ERC, Nekoka, 101083038). Views and opinions expressed are however those of the authors only and do not necessarily reflect those of the European Union or the European Research Council. Neither the European Union nor the granting authority can be held responsible for them.
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
