This work investigates the relation between model-based quantifier instantiation (MBQI) and enumerative instantiation (EI) in Satisfiability Modulo Theories (SMT). MBQI operates at the semantic level and guarantees to ifnd a counterexample to a given a model. However, it may lead to weak instantiations. In contrast, EI strives for completeness by systematically enumerating terms at the syntactic level. However, such terms may not be counter-examples. Here we investigate the relation between the two techniques and report on our initial experiments of the proposed algorithm that combines the two.
We assume a basic understanding of SMT [
We give a brief overview of MBQI. For simplicity of presentation, assume the input formula is given in the form where is ground, and the only free variables in each are ¯ . Let ℳ be a model of that can be expressed in the underlying theory, and let ℳ be the evaluation of in ℳ, meaning that each non-variable symbol in is replaced by its interpretation from ℳ. We then check the satisfiability of (1) ∧ ⋀︁ ∀¯ . ¬ ℳ, which is quantifier-free and contains only the free variables ¯ and interpreted functions and predicates. (We note this makes the satisfiablity check easier than checking (1), although for some theories it is still undecidable).
If the formulas ¬ ℳ for all are unsatisfiable , then the original formula (1) is true in ℳ and hence it is satisfiable. Further, we know that ℳ is a model of (1) and the algorithm terminates. If some ¬ ℳ is satisfiable , then the values ¯ of ¯ give a counterexample to the model ℳ. We select ground terms ¯ that have the values ¯ in ℳ, instantiate with ¯, and repeat the process with this instantiation, i.e., repeat with the following formula:
The key observation driving our work is that in arithmetic theories, MBQI has an infinite set of theory
constants, i.e. terms that denote value in a theory, that can possibly serve as a counter-example to
the current model. Instantiating by such arbitrary constants introduces new terms at the ground level.
On the other hand, reducing the number of new terms can have a significant positive impact on the
performance [
Although the original MBQI paper [
() = − 1000 * ( − 1), (0) = 1, (20) < 0 To reach a contradiction, the solver must consider the sequence of numbers from 0 to 20. However, both cvc5 and Z3, when running MBQI without E-matching, fail to conclude unsatisfiability.
Algorithm 1 shows the general outline, following the recipe for MBQI (Section 2). As customary, the
algorithm assumes that the formula is split into a set of quantified subformulas ( ∀¯ . ) and a ground
part , where are quantifier-free and contain only free variables in ¯ . Such form can be obtained
by clausification [
We note that we look for a new model of the ground part only after producing a counterexample for all quantified formulas for which there was one. The instantiation step and the calculation of relevant domains are explained further in Subsections 3.1 and 3.2, respectively.
We assume that constructing the formula ℳ is straightforward (line 9) as we work only with arithmetic sorts and thus each element from the model has a uniquely corresponding interpreted constant or function. This is strictly speaking not true because of the real domain, which is uncountable. However, in practice, solvers only produce “well-behaved models”.
This section focuses on how a counterexample is chosen in Algorithm 1 (step 11). Consider a quantified formula ∀ . [¯ ] and a model ℳ. The objective is to construct a counterexample from the relevant terms. There may be still too many of them, so we restrict those heuristically as follows.
For each variable in ¯ , first determine a total preference ordering on the terms in its relevant domain (, ) based on the current set of formulas. The ordering is a lexicographic ordering based on how frequently does a term appears in the formula, its depth, and in which iteration the term was added to the formula. We make the ordering total by appending a comparison based on the string Algorithm 1: MBQI with Relevant Domain
Input: A formula ∧ ⋀︀ ∀¯ . , where is ground and each has only the free variables ¯ Output: Satisfiability of the input formula 1 while true do 2 foreach and each variable in ¯ do 3 Construct the relevant domain (, ) // Section 3.2 is-sat ← true foreach [¯ ] do
Fix all non-variable symbols according to ℳ, obtaining ℳ[¯ ] if ¬ ℳ[¯ ] is satisfiable then
Using (, ), find ground terms ¯ s.t. ¬ ℳ[¯] is true ← ∧ [¯] is-sat ← false if is-sat then return satisfiable // Section 3.1 representation of the term. Let (, ) denote the first third of the terms in (, ) with respect to this ordering. We call these the preferred terms.
To look for a counterexample using the preferred terms, consider again the formula ℳ[¯ ], where all non-variable uninterpreted symbols in are interpreted by their interpretation in the model ℳ. Assume ¬ ℳ[¯ ] is satisfiable. Then, construct the following formula.
¬ ℳ[¯ ] ∧ ⋀︁
⋁︁ ∈ ¯ ∈ (,) = ℳ
As in MBQI, the formula looks for a counterexample to the model ℳ, but additionally, it restricts that the counterexample is equal to a vector of preferred terms (all this modulo what holds in the model ℳ). Such counterexample might not exist. Therefore, we proceed by gradually loosening the domains of variables from ¯ .
If the formula (2) is satisfiable, extract the equalities = ℳ that are satisfied in it and add the corresponding instantiation [¯ ↦→ ]¯ to the ground part, where each is the least term such that ℳ = ℳ. In case it is unsatisfiable, one of the new clauses must be unsatisfiable. We look for that clause and extend the set of available terms to all terms in the relevant domain of the corresponding variable. We do this by taking an arbitrary such clause from an unsatisfiable core of (2). This clause corresponds to some variable . Next, we permit to range over the whole set of relevant domain, not just the preferred terms. Let = {} and = ¯ ∖ . Next, construct the following formula. ¬ ℳ[¯ ] ∧ ⋀︁
⋁︁ ∈ ∈ (,) = ℳ ∧ ⋀︁ ⋁︁
= ℳ ∈ ∈ (,)
If formula (3) is satisfiable, we have a counterexample, as before. Otherwise, if (3) is unsatisfiable, continue by loosening the set of possible terms to the whole relevant domain for variables in the core, one by one. Efectively, moving variables from to in (3). It this process does not yield a counterexample, i.e. if the relevant domain is too restrictive, we gradually drop the clauses altogether, efectively allowing the underlying SMT solver to pick a theory constant (numeral). This is done analogously as before by taking the core of (3) and removing variables from , for some whose clause appears in the core. (2) (3)
The approach overall can be seen a mix of enumerative instantiation [
In arithmetic benchmarks, integers/reals are often used to model the set of some more specific objects, e.g. addresses on the heap. The objective of relevant domain is to identify such scenarios. For example, if we know that the function : Z → Z operates on addresses, we want to instantiate () only with terms that also represent addresses, even though ranges over all integers.
Therefore, for each quantified variable, we construct a set of candidate terms that are relevant for its
instantiation. We call such a set the relevant domain. To compute these sets, we use the relevant domain
approach based on [
We start by creating and initializing the following domains: • , = ∅ for each formula and each in ¯ , called the relevant domain for , • = ∅ for each uninterpreted function or predicate symbol , • , = ∅ for each uninterpreted symbol with arity ≥ 1 and each 1 ≤ ≤ , • = {} for each ground term occurring anywhere in the input formula.
Then we follow the rules shown below to merge these sets. We represent the merged set by a union containing the sets it was formed from, and we abuse to notation to refer to the union by any of its constituting sets. For example, the result of merging and ,1 is { , ,1}, and the result of a subsequent merge of and is { , ,1, }. To denote that 1 and 2 should be merged, we write merge(1, 2).
Although the sets , are initially empty, after applying the merging rules exhaustively, they may become members of a union containing some sets of ground terms . Let us define (, ) as { | is a ground term ∧ ∃. ∈ ∧ , ∈ } – i.e., the set of ground terms whose corresponding set belongs to the same union as , . We consider all the terms of (, ) to be relevant for instantiating the quantified variable in the subformula . If (, ) is empty, we add a default theory constant to it; in our case of arithmetic, this default is 0.
We now explain the merging rules. First, we define the function tls that assigns to each term2 its top level symbol: tls() = ⎧ ⎪ ⎪ ⎪⎪⎪ ⎪ ⎪ ⎪ ⎪⎨ if is a ground term if is a quantified variable in subformula if is (1, . . . , ), where is uninterpreted and is not ground ⎪tls(1) if is 1 * · · · * and is not ground ⎪ ⎪⎪⎪⎪tls(1) if is 1 + · · · + and is not ground ⎪ ⎪ ⎪⎩tls(1) if is 1 − 2 and is not ground Next, we define the function * that maps terms to their respective sets based on their top level symbols.
⎧⎪ if tls() is a ground term * () = ⎨, if tls() is a quantified variable in subformula
⎪⎩ if tls() is an uninterpreted function (predicate) symbol and is not ground 2In practice, SMT-LIB benchmarks typically do not include division operations, so we disregard such terms.
The rules merge the introduced sets based on where a term appears within the formula. Specifically, we distinguish between terms that occur as arguments of uninterpreted function symbols, arithmetic operations, or relational operators such as {=, ≤ , <}. We apply these rules based on term occurrences in the whole formula ∧ ⋀︀ ∀¯ . .
( (3, ) ≥ 4 + ()) ∧ (∀, . (, ) < + ()) ∧ (∀. () = ( + 2)) ⏟ ⏞ ⏟ ∀,.⏞1 ⏟ ∀. ⏞2 Because and () are summed in 1, we apply the operation merge(,1, ). Similarly, because is also the first argument of , we apply merge(,1, ,1). Using these two rules we get the union {,1, ,1, }. After performing all the possible merges, we get two disjoint unions of sets. {,1, ,1, , , 4, 3, (4+())}
{,1, ,2, ,1, , , ,2, 2} Since the first set contains both ,1 as well as 4, 3, and (4+()), we get that (,1) = {3, 4, 4 + ()}, and similarly (,1) = (,2) = {2, , }.
Note that we repeat the merging after each instantiation step (line 12 of Algorithm 1). This is because an instantiation may give us more information about the relevant domains. For example, instantiating = 2 in the last subformula yields a ground formula (2) = (4). After adding it to the ground part, we apply merge(,1, 4) and merge the two unions of sets into one.
We initially implemented the algorithm described in Section 3 as a standalone Python module using
PySMT [
Benchmarks. For preliminary evaluation, we used a subset of benchmarks from [
In this paper we gave preliminary results on MBQI combined with a custom relevant domain approach.
The approach resembles enumerative instantiation [
The current prototype shows promise since it allows solving small but dificult problems. We plan to investigate improvements to the implementation that would enable solving also larger problem instances and integrating it into an existing solver.
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.
The authors used ChatGPT and Grammarly for grammar and spell-checking. After using these tools, the authors reviewed and edited content as needed and take full responsibility for the publication’s content.