This paper proposes a technique to limit the number of possible terms to be considered in quantifier instantiation. One of the major hurdles that SMT solvers face when dealing with quantifiers is that there are simply too many terms to instantiate with. So even if the right set of terms is available to the solver, meaning they appear in the formula, the solver might not have enough resources to come upon the right combination. This motivates the technique presented in this paper, which instantiates only by a certain type of terms, called discriminating terms. The paper introduces a class of formulas, where the proposed technique has a considerable impact.
Quantifiers represent one of the major challenges for contemporary SMT solvers and since typically they lead to undecidability or extreme computational complexity, they are likely to remain a challenge for times to come.
Most commonly, the general techniques for dealing with quantifiers gradually instantiate the
quantified part of the formula with ground terms until the resulting ground formula becomes
unsatisfiable. The terms to be used in instantiations may be chosen either by syntactic properties
(E-matching [
This is where this paper comes in. We propose a technique to limit the set of terms to enumerate. Roughly speaking, in the context of first order logic with equality, a term is labeled as discriminating if it participates in a disequality.
We have modified the enumeration instantiation algorithm in CVC4 [
Kaminski and Smolka [
∀. = ∨ = ∨ = stating there are at most two elements and making the conclusion ( ( ())) = (). A formal proof would proceed by equational reasoning after instantiating the quantifiers using the subterms of the conjecture: , (), ( ()) and ( ( ())). This problem can be made slightly more dificult by including unary functions 0, . . . , − 1 and writing the conclusion as ( ( (0(· · · − 1() · · · )))) = (0(· · · − 1() · · · )). The modified problem has + 4 subterms instead of only 4. The subterms of the form (· · · − 1() · · · ) with > 0 are red herrings. The four subterms (0(· · · − 1() · · · )) with ∈ {0, 1, 2, 3} are suficient to use as instantiations to complete the proof.
The problems can also be made more dificult in a diferent way. Following a proof from [
To construct the family of formulae in question, define atmost to be the first-order formula ∀0 · · · .
⋁︁ 0≤ <≤ = and let kam be the first-order formula
atmost ∧ lcm({2,...,})+− 1(0(· · · − 1() · · · )) ̸= − 1(0(· · · − 1() · · · )).
2.1. Unsatisfiability of kam
Following the proof (and terminology) of Theorem 7 in [
lcm({2,...,})+− 1() = − 1()
The intuition for the equality is as follows. The sequence , (), . . . , (), . . . must eventually repeat. Both sides of the equation will be in the part that repeats and the length of the repeating part will be a number at most . Since this length divides lcm({2, . . . , }) we will be able to conclude
lcm({2,...,})( − 1()) = − 1() Let us now expand this idea more carefully.
Consider an arbitrary interpretation of the function and the constant assuming that
the universe has at most elements. For the purpose of this subsection, we abuse notation
by writing (· · · ) for the value of under such interpretation and write for the value of
under the interpretation. By the pigeonhole principle there must exist 1 and 2 such that
0 ≤ 2 < 1 ≤ such that 1 () = 2 (). Let 1 and 2 be the least numbers with this
property. Following [
lcm({2,...,})( − 1()) = − 1() as desired.
The tableau calculus from [
The change of setting from the tableau calculus of [
∀. = ∨ = ∨ =
and one disequation ( ( ())) ̸= (). There are only two discriminating terms: 3() and
(). Instantiating , and with these two terms will always lead to at least two of , and
being the same term so that the resulting disjunction will always have a literal that is trivial by
reflexivity. In the calculus of [
One option would be to extend CVC4 to behave in ways that simulate the additional rules
of [
300 instances 400 500 clause corresponding to 3() = () ∨ 2() ̸= . Further tableau rules that would need to have a similar counterpart are the mating and confrontation rules.
We have chosen a simpler, heuristic approach without attempting to maintain completeness. However, a heuristic that restricts to discriminating terms without simulating the tableau rules would be far too restrictive. An intermediate heuristic is to restrict to terms that would be discriminating if the decomposition rule were included. We call these quasidiscriminating terms.
As a technical definition, we say a pair (, ) is a discriminating pair if the literal = is assigned false by the propositional model. We recursively define quasidiscriminating pairs (, ) as follows: Every discriminating pair is a quasidiscriminating pair. If ( (1, . . . , ), (1, . . . , )) is a quasidiscriminating pair, then (, ) is a quasidiscriminating pair for each ∈ {1, . . . , } where and are not the same term. A term is quasidiscriminating if there is some such that (, ) or (, ) is a quasidiscriminating pair.
We have modified the enumeration instantiation algorithm in CVC4 [
The problems used for evaluation are the formulas kam as defined above. The parameters were chosen as follows. The parameter ranges between 4..10 and the value of ranges between 0..99 for ∈ 4..8 and it ranges between 0..9 for ∈ 9..10. Recall that the parameter represents the domain size and the number of the “dummy” terms .
For the comparison we considered the default version of CVC4, CVC4 run only in the enumeration mode, and Z3. Figure 1 shows a cactus plot for the experiment results under 5-minute timeout (300s). Table 1 breaks down the number of solved instances by the domain size, i.e. by the parameter . domain 4 5 6 7 8 9 10 Total (520)
Our strategy using discriminating terms solved all the considered benchmarks very quickly
except for the largest ones. CVC4’s enumerative is also performing quite well but the time starts
to increase much more quickly and eventually it times out on the largest problems. The default
version of CVC4 performs rather poorly; our explanation for this is that the conflict-based
instantiation [
This paper proposes a way to restrict possible candidates term for quantifier instantiation by looking at syntactic properties of the given formula. In particular, we consider only terms that participate in a disequality. We construct a family of formulas where this technique has demonstrably the best results.
The presented techniques opens a number of avenues for future work. Since the presented technique disregards theories, a natural generalization would be to include theory-specific predicates, other than just disequality. For instance, in the context of arithmetic strict comparisons (<) imply disequality and therefore could be used in a similar fashion. While the technique is clearly performing well on the constructed family of formulas, as of now we don’t have any dividends that is helpful on general formulas. We conjecture that this might happen in problems with many function nesting but also, careful integration with other techniques will be needed. A natural next step to take would be to run the modified CVC4 over the problem sets in the SMT-LIB to obtain data for how often the quasi-discriminating terms technique is helpful and how often it is not.
The family of formulas proposed here is interesting on its own, if only because they are easy to understand and yet present a challenge to existing SMT solvers and first-order automated theorem provers. In general, it is unclear whether it is better to instantiate with deeper terms or with more shallow terms. In the provided family, the outermost terms are actually the right ones and the inner ones are “red herrings.” But one can envision scenarios where the opposite is true. So the question is, how to distinguish scenarios like these. The results were supported by the Ministry of Education, Youth and Sports within the dedicated program ERC CZ under the project POSTMAN no. LL1902. This scientific 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.