Revisiting Enumerative Instantiation

Revisiting Enumerative Instantiation#

Reference:

  • Andrew Reynolds, Haniel Barbosa and Pascal Fontaine, “Revisiting Enumerative Instantiation”, TACAS 2018, LNCS 10806, pp. 112–131, [27]. Open access; the PDF is not stored in the repository.

Read for Primo’s quantifier component: Sections 2, 3, 4 and 4.1, including Figure 2. Section 5 (experiments) was not used.

Status: implemented (M4 of Quantifiers: parsing and term representation) and evaluated on the SMT-LIB UF division. This note is the paper checklist written before the instantiation code. It records what the paper says and which subset Primo implements.

Section 2: the instantiation loop#

The ground solver abstracts “all atoms and quantified formulas and treat[s] them as if they were propositional variables”. It returns an assignment E ∪ Q: E is a set of ground literals and Q a set of quantified formulas that together propositionally entail the input.

The instantiation module adds lemmas ∀x̄. ϕ ⇒ ϕσ, where σ maps the variables of ϕ to ground terms. The loop ends when the added instances make the ground problem unsatisfiable.

The paper assumes every quantified formula is ∀x̄. ϕ with ϕ quantifier-free, “achieved by prenex form transformation and Skolemization”.

Section 3: which terms suffice#

  • Theorem 1. E ∪ Q (ground literals and universally quantified clauses, with at least one term of each sort) is unsatisfiable iff there is a series of finite instance sets Qi with E ∪ Q1 ∪ … ∪ Qn unsatisfiable, where each Qi+1 uses only substitutions with ran(σ) ⊆ T(E ∪ Q1 ∪ … ∪ Qi). Only terms already present, or generated by earlier instances, are needed, not the whole Herbrand universe.

  • Scope of the theorem. It holds in pure first-order logic with equality, and in theories that preserve compactness. For EPR formulas the term sets are finite, so the enumeration always terminates.

  • Lemma 1. An infinite series of satisfiable ground assignments Ei, where Qi instantiates Q with terms from T(Ei) and Ei+1 |= Ei ∪ Qi, implies that E ∪ Q is satisfiable.

  • Corollary 1 (model soundness). If the module cannot generate an instance that E does not already entail, using terms T(E), the input is satisfiable.

  • Corollary 2 (refutational completeness). On an unsatisfiable input, the loop terminates provided instance generation is fair.

Section 4 and Figure 2: strategy u#

Definition 1: an instantiation strategy maps a T-satisfiable set of ground literals E and a quantified formula ∀x̄. ϕ to a set of substitutions with domain x̄.

Figure 2 lists four strategies: conflict-based (c), E-matching (e), model-based (m) and enumerative (u). MBQI is due to Ge and de Moura (CAV 2009, §6) [18]; this paper supplies the comparison with enumerative instantiation.

Enumerative instantiation u(E, ∀x̄. ϕ):

  1. choose an ordering ≺ on tuples of quantifier-free terms;

  2. return {x̄ ↦ t̄}, where t̄ is a minimal tuple from T(E) such that E ⊭ ϕ{x̄ ↦ t̄}, or ∅ if none exists.

The paper’s comparison with model-based instantiation: u considers every substitution whose instance E does not entail, and introduces predicates on fewer new terms (“minimally diverse”). Model-based instantiation suits satisfiable problems better (Example 3).

Section 4.1: implementation details in CVC4#

  • Tuple ordering. (t1…tn) ≺ (s1…sn) if max ti ≺ max si, or the maxima are equal and the tuples are lexicographically ordered. Tuples involving a later term come only after every combination of earlier terms. The underlying term order is dynamic: a finite list t1 ≺ … ≺ tn grows by a term that E does not entail equal to any ti, once all combinations are entailed. “The particular choice of t beyond this criteria is arbitrary.”

  • Entailment checks. A cache of already returned instances, plus an incomplete fast check. It uses congruence classes over T(E), a per-function term index, and iterated rewriting of a literal to ⊤, extended to Boolean structure.

  • Restricting the enumeration space. Relevant domains (Ge and de Moura), or sort inference, shrink the candidate terms.

  • Compound strategies. Priority s1; s2 and interleaving s1 + s2. The paper reports c;e;u and c;e+u as most effective for unsatisfiable problems.

Primo mapping#

Equality and completeness review, 2026-09-30. Reread §3’s completeness statement and §4.1’s term-ordering and entailment rules. The equality used in term selection is entailment by the current ground assignment \(E\). Two terms merely receiving the same value in a candidate model need not satisfy that condition. Substitutivity justifies replacing an instance by an equal tuple within a fixed context; a procedure retaining skipped work across changing contexts also needs a coverage and fairness argument. The open investigation in docs-next/leads/quantifier-instantiation.md records these obligations. No current cvc5 implementation audit or completeness counterexample is claimed.

Also reread §4, Figure 2 and Example 2: a non-entailed instance need not be false in the chosen candidate model. The example shows how instances already satisfied by that model can still contribute to a short refutation together with another instance. An enumerator can still filter its candidates by their truth in the current model without becoming MBQI: enumeration generates the tuples, while the model test controls emission. The same open lead connects this proposed filter to equality-based enumeration and fail masks, with completeness and revisitation obligations for changing models.

Paper element

Primo owner

propositional abstraction of quantified formulas

BooleanClausifier theory atoms of kind Forall/Exists

instantiation module

QuantifierComponent (src/theory/quantifiers/), a TheoryComponent

adding ∀x̄. ϕ ⇒ ϕσ

lemma queue drained by solve_component_recipe at its atom-growth boundary

ϕσ

core::instantiate on de Bruijn indices (src/core/binders.*)

T(E)

per-sort term pool

ordering ≺

max-then-lexicographic tuple order over the pool’s append-only list

Implemented subset and deviations#

  • Strategy. Strategy u alone. No c or e, and so no compound strategy.

  • Skolemization. No prenex or Skolem-normal-form preprocessing. A quantifier atom assigned so that it needs Skolemization (a true ∃, or a false ∀) gets one Skolem lemma with fresh constants. Nested quantifiers in an instance become new quantifier atoms of the lemma, handled the same way.

  • Term pool. Ground subterms of the input assertions and of every added lemma, a superset of T(E). Theorem 1’s term set T(E ∪ Q1 ∪ … ∪ Qi) justifies this for refutation. Lemma 1 and Corollary 1 are stated for T(Ei), so no model-soundness claim is made from this pool.

  • Term order. Order of first appearance, which the paper allows (“arbitrary”). Entailed-equal terms are not merged.

  • Entailment. No congruence-based entailment check. Two caches replace it: instances as instantiated, and instances after a shallow equivalence-preserving normalization (theory::InstanceSimplifier). Instances true outright are dropped. More instances may be generated than the paper’s filter allows, but each is still a valid consequence.

  • Answers. unsat from the ground solver. sat only when every assigned quantifier atom is covered by a Skolem lemma, so that no universal remains. Otherwise unknown: without the entailment check, Corollary 1 is not available.

  • Empty sorts and Bool. Theorem 1 assumes a term of every sort. A sort with no ground term gets one fresh constant. Bool-sorted variables range over true and false only.

  • Rounds. At each complete assignment, at most --quantifier-instances-per-round new instances are queued, shared evenly across the universally behaving atoms, starting from a rotating one. Once the round has a lemma, an atom whose scan visits --quantifier-stall-tuples tuples without a new one stops; the round keeps its enumeration state. One solve tries at most --quantifier-max-instances distinct instances, then answers unknown with reason resource-limit.

  • Not implemented. Relevant domains, sort inference, and model export.

Tests derived from the paper#

  • Example 1 and Example 2 shapes: the instance on the minimal term refutes.

  • Example 3 shape: repeated enumeration over three terms ends in unknown, not sat.

  • Fairness of the tuple order: a term appended later is used only after all combinations of earlier terms.

  • Theorem 1: a refutation needing a term that appears only in an earlier instance.