Amine Asselah
email: amine.asselah@u-pec.fr

Bruno Schapira
email: bruno.schapira@univ-amu.fr

On the nature of the Swiss cheese in dimension 3

Keywords: Random Walk, Large Deviations, Range. MSC 2010 subject classifications. Primary 60F10, 60G50

We study scenarii linked with the Swiss cheese picture in dimension three obtained when two random walks are forced to meet often, or when one random walk is forced to squeeze its range. In the case of two random walks, we show that they most likely meet in a region of optimal density. In the case of one random walk, we show that a small range is reached by a strategy uniform in time. Both results rely on an original inequality estimating the cost of visiting sparse sites, and in the case of one random walk on the precise Large Deviation Principle of van den Berg, Bolthausen and den Hollander [BBH01], including their sharp estimates of the rate functions in the neighborhood of the origin.

1 Introduction.

In this note, we are concerned with describing the geometry of the range of a random walk on Z 3 , when forced to having a small volume, deviating from its mean by a small fraction of it, or to intersecting often the range of another independent random walk. These issues were raised in two landmark papers of van den Berg, Bolthausen, and den Hollander (referred to as BBH in the sequel) written two decades ago [START_REF] Van Den Berg | Moderate deviations for the volume of the Wiener sausage[END_REF] [START_REF] Van Den Berg | On the volume of the intersection of two Wiener sausages[END_REF]. Both papers dealt with the continuous counterpart of the range of a random walk, the Wiener sausage. They showed a Large Deviation Principle, in two related contexts: (i) in [START_REF] Van Den Berg | Moderate deviations for the volume of the Wiener sausage[END_REF] for the downward deviation of the volume of the sausage, (ii) in [START_REF] Van Den Berg | On the volume of the intersection of two Wiener sausages[END_REF] for the upward deviation of the volume of the intersection of two independent sausages. They also expressed the rate function with a variational formula. Their sharp asymptotics are followed with a heuristic description of the optimal scenario dubbed the Swiss cheese picture where, in case (i), the Wiener sausage covers only part of the space leaving random holes whose sizes are of order 1 and whose density varies on space scale t 1/d , and in case (ii) both Wiener sausages form apparently independent Swiss cheeses. However, they acknowledge that to show that conditioned on the deviation, the sausages actually follow the Swiss cheese strategy requires substantial extra work.

Remarkably the Swiss cheese heuristic also highlight a crucial difference between dimension 3 and dimensions 5 and higher. Indeed, in dimension three the typical scenario is time homogeneous, in the sense that the Wiener sausage considered up to time t, would spend all its time localized in a region of typical scale (t/ε) 1/3 , filling a fraction of order ε of every volume element, when the deviation of the volume occurs by a fraction ε of the mean. On the other hand in dimension 5 and higher the typical scenario would be time-inhomogeneous: the Wiener sausage would localize in a smaller region of space with scale of order (εt) 1/d , only during a fraction ε of its time, and therefore would produce a localization region where the density is of order one, no matter how small ε is.

Recently Sznitman [S17] suggested that the Swiss cheese could be described in terms of so-called tilted Random Interlacements. In the same time, in [START_REF] Asselah | Moderate deviations for the range of a random walk: path concentration[END_REF] we obtained a first result in the discrete setting, which expressed the folding of the range of a random walk in terms of its capacity. More precisely we showed that a positive fraction of the path, considered up to some time n, was spent in a subset having a volume of order n and a capacity of order n 1-2/d , that is to say of the same order as the capacity of a ball with volume n.

In this note, we present a simple and powerful estimate on the probability a random walk visits sites which are far from each others, see Proposition 1.3 below. We then deduce two applications in dimension three that we state vaguely as follows.

• One random walk, when forced to have a small range, folds in a time-homogeneous way.

• Two random walks, when forced to meet often, do so in a region of optimal density.

To state our results more precisely, we introduce some notation. We denote by {S n } n≥0 the simple random walk on Z d (in most of the paper d = 3), and by R(I) := {S n } n∈I , its range in a time window I ⊂ N, which we simply write as R n , when I is the interval Q(x, r), which we simply write V n (ρ, r), when I = I n . Thus, R(I) ∩ V(ρ, r, I) is the set of visited sites around which the range has density, on a scale r, above ρ in the time window I.

I n := {0, . . . , n}. We let Q(x, r) := (x + [-r, r[ d ) ∩ Z d ,
Our first result concerns the problem of forcing a single random walk having a small range. For ε ∈ (0, 1), we denote by Q ε n the law of the random walk conditionally on the event

{|R n |-E[|R n |] ≤ -εn}.
Theorem 1.1. Assume d = 3. There exist positive constants β, K 0 and ε 0 , such that for any ε ∈ (0, ε 0 ), and any

1 ≤ r ≤ ε 5/6 n 1/3 , lim n→∞ Q ε n |R(I) ∩ R(I c ) ∩ V n (βε, r)| ≥ ε 8 |I|, for all intervals I ⊆ I n , with |I| = K 0 εn = 1.
This result expresses the fact that under Q ε n , in any time interval of length of order εn, the random walk intersects the other part of its range a fraction ε of its time, which is in agreement with the intuitive idea that, if during some time interval, the walk moves in a region with density of visited sites of order ε, it should intersect it a fraction ε of its time. Note that it brings complementary information to the results obtained in [START_REF] Asselah | Moderate deviations for the range of a random walk: path concentration[END_REF], where it was shown that for some positive constants α, β, C, and ε 0 ∈ (0, 1), for any ε ∈ (0, ε 0 ), and any Cε -5/9 n 2/9 log n ≤ r ≤ 1

C √ εn 1/3 , lim n→∞ Q ε n ∃V ⊆ V n (βε, r) : |V ∩ R n | ≥ αn, and cap(V) ≤ C( n ε ) 1/3 = 1, (1.1)
with cap(Λ) being the capacity of a finite set Λ ⊂ Z d (see for instance [START_REF] Lawler | Random walk: a modern introduction[END_REF] for a definition). This is in a sense stronger than the result of Theorem 1.1, which only gives (by summation over disjoint intervals) that with high Q ε n -probability, |R n ∩ V n (βε, r)| ≥ 1 8 εn. On the other hand (1.1) says nothing on the distribution of the times when the random walk visits the sets V n (βε, r), while Theorem 1.1 shows that they are in a sense uniformly distributed. Both results are proved using different techniques: while (1.1) was obtained by using only elementary arguments, Theorem 1.1 relies on the sharp and intricate results of [START_REF] Van Den Berg | Moderate deviations for the volume of the Wiener sausage[END_REF] (which have been obtained in the discrete setting by Phetpradap in his thesis [START_REF] Phetpradap | Intersections of Random Walks[END_REF]).

Our second result concerns the problem of intersection of two independent ranges. For n ≥ 1, and ρ ∈ (0, 1), we denote by Q ρ n the law of two independent ranges R n and R n , conditionally on the event

{|R n ∩ R n | > ρn}.
Theorem 1.2. Assume d = 3. There exist positive constants c and κ, such that for any n ≥ 1, ρ ∈ (0, 1), δ ∈ (0, 1), and r ≤ cδ 2/3 (ρn

) 1/3 , lim n→∞ Q ρ n |R n ∩ R n ∩ V n (δρ, r)| > (1 -κδ) ρn = 1. (1.2)
Recall that the heuristic picture is that as ρ goes to zero, under the law Q ρ n , both random walks should localize in a region of typical diameter (n/ρ) 1/3 , during their whole time-period. Thus, the occupation density in the localization region is expected to be of order ρ, and (1.2) provides a precise statement of this picture. Let us stress that unlike Theorem 1.1, the proof of this second result does not rely on BBH's fine Large Deviation Principle, but only on relatively soft arguments.

Our main technical tool for proving both Theorems 1.1 and 1.2 is the following proposition, which allows us to estimate visits in a region of low density at a given space scale r. Proposition 1.3. Assume that Λ is a subset of Z d with the following property. For some ρ ∈ (0, 1), and r ≥ 1,

|Λ ∩ Q(x, r)| ≤ ρ • |Q(x, r)|, for all x ∈ 2rZ d . (1.3)
There is a constant κ > 1 independent of r, ρ, and Λ, such that for any n ≥ ρ 2 d -1 r 2 , and t ≥ κρ n,

P [|R n ∩ Λ| ≥ t] ≤ exp -ρ 1-2 d t 2r 2 ).
(1.4) Note that in (1.4) the smaller is the scale the smaller is the probability. Note also that this result holds in any dimension d ≥ 3. Now some remarks on the limitation of our results are in order. Let us concentrate on Theorem 1.1 which is our main result. First the size of the time-window is constrained by the degree of precision in BBH's asymptotics. The fact that one can only consider windows of size order εn, and not say order ε K n, for some K > 1, is related to the asymptotic of the rate function in the neighborhood of the origin, see (2.3) below. From [START_REF] Van Den Berg | Moderate deviations for the volume of the Wiener sausage[END_REF] one knows the first order term in dimension 3. However, pushing further the precision of this asymptotic would allow to consider higher exponents K. On the other hand it would be even more interesting to allow time windows of smaller size, say of polynomial order n κ , with κ ∈ (2/3, 1). Going below the exponent 2/3 does not seem reasonable, as the natural belief is that strands of the path of length n 2/3 should typically move freely, and might visit from time to time regions with very low occupation density. Thus, we believe that a result in the same vein as Theorem 1.1 should hold for exponents κ ∈ (2/3, 1). One would need however a much better understanding of the speed of convergence in the Large Deviation Principle, see (2.2) below.

Similarly, one could ask whether our proof could show a kind of time inhomogeneity in dimension 5 and higher. However, a problem for this is the following. Given two small time windows (say of order εn), one would like to argue that the walk cannot visit regions with high occupation density in both, unless these two time windows were adjacent. However, even if they are not, the cost for the walk to come back at the origin at the beginning of each of them is only polynomially small, which is almost invisible when compared to the (stretched) exponentially small cost of the large deviations. Therefore obtaining such result seems out of reach at the moment.

Let us sketch the proof of Theorem 1.1. The first step, which reveals also the link between [START_REF] Van Den Berg | Moderate deviations for the volume of the Wiener sausage[END_REF] and [START_REF] Van Den Berg | On the volume of the intersection of two Wiener sausages[END_REF] is to show that

{|R n | -E[|R n |] < -εn} implies large mutual intersections {|R(I) ∩ R(I c
)| > βε|I|} for some constant β as soon as the interval I ⊂ [0, n] is large enough. This requires to show a LDP on the same precision as [START_REF] Van Den Berg | Moderate deviations for the volume of the Wiener sausage[END_REF] for R(I c ), where I c typically consists of two subintervals: this step presents some subtleties, which we deal with by wrapping parts of the two trajectories, and use that the intersection essentially increases under such operation. Then one falls back on an estimate similar to Theorem 1.2.

The rest of the paper is organized as follows. In Section 2 we gather useful results on the range: BBH's results, as well as the upward large deviation principle of Hamana and Kesten [START_REF] Hamana | A large-deviation result for the range of random walk and for the Wiener sausage[END_REF], and estimates on probability that the walk covers a fixed region with low density for a long time. We then prove Proposition 1.3 and Theorem 1.2. In Section 3 we prove an extension of BBH's estimate when one considers two independent walks starting from different positions. The proof of Theorem 1.1 is concluded in Section 4.

Visiting Sparse Regions

In this section, we prove our main tool, Proposition 1.3, and then Theorem 1.2, after we recall well known results.

Preliminaries

Dvoretzky and Erdós [START_REF] Dvoretzky | Some problems on random walk in space[END_REF] established that there exists a constant κ d > 0, such that almost surely and in L 1 ,

lim n→∞ |R n | n = κ d .
In addition, one has

|E[|R n |] -κ d n| =    O( √ n) when d = 3 O(log n) when d = 4 O(1)
when d ≥ 5.

(2.1)

Precise asymptotic of the variance and a Central Limit Theorem are obtained by Jain and Orey [START_REF] Jain | On the range of random walk[END_REF] in dimensions d ≥ 5, and by Jain and Pruitt [START_REF] Jain | The range of transient random walk[END_REF] in dimensions d ≥ 3.

The analogue of the LDP of [START_REF] Van Den Berg | Moderate deviations for the volume of the Wiener sausage[END_REF] has been established in the discrete setting by Phetpradap in his thesis [START_REF] Phetpradap | Intersections of Random Walks[END_REF], and reads as follows: there exists a function I d , such that for any ε ∈ (0, κ d ),

lim n→∞ 1 n 1-2 d log P [|R n | -E[|R n |] ≤ -εn] = -I d (ε). (2.2)
Moreover, there exist positive constants C, µ d and ν d , such that for ε ∈ (0, ν d ),

µ 3 ε 2/3 µ 4 √ ε ≤ I d (ε) ≤ µ 3 ε 2/3 (1 + Cε) when d = 3 µ 4 √ ε(1 + Cε 1/3 ) when d = 4, (2.3) and if d ≥ 5, I d (ε) = µ d ε 1-2 d .
These results were first obtained in [START_REF] Van Den Berg | Moderate deviations for the volume of the Wiener sausage[END_REF] for the Wiener sausage: the lower bounds are given by their Theorem 4 (ii) and Theorem 5 (iii), respectively for dimension 3, 4, and for dimension 5 and higher (note that their constants µ d differs from ours by a universal constant, see also [START_REF] Phetpradap | Intersections of Random Walks[END_REF] for details). The upper bound in dimension 5 and higher is also provided by their Theorem 5 (iii). The upper bound in dimension three and four is obtained in the course of the proof of Theorem 4 (ii), see their equations (5.73), (5.81) and (5.82). Note that, as they use Donsker-Varadhan's large deviation theory, their rate functions I d are given by variational formulas. Now a basic fact we need is an estimate of the variance of |R n ∩ Λ| uniform on Λ.

Lemma 2.1. There exists a constant C > 0, such that for any positive integer n, and

Λ ⊂ Z d , Var(|R n ∩ Λ|) ≤ Cn • log 2 n.
(2.4)

It is important to stress that C is independent of Λ and n. This lemma is obtained using the same argument as in [LG86, Lemma 6.2].

Upward large deviations are obtained by Hamana and Kesten [START_REF] Hamana | A large-deviation result for the range of random walk and for the Wiener sausage[END_REF]. Their result implies that there exists a positive function J d , such that for ε ∈ (0, 1 -κ d ),

lim n→∞ 1 n log P (|R n | -E[|R n |] ≥ εn) = -J d (ε). (2.5)
Finally, an elementary fact we shall need is the following (see for instance Lemma 2.2 in [START_REF] Asselah | Moderate deviations for the range of a random walk: path concentration[END_REF]).

Lemma 2.2. There exists a constant C > 0, such that for any ρ ∈ (0, 1), r ≥ 1, and Λ ⊂ Z d , satisfying (1.3) one has for all n ≥ 1,

E[|R n ∩ Λ|] ≤ C(ρ 2/d r 2 + ρn).

Proof of Proposition 1.3

Let T := r 2 /ρ 1-2 d , and R j := |R[jT, jT + T ] ∩ Λ|. Note first that

|R n ∩ Λ| ≤ n/T +1 j=0 R j .
(2.6) Now, consider the martingale (M ) ≥0 , defined by

M := j=0 R j -E [R j | F jT ] .
By choosing κ ≥ 8C, with C as in Lemma 2.2, we deduce from this Lemma, that for any t ≥ κρ n,

and ρn ≥ ρ 2/d r 2 that n/T +1 j=0 E [R j | F jT ] ≤ t/2.
Hence, using (2.6) we get

P [|R n ∩ Λ| ≥ t] ≤ P M k/T +1 ≥ t/2 .
Moreover, the increments of the martingale (M ) ≥0 are bounded by T , and by (2.4) their conditional variance is O(T log 2 T ) (uniformly in Λ). Thus, McDiarmid's concentration inequality (see Theorem 6.1 in [START_REF] Chung | Concentration inequalities and martingale inequalities: a survey[END_REF]), gives

P M n/T +1 ≥ t/2 ≤ exp(- t 2T
), by taking larger κ if necessary. This proves the desired result.

Proof of Theorem 1.2

Fix ρ ∈ (0, 1) and δ ∈ (0, 1). We proved in [AS17] a lower bound for visiting a set of density ρ in dimension three: Proposition 4.1 of [START_REF] Asselah | Moderate deviations for the range of a random walk: path concentration[END_REF] indeed establishes that for some positive constants c and c , P |R n ∩ Λ| > ρ|Λ| ≥ exp(-c ρ 2/3 n 1/3 ), for any Λ ⊂ B(0, c(n/ρ) 1/3 ).

By forcing one of the two walks to stay inside the desired ball, we deduced that for some positive constant c 0 we have the following rough bound on the intersection of two random walks:

P |R n ∩ R n | > ρn ≥ exp(-c 0 ρ 2/3 n 1/3 ). (2.7)
Now, the (random) set R n ∩ V c n (δρ, r) satisfies the hypothesis (1.3) of Proposition 1.3 with density δρ, thus giving with the constant κ of this proposition

P |R n ∩ R n ∩ V c n (δρ, r)| > κ δρ n ≤ exp -(δρ) 1/3 κ δρ n 2r 2 .
The proof follows after we observe that this probability becomes negligible, compared to the one in (2.7), if we choose r, satisfying r ≤ κ 2c 0 1/2 δ 2/3 (ρn) 1/3 .

Large deviation estimate for two random walks

In this section we prove an extension of (2.2), when one considers two independent random walks starting from (possibly) different positions. We show that the upper bound in (2.2) still holds, up to a negligible factor, uniformly over all possible starting positions. While this result could presumably be also obtained by following carefully the proof of [START_REF] Van Den Berg | Moderate deviations for the volume of the Wiener sausage[END_REF], we have preferred to follow here an alternative way and deduce it directly from (2.2), using no heavy machinery. We state the result for dimension three only, since this is the case of interest for us here, but note that a similar result could be proved in any dimension d ≥ 3, using exactly the same proof.

For x ∈ Z 3 , we denote by P 0,x the law of two independent random walks S and S starting respectively from the origin and x. We write R and R for their ranges. Furthermore, for an integrable random variable X, we set X := X -E[X], and for x ∈ Z 3 , we denote by x its Euclidean norm.

Proposition 3.1. Assume that d = 3. There exists ε 0 > 0, such that for any ε ∈ (0, ε 0 ), for n large enough, and k ≤ n,

sup x ≤n 2/3 P 0,x |R k ∪ R n-k | ≤ -εn ≤ exp -I 3 ( ε 1 + ε 2 )n 1/3 .
Proof. Set m := ε 2 n . First using (2.2), we know that

lim n→∞ 1 n 1/3 log P |R n+m | ≤ -ε(1 -ε 3 )n = -I 3 ( ε(1 -ε 3 ) 1 + ε 2 )(1 + ε 2 ) 1/3 .
Now consider x, with x ≤ ε 5/2 n 2/3 , and k ≤ n. Note that by (2.1), we get for ε > 0,

|R[0, n + m]| ≤ |R[0, k] ∪ R[k + m, n + m]| + |R[k, k + m] + O( √ n).
Therefore, at least for n large enough,

P |R n+m | ≤ -ε(1 -ε 3 )n ≥ P |R k ∪ R[k + m, n + m]| ≤ -εn, |R[k, k + m]| ≤ ε 5 n, S k+m -S k = x ≥ P 0,x |R k ∪ R n-k | ≤ -εn • P |R m | ≤ ε 5 n, S m = x ,
using the Markov property and reversibility of the random walk for the last inequality. Now using Hamana and Kesten bound (2.5), the local central limit theorem (see Theorem 2.3.11 in [START_REF] Lawler | Random walk: a modern introduction[END_REF]), and that x ≤ ε 5/2 n 2/3 , we get that for some constant c > 0 (independent of x), and for all n large enough,

P |R m | ≤ ε 5 n, S m = x ≥ P(S m = x) -P(|R m | ≥ ε 5 n) ≥ exp(-cε 3 n 1/3 ) -exp(-J d (ε 3 )(1 -ε)ε 2 n) ≥ 1 2 exp(-cε 3 n 1/3 ).
Moreover, it follows from (2.3), that for ε small enough

I 3 ( ε(1 -ε 3 ) 1 + ε 2 )(1 + ε 2 ) 1/3 -cε 3 ≥ I 3 ( ε 1 + ε 2 )(1 + 1 4 ε 2 ).
Therefore, for ε small enough, and then for all n large enough, sup

x ≤ε 5/2 n 2/3 P 0,x |R k ∪ R n-k | ≤ -εn ≤ exp -I 3 ( ε 1 + ε 2 )(1 + 1 5 ε 2 )n 1/3 . (3.1)
It remains to consider x satisfying ε 5/2 n 2/3 ≤ x ≤ n 2/3 . Our strategy is to show that there exists a constant ρ ∈ (0, 1), such that for any such x, the probability of the event

A := {|R k ∪ R n-k | ≤ -εn}, (3.2)
under P 0,x is bounded by the probability of the same event under P 0,x , with x satisfying x ≤ ρ x , up to some negligible error term. Applying this estimate at most order log(1/ε) times, and using (3.1), the result obtains.

Fix x such that ε 5/2 n 2/3 ≤ x ≤ n 2/3 , and assume, without loss of generality, that its largest coordinate in absolute value is the first one, say x 1 , and that it is positive. In this case x ≥ x 1 ≥ x / √ 3. Recall next that we consider two random walks S and S, one starting from the origin and running up to time k, and the other one starting from x and running up to time n -k. For x 1 /3 ≤ y ≤ 2x 1 /3, consider the hyperplane H y of vertices having first coordinate equal to y. Denote by N y the number of excursions out of H y , made by one of the two walks S or S, which hit the hyperplane H y+[ε -10 ] . Note that one can order them by time of arrival, considering first those made by S and then those made by S. Let N y be the number of excursions among the first N y ∧ (2ε 3 n 1/3 ) previous ones, which spend a time at least ε -17 in the region between H y and H y+[ε -10 ] . Note that for a single excursion, the probability to hit H y+[ε -10 ] in less than ε -17 steps, is of order exp(-cε -3 ), for some constant c > 0. By independence between the first 2ε 3 n 1/3 excursions, we deduce that

P 0,x (N y ≤ ε 3 n 1/3 , N y ≥ 2ε 3 n 1/3 ) ≤ exp(-cn 1/3 ), (3.3)
for some possibly smaller constant c > 0. On the other hand, let T y be the cumulated total time spent by S and S in the region between H y and H y+[ε -10 ] . Observe that the number of levels y between x 1 /3 and 2x 1 /3 which are integer multiples of [ε -10 ] is of order ε 10 x 1 /3, and that the latter is (at least for ε small enough) larger than ε 13 n 2/3 . Thus, for at least one such y, one must have both N y ≤ ε 3 n 1/3 and T y ≤ ε -13 n 1/3 (otherwise the total time spent in the region between the hyperplanes H x 1 /3 and H 2x 1 /3 would exceed n). Using (3.3), we deduce that P 0,x N y ≥ 2ε 3 n 1/3 or T y ≥ ε -13 n 1/3 , for all y ∈ {x 1 /3, . . . , 2x 1 /3} ≤ x 1 exp(-cn 1/3 ), for some constant c > 0. Then as a consequence of the pigeonhole principle, there exists (a deterministic) y 0 ∈ {x 1 /3, . . . , 2x 1 /3}, such that

P 0,x (N y 0 ≤ 2ε 3 n 1/3 , T y 0 ≤ ε -13 n 1/3 , A) ≥ 1 x 1 P 0,x (A) -exp(-cn 1/3 ),
with the event A as defined in (3.2).

Denote now by x the symmetric of x with respect to H y 0 . First observe that since x 1 ≥ x / √ 3, and x 1 /3 ≤ y 0 ≤ 2x 1 /3, there exists ρ ∈ (0, 1) (independent of x), such that x ≤ ρ x . Next recall that any excursion out of H y 0 and its symmetric with respect to H y 0 have the same probability to happen, and similarly for the first part of the trajectory of S, up to the hitting time, say τ , of H y 0 , under the law P 0,x . Moreover, by reflecting (with respect to H y 0 ) all the excursions out of H y 0 which hit H y 0 +[ε -10 ] , plus S[0, τ ], one can increase the size of the range by at most T y 0 . Therefore,

P 0,x (N y 0 = 0, |R k ∪ R n-k | ≤ -εn + ε -13 n 1/3 ) ≥ 2 -2ε 3 n 1/3 P 0,x (N y 0 ≤ 2ε 3 n 1/3 , T y 0 ≤ ε -13 n 1/3 , A).
Combining the last two displays we conclude that for n large enough,

P 0,x (A) ≤ 2 4ε 3 n 1/3 P 0,x |R k ∪ R n-k | ≤ -εn + ε -13 n 1/3 + exp(-cn 1/3 ),
for some (possibly smaller) constant c > 0. Repeating the same argument (5/2) log ε/(log ρ) times, and using (3.1) and (2.3), we obtain the desired result.

4 Proof of Theorem 1.1

Let k ≤ ≤ n be given, satisfying -k = K 0 ε n , with K 0 a constant to be fixed later. Write I = {k, . . . , }. Using that

|R n | = |R(I)| + |R(I c )| -|R(I) ∩ R(I c )|,
we have, with ν := 1 -K 0 ε 3 ,

P(|R n | ≤ -εn) ≤ P(|R(I)| + |R(I c )| ≤ -νεn) + P(|R(I) ∩ R(I c )| ≥ K 0 3 ε 2 n). (4.1)
We start by showing that the first probability on the right-hand side is negligible (when compared to the probability on the left-hand side). For this let N = ε -2 , and for i = 0, . . . , N , let α i := iε 2 . Then, note that for n large enough, )), (4.2) using Chernoff's bound for the last inequality (see for instance Theorem 3.1 in [START_REF] Chung | Concentration inequalities and martingale inequalities: a survey[END_REF]). Now applying the Markov property and using Proposition 3.1 and (2.2), we get that for any i ≤ N , there exists n i ≥ 1, such that for all n ≥ n i ,

x ≤n 2/3 P |R(I)| ≤ -να i εn, |R(I c )| ≤ -ν(1 -α i+1 )εn, S -S k = x ≤ x ≤n 2/3 P |R(I)| ≤ -να i εn, S -S k = x • exp -I 3 ( ε i 1 + ε 2 i )(1 -K 0 ε) 1/3 n 1/3 ≤ exp -I 3 ( ε i )(1 -ε 2 )(K 0 εn) 1/3 -I 3 ( ε i 1 + ε 2 i )(1 -K 0 ε) 1/3 n 1/3 , (4.3)
with

ε i := ν (1 -α i+1 )ε 1 -K 0 ε , and
ε i := να i K 0 .
Note that by choosing larger n i if necessary, one can also assume that (4.2) holds for n ≥ n i . Note furthermore that by (2.3), the first term in the exponential in (4.3) is already larger than 2I 3 (ε)n 1/3 , when α i ≥ K 0 √ ε, at least provided K 0 is large enough and ε small enough. Thus in the following one can assume that α i ≤ K 0 √ ε. We will also assume that ε is small enough, so that K 0 √ ε < 1/2. Then, using in particular that α i+1 = α i + ε 2 , we get (recall that ν = 1 -K 0 ε 3 )

I 3 ( ε i )(1 -ε 2 )(K 0 ε) 1/3 + I 3 ( ε i 1 + ε 2 i )(1 -K 0 ε) 1/3 ≥ µ 3 (1 - K 0 ε 3 ) 2/3 α 2/3 i K 1/3 0 ε 1/3 + (1 -α i ) 2/3 (1 -K 0 ε) 1/3 ε 2/3 -O(ε 2 ).
Now we claim that the bound in the parenthesis above reaches its infimum when i = 0, or equivalently when α i = 0. To see this, it suffices to consider the variations of the function f defined for u ∈ (0, 1) by

f (u) = c 1/3 1 u 2/3 + c 1/3 2 (1 -u) 2/3
, with c 1 = (K 0 ε) -1 , and c 2 = (1 -K 0 ε) -1 . A straightforward computation shows that f (u) > 0 on (0, u 0 ), with u 0 = 1 -K 0 ε. Since we assumed that u 0 > 1/2 > K 0 √ ε, this proves our claim. By taking K 0 = 100C, with C the constant appearing in the upper bound of I 3 in (2.3), one deduces that for ε small enough,

I 3 ( ε i )(1 -ε 2 )(K 0 ε) 1/3 + I 3 ( ε i 1 + ε 2 i )(1 -K 0 ε) 1/3 ≥ µ 3 (1 + K 0 ε 10 )ε 2/3 -O(ε 2 ) ≥ I 3 (ε)(1 + K 0 ε 20 ).
As a consequence, letting N (ε) := max i n i , we get that for ε small enough, for all n ≥ N (ε),

N i=0 P |R(I)| ≤ -να i εn, |R(I c )| ≤ -ν(1 -α i+1 )εn ≤ exp(-I 3 (ε)(1 + K 0 ε 20 )n 1/3 ).
One can obtain similarly the same bound for the term P(|R(I c )| ≤ -νεn), also for all n ≥ N (ε), possibly by taking a larger constant N (ε) if necessary. Finally using again (2.2), we get that for all ε small enough, Both terms on the right-hand side are treated similarly. We first fix β < 1/(24κ), with κ the constant appearing in statement of Lemma 1.3. Then applying Lemma 1.3 with ρ = βε, n = K 0 εn , and t = K 0 24 ε 2 n, we get (using also the Markov property at time k),

P(|R(I) ∩ R 1 ∩ Λ c 1 | ≥ K 0 24 ε 2 n) ≤ exp(-(βε) 1/3 K 0 ε 2 n 48r 2 )
≤ exp(-β 1/3 K 0 48 ε 2/3 n 1/3 ), using that r ≤ ε 5/6 n 1/3 , for the last inequality. By taking larger K 0 if necessary, one can ensure that this bound is o((1/n) • P(|R n | ≤ -εn)). This way we obtain

P(|R(I) ∩ R 1 ∩ Λ c 1 | ∨ |R(I) ∩ R 2 ∩ Λ c 2 | ≥ K 0 24 ε 2 n) = o 1 n P(|R n | ≤ -εn) . (4.5)
Coming back to (4.1), dividing both sides of the inequality by the term on the left-hand side, and using (4.4) and (4.5), we get that for all ε small enough,

Q ε n |R(I) ∩ Λ 1 ∩ R 1 | ≥ K 0 8 ε 2 n, or |R(I) ∩ Λ 2 ∩ R 2 | ≥ K 0 8 ε 2 n ≥ 1 -o 1 n .
Since both Λ 1 ∩ R 1 ⊆ V n (βε, r) ∩ R(I c ), and Λ 2 ∩ R 2 ⊆ V n (βε, r) ∩ R(I c ), we get

Q ε n |R(I) ∩ R(I c ) ∩ V n (βε, r)| ≥ K 0 8 ε 2 n ≥ 1 -o 1 n .
The proof of Theorem 1.1 follows by a union bound, since there are at most n intervals I of fixed length in I n .

  be the cube of side length 2r, and then define regions of high density as follows. First we define the (random) set of centers, depending on a density ρ, a scale r, and a time window I as: C(ρ, r, I) := {x ∈ 2rZ d : |R(I) ∩ Q(x, r)| ≥ ρ • |Q(x, r)|}, and then the corresponding region V(ρ, r, I) := x∈C(ρ,r,I)

PP

  (|R(I)| + |R(I c )| ≤ -νεn) ≤ N i=0 |R(I)| ≤ -να i εn, |R(I c )| ≤ -ν(1 -α i+1 )εn + P |R(I c )| ≤ -νεn ≤ N i=0 x ≤n 2/3 P |R(I)| ≤ -να i εn, |R(I c )| ≤ -ν(1 -α i+1 )εn, S -S k = x + P |R(I c )| ≤ -νεn + O(exp(-cn 1/3

P

  (|R(I)| + |R(I c )| ≤ -νεn) = o 1 n P(|R n | ≤ -εn) . (4.4)It remains to estimate the second term in the right-hand side of (4.1). This is similar to the proof of Theorem 1.2. Assume given 1 ≤ r ≤ ε 5/6 n 1/3 , and β > 0, whose value will be made more precise in a moment. To simplify notation, writeR 1 = R[0, k] and R 2 := R[ , n]. Next set Λ 1 = ∪ x∈C 1 Q(x, r), and Λ 2 = ∪ x∈C 2 Q(x, r),withC 1 := {x ∈ 2rZ d : |Q(x, r) ∩ R 1 | ≥ βεr d }, and C 2 := {x ∈ 2rZ d : |Q(x, r) ∩ R 2 | ≥ βεr d }. Since R(I c ) = R 1 ∪ R 2 , one has |R(I) ∩ R(I c )| ≤ |R(I) ∩ R 1 | + |R(I) ∩ R 2 |,and therefore,P(|R(I) ∩ R(I c )| ≥ K 0 3 ε 2 n) ≤ P(|R(I) ∩ R 1 | ≥ K 0 6 ε 2 n) + P(|R(I) ∩ R 2 | ≥ K 0 6 ε 2 n).


Andrew Reynolds
email: andrew.j.reynolds@gmail.com

Haniel Barbosa
email: haniel.barbosa@inria.fr

Pascal Fontaine
email: pascal.fontaine@inria.fr

Revisiting Enumerative Instantiation

published or not. The documents may come

Introduction

In many formal methods applications, such as verification, it is common to represent proof obligations in terms of the Satisfiability Modulo Theories (SMT) problem. SMT solvers have thus become popular backends for such applications. They have been primarily designed to be decision procedures for quantifier-free problems, on which they are highly efficient and capable of handling large formulas over background theories. Quantified formulas are generally handled with instantiation techniques that are often incomplete, even on decidable or semi-decidable fragments. Heavily relying on incomplete heuristics however leads to instability and unpredictability on the solver's behavior, which is undesirable for the tools relying on them. To address these issues some systems use model-based instantiation (MBQI) [START_REF] Ge | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories[END_REF], a complete technique for first-order logic with equality and for several restricted fragments containing theories, which can be used as a fallback strategy to the incomplete techniques.

In this paper we introduce a novel enumerative instantiation technique which can serve as a simpler alternative to model-based instantiation. Similar to MBQI, our technique can be used as a secondary strategy when incomplete techniques fail. Our exper-iments show that a careful implementation of this technique in the state-of-the-art SMT solver CVC4 leads to noticeable gains in performance on unsatisfiable problems.

Background Some of the earliest tools for theorem proving in first-order logic come from the work by Skolem and Herbrand. The Herbrand Theorem states that if a closed formula in Skolem normal form, i.e. a prenex formula without existential quantifiers, is unsatisfiable, then there is an unsatisfiable finite conjunction of Herbrand instances of the formula, that is, instances on terms from the Herbrand universe, i.e. the set of all possible well-sorted ground terms in the formula's signature. The first theorem provers for first-order logic to be implemented based on Herbrand's theorem employed a completely unguided search on the Herbrand Universe (e.g. Gilmore [START_REF] Gilmore | A proof method for quantification theory: Its justification and realization[END_REF] and Davis, Logemann and Loveland [START_REF] Davis | A machine program for theorem-proving[END_REF] early efforts). Such systems were only capable of dealing with very simple formulas and were soon put aside. Techniques which would only generate Herbrand instances when needed were first introduced by Prawitz [START_REF] Prawitz | An improved proof procedure1[END_REF] and later refined by Davis and Putnam [START_REF] Davis | A computing procedure for quantification theory[END_REF], culminating in the resolution calculus introduced by Robinson [START_REF] Robinson | A machine-oriented logic based on the resolution principle[END_REF]. The most successful techniques for handling pure first-order logic have been based on resolution and ordering criteria [START_REF] Bachmair | Resolution theorem proving[END_REF]. More recently, techniques based on instantiation have shown promise for first-order logic as well [START_REF] Ganzinger | New directions in instantiation-based theorem proving[END_REF][START_REF] De Moura | Efficient E-Matching for SMT Solvers[END_REF][START_REF] Reynolds | Finding conflicting instances of quantified formulas in SMT[END_REF]. Inspired by early work on the subject, this paper revisits whether modern implementations of the latter class of techniques can benefit from enumerative instantiation.

Outline We first give preliminaries in Section 2. Then, we introduce a stronger Herbrand Theorem as the basis for making enumerative instantiation practical so that it can be used in modern systems in Section 3. We formalize the different instantiation strategies used by state-of-the-art SMT solvers, discuss their strengths and weaknesses, and present a schematization of how to combine such strategies in Section 4, with a focus on a new strategy for enumerative instantiation. An extensive experimental evaluation of enumerative instantiation as implemented in CVC4 is presented in Section 5.

Preliminaries

We work in the context of many-sorted first-order logic with equality (see e.g. [START_REF] Enderton | A mathematical introduction to logic[END_REF]) and assume the reader is familiar with the notions of signature, term, (quantified and ground) formula, atom, literal, free and bound variable, and substitution.

We consider signatures Σ containing a Bool sort and constants , ⊥ and a family of predicate symbols (≈ : τ × τ → Bool) interpreted as equality for each sort τ. Without loss of generality, we assume ≈ is the only predicate in Σ. We use = for syntactic equality. The set of all terms occurring in a formula ϕ (resp. term t) is denoted by T(ϕ) (resp. T(t)). We write t for the sequence of terms t 1 , . . . , t n for an unspecified n ∈ N + that is either irrelevant or deducible from the context.

An interpretation is a triple M = (D, I , V ) in which D is a collection of nonempty domain sets for all sorts in Σ, I interprets symbols by mapping them into

SMT formula

Model

UNSAT

SMT solver Instantiation module

Instance Assignment

Ground

SMT solver

Fig. 1: The SMT instantiation loop for quantified formulas functions over domain sets according to the symbol sort, and V maps free variables to elements of their respective domain sets. A theory is a pair T = (Σ, Ω) in which Σ is a signature and Ω is a class of interpretations denoted the models of T . The empty theory is the theory for which the class of interpretations Ω is unrestricted, which coincides with first-order logic with equality. Throughout this paper we assume a fixed background theory T , which unless otherwise stated is the empty theory. A formula ϕ is satisfiable (resp. unsatisfiable) in T if it is satisfied by some (resp. no) interpretation M ∈ Ω, written M |= T ϕ. A formula ϕ entails in T a formula ψ, written ϕ |= T ψ, if every interpretations in Ω satisfying ϕ also satisfies ψ. For these notions of model satisfaction and entailment in the empty theory, we omit the subscript.

A substitution σ maps variables to terms and its domain, dom(σ), is finite. We write ran(σ) to denote its range. Throughout the paper, conjunctions may be written as sets or tuples, and vice-versa, whenever convenient and unambiguous. All definitions are assumed to be lifted in the expected way from formulas into sets or tuples of formulas.

Instantiation-Based SMT Solvers

Quantifiers in formulas are generally handled by SMT solvers through instantiationbased techniques, which capitalize on their capability to handle large ground formulas. In this approach, an input formula ψ is given to the ground SMT solver, which will abstract all atoms and quantified formulas and treat them as if they were propositional variables. The solver for ground formulas will provide an assignment E ∪ Q, where E is a set of ground literals and Q is a set of quantified formulas appearing in ψ, such that E ∪ Q propositionally entails ψ. We assume that all quantified formulas in ψ are of the form ∀ x. ϕ with ϕ quantifier-free. This can be achieved by prenex form transformation and Skolemization. The instantiation module of the solver will then generate new ground formulas of the form ∀ x. ϕ ⇒ ϕσ where ∀ x. ϕ is a quantified formula in Q and σ is a substitution from the variables in ϕ to ground terms. These instances will be added conjunctively to the input of the ground solver, hence refining its knowledge of the quantified formulas. The ground solver may then provide another assignment E ∪ Q , where this is a set that entails both ϕ and the newly added instances. This new assignment might either be the previous one, augmented by new ground literals com-ing from the new instances, or if the previous E has been refuted by the new instances, a completely different set. On the other hand, the process may terminate if the newly added instances suffice to prove the unsatisfiability of the original formula. We will refer to the game between the ground solver that provides assignments for the abstraction of the formula and the instantiation module that provides instances added conjunctively to the formula, as the instantiation loop of the SMT solver (see Figure 1).

Herbrand Theorem and Beyond

The Herbrand Theorem (see e.g. [START_REF] Enderton | A mathematical introduction to logic[END_REF]) for pure first-order logic with equality1 provides a refutationally complete procedure to check the satisfiability of a formula ψ, or more specifically of a set of literals and quantifiers

E ∪ Q. Indeed, E ∪ Q is satisfiable if and only if E ∪ Q g is satisfiable,
where Q g is the set of all (Herbrand) instances one can build from the quantifiers in Q by instantiation with the Herbrand universe, i.e. all the possible well-sorted terms built on the signature used in E ∪ Q. Based on this, an instantiation module has a simple refutationally complete strategy for pure first-order logic with equality: it suffices to enumerate Herbrand instances. The major drawback of this strategy is that the Herbrand universe is large. For instance, as soon as there is a function with the range sort also used as an argument, the Herbrand universe is infinite. Fortunately, a stronger variant of the Herbrand Theorem holds. Using this variant, the instantiation module does not need to consider all possible well-sorted terms (i.e. the full Herbrand universe), but only the terms already available in E ∪ Q, and those subsequently generated.

Theorem 1. Consider the conjunctive sets E and Q of ground literals and universally quantified clauses respectively where T(E) contains at least one term of each sort. The set E ∪ Q is unsatisfiable in pure first-order logic if and only if there exists a series Q i of finite sets of instances of Q such that for some number n, the finite set of formulas

E ∪ n i=1 Q i is unsatisfiable; -Q i+1 ⊆ ϕσ | ∀ x. ϕ ∈ Q, ran(σ) ⊆ T(E ∪ i j=1 Q j ) .
Proof. All proofs for this section are included in [START_REF] Reynolds | Revisiting enumerative instantiation[END_REF].

The above theorem is stronger than the classical Herbrand theorem in the sense that the set of instances considered above is smaller (or equal) than the set of instances considered in the classical Herbrand theorem. As a trivial example, if a function f appears only in E ∪ Q in ground terms, no new applications of f are considered. The theorem does not consider all arbitrary terms from the signature, but only those that are generated by the successive instantiations with only already available ground terms.

Note the theorem holds for pure first-order logic with equality, and in any theory that preserves the compactness property. It is also necessary however to consider the axioms of the theory for the generation of new terms, that might lead to other instances.

In the Bernays-Schönfinkel-Ramsey fragment of first-order logic (also know as the EPR class) formulas do not contain non constant function symbols, therefore the Herbrand universe of any formula is a finite set. Since the above sets of terms are a subset of the Herbrand universe, the enumeration will always terminate, even when the formula is satisfiable. Therefore, the resulting ground problem is decidable, and the above method comprises a decision procedure for this fragment, just like some variant of model-based quantifier instantiation.

Theorem 1 implies that an instantiation module only has to consider terms occurring within assignments, and not all possible terms. To show refutational completeness (termination on unsatisfiable input) and model soundness (termination without declaring unsatisfiability implies that the input is satisfiable), it is however necessary to account for the successive assignments produced by the ground SMT solver and the consecutive generation of instances. This is achieved using the following lemma.

Lemma 1. Consider the conjunctive sets E and Q of ground literals and universally quantified clauses respectively where T(E) contains at least one term of each sort. If there exists an infinite series of finite satisfiable sets of ground literals E i and of finite sets of ground instances

Q i of Q such that -Q i = ϕσ | ∀ x. ϕ ∈ Q, dom(σ) = { x} ∧ ran(σ) ⊆ T(E i ) ; -E 0 = E, E i+1 |= E i ∪ Q i ;
then E ∪ Q is satisfiable in the empty theory with equality.

The above lemma has two direct consequences on the instantiation loop of SMT solvers, where instances are generated from the set of available terms in the ground assignment provided by the ground SMT solver. The following two corollaries state the model soundness and the refutational completeness of the instantiation loop respectively.

Corollary 1. Given a formula ψ, if there exists a satisfiable set of literals E and a set of quantified clauses Q such that E ∪ Q |= ψ and the instantiation module of the SMT solver cannot generate any new instance, i.e. E already entails all instances of Q for substitutions built with terms T(E), then ψ is satisfiable.

Proof. A formal statement of the corollary and a proof is available in [START_REF] Reynolds | Revisiting enumerative instantiation[END_REF].

Corollary 2. Given an unsatisfiable formula, if the generation of instances is fair the instantiation loop of the SMT solver terminates.

Proof. A formal statement of the corollary and a proof is available in [START_REF] Reynolds | Revisiting enumerative instantiation[END_REF].

Quantifier Instantiation in CDCL(T )

This section overviews recent techniques used by SMT solvers for quantifier instantiation, and comments on their relative strengths and weaknesses. We will focus on enumerative quantifier instantiation, a technique which has received little attention in recent work, but has several compelling advantages with respect to current techniques.

Definition 1 (Instantiation Strategy

). An instantiation strategy takes as input:

1. A T -satisfiable set of ground literals E, and 2. A quantified formula ∀ x. ϕ.

It outputs a set of substitutions {σ 1 , . . . , σ n } where dom(σ i ) = x for each i = 1, . . . , n.

Figure 2 gives four instantiation strategies used by modern SMT solvers, each that have the interface given in Definition 1. The first three have been described in detail in previous works (see [START_REF] Reynolds | Conflicts, models and heuristics for quantifier instantiation in SMT[END_REF] for a recent overview). We briefly review these techniques in this section. The fourth, enumerative quantifier instantiation, is the subject of this paper.

Conflict-based instantiation (c) was introduced in [START_REF] Reynolds | Finding conflicting instances of quantified formulas in SMT[END_REF] as a technique for improving the performance of SMT solvers for unsatisfiable problems. In this strategy, we return a substitution σ such that ϕσ together with E is unsatisfiable, We refer to ϕσ as a conflicting instance (for E). Typical implementations of this strategy do not insist that a conflicting instance be returned if one exists, and hence the strategy may choose to return the empty set of substitutions. Recent work [START_REF] Barbosa | Congruence closure with free variables[END_REF][START_REF] Barbosa | New techniques for instantiation and proof production in SMT solving[END_REF] gives a strategy for conflictbased instantiation that has refutational completeness guarantees for the empty theory with equality, that is, when a conflict instance exists for a quantified formula in this theory, the strategy is guaranteed to return it. E-matching instantiation (e) is the most commonly used strategy for quantifier instantiation in modern SMT solvers [START_REF] Detlefs | Simplify: A Theorem Prover for Program Checking[END_REF][START_REF] De Moura | Efficient E-Matching for SMT Solvers[END_REF][START_REF] Ge | Solving Quantified Verification Conditions Using Satisfiability Modulo Theories[END_REF]. In this strategy, we first heuristically choose a set of triggers for a quantified formula ∀ x. ϕ, where a trigger is a tuple of terms whose free variables are x. In practice, triggers can be selected using user-provided annotations, or selected automatically by the SMT solver. For each trigger ti , we select a set of substitutions S i such that for each σ in this set, E entails that ti σ is equal to a tuple of ground terms g i in E. We return the union of these sets S i for each selected trigger. E-matching instantiation is generally incomplete, but works well in practice for unsatisfiable problems, and hence is a key component of most SMT solvers that support quantified formulas.

Model-based quantifier instantiation (m) was introduced in [START_REF] Ge | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories[END_REF], and has also been used for improving the performance of finite model finding [START_REF] Reynolds | Quantifier Instantiation Techniques for Finite Model Finding in SMT[END_REF]. In this strategy, we first construct a model M for the quantifier-free portion of our input E, where typically the interpretations of functions for values not constrained by E are chosen heuristically. Notice that M does not necessarily satisfy the quantified formula ∀ x. ϕ. If it does not, we return a single substitution σ for which M does not satisfy ϕσ, where typically σ maps variables from x to terms that occur in T(E). With respect to conflict-based and E-matching instantiation, model-based quantifier instantiation has the advantage that it is model sound: when it returns / 0, then E ∪ {∀ x. ϕ} is satisfiable. This paper revisits enumerative quantifier instantiation (u) as a viable alternative to model-based quantifier instantiation. In this strategy, we assume an ordering on quantifier-free terms. This ordering is not related to the usual term ordering one generally uses for saturation theorem proving, but rather determines which instance will be generated first. The strategy returns the substitution { x → t}, where t is the minimal tuple of terms with respect to from T(E) such that ϕ{ x → t} is not entailed by E. We refer to this strategy as enumerative instantiation since in the worst case it generates instantiations by enumerating tuples of all terms of the proper sort from E, according to the ordering . In practice, the number of instantiations produced by this strategy is kept small by interleaving it with other strategies like c or e, or due to the fact that a small number of instances may already allow the SMT solver to conclude the input is unsatisfiable. Moreover, thanks to the results in Section 3, this strategy is refutationally complete and model sound for quantified formulas in the empty theory with equality. In the previous example, clearly {x → b} is the most useful substitution, since it leads to an instance P(b) ∨ R(b) which together with E is unsatisfiable. The substitution {x → c} is definitely not a useful substitution, since it is already entailed by P(c) ∈ E. The substitution {x → a} is potentially useful since it forces the solver to satisfy P(a) ∨ R(a). Here, we point out that the effect of enumerative instantiation and model-based instantiation is essentially the same, as both return an instance that is not entailed by E. However, the substitutions produced by enumerative instantiation often have advantages with respect to model-based instantiation on unsatisfiable problems. A key observation is that useful instantiations can be obscured by guesses made when constructing models M . Here, since we decided R(a) M = ⊥, the substitution {x → a} was not considered when applying model-based instantiation to the second quantified formula, and since S (a) M = ⊥, the substitution {x → a} was not considered when applying it to the third. In implementations of model-based instantiation, certain values in models are chosen heuristically, leading to this behavior. This is done out of necessity, since determining whether there exists a model that satisfies quantified formulas, even for a fixed context, is a challenging problem.

On the other hand, the range of substitutions considered by enumerative instantiation in the previous example include all terms that correspond to instances that are not entailed by E. The substitutions it considers are "minimally diverse", that is, in the previous example they introduce new predicates on term a only, whereas modelbased instantiation introduces new predicates on a, b and c. Reducing the number of new terms introduced by instantiations can have a significant positive impact on performance in practice. Furthermore, enumerative instantiation has the advantage that a term ordering allows fine-grained heuristics better suited for unsatisfiable problems, which we comment on in Section 4.1.

Example 3. Consider the sets E = {a ≈ b, b ≈ a ≈ c} and Q = {∀x. P(x)}. For the input (E, ∀x. P(x)), model-based quantifier instantiation will first construct a model M for E, where assume that P M = λx. . It is easy to see M |= ϕ{x → t} for a, b, c ∈ T(E), and hence it returns the empty set of substitutions, indicating that E∪Q is satisfiable. On the other hand, assume enumerative instantiation chooses the lexicographic extension of a term ordering where a ≺ b ≺ c. Since E |= P(a) and a is smaller than b and c according to , u(E, P(x)) returns the set containing {x → a}. Subsequently and for similar reasons, two more iterations of this strategy will be invoked, resulting in the instances P(b) and P(c) before it terminates with the empty set.

In this example, model-based instantiation was able to terminate on the first iteration, since it guessed the correct interpretation for P, whereas enumerative instantiation considered substitutions mapping x to each ground term a, b, c from E. For this reason, model-based instantiation is typically better suited for satisfiable problems.

Implementing Enumerative Instantiation

We comment on several important details concerning the implementation of enumerative quantifier instantiation in the SMT solver CVC4.

Term Ordering Given a term ordering , CVC4 considers the extension to tuples of terms such that:

(t 1 , . . . , t n ) ≺ (s 1 , . . . , s n ) if max n i=1 t i ≺ max n i=1 s i , or max n i=1 t i = max n i=1 s i and (t 1 , . . . , t n ) ≺ lex (s 1 , . . . , s n )
where ≺ lex is the lexicographic extension of

≺. For example, if a ≺ b ≺ c, then we have that (a, a) ≺ (a, b) ≺ (b, a) ≺ (b, b) ≺ (a, c) ≺ (c, b) ≺ (c, c).
By this ordering, we consider substitutions involving c only after all combinations of substitutions involving a and b are considered. This choice is important since it leads to instantiations that introduce fewer terms, and are thus more likely to lead to conflicts at the ground level.

The underlying term ordering is determined dynamically based on the current set of assertions E. At all times, we maintain a finite list of quantifier-free terms such that we have fixed the ordering t 1 ≺ . . . ≺ t n . Then, if all combinations of instantiations for t 1 , . . . , t n are currently entailed by E, we choose a term t ∈ T(E) that is such that E |= t ≈ t i for i = 1, . . . , n if one exists, and append it to our ordering so that t n ≺ t. The particular choice of t beyond this criteria is arbitrary. An experimental evaluation of more sophisticated term orderings, such as those inspired by first-order automated theorem proving [START_REF] Baader | Term Rewriting and All That[END_REF] is the subject of future work.

Entailment Checks For a set of ground equalities and disequalities E, quantified formula ∀ x. ϕ and substitution { x → t}, CVC4 implements a two-layered method for checking whether the entailment E |= ϕ{ x → t} holds. First, we maintain a cache of instantiations that have already been returned on previous iterations. Hence if E satisfies a set of formulas containing ϕ{ x → s}, where E |= t ≈ s, then the entailment clearly holds.

Second, we use an incomplete and fast method for inferring when an entailment holds. We first compute from E congruence classes over T(E). For each t ∈ T(E), let [t] be the representative of term t in this equivalence relation. For each function f , we use a term index data structure I f that stores an entry of the form

([t 1 ], . . . , [t n ]) → [ f (t 1 , . . . , t n )] ∈ I f for each uninterpreted function application f (t 1 , . . . , t n ) ∈ T(E).
To check the entailment of E |= where is a literal, we update based on the iterative process until a fixed point is reached: Then, if the resultant ψ is , then the entailment holds. Although not shown here, the above process is extended in a straightforward way to handle Boolean structure, and also can be extended in the presence of other background theories in a straightforward way by incorporating theory-specific rewriting steps.

1. Replace each constant t in with [t]. 2. Replace each function term f (t 1 , . . . , t n ) in with s if (t 1 , . . . , t n ) → s ∈ I f . 3. If is t ≈ t,
Restricting Enumeration Space Enumerative instantiation can be refined further by noticing that only a subset of the set of terms T(E) will ever be relevant for showing unsatisfiability of a quantified formula. An approach in this spirit was used by Ge and de Moura [START_REF] Ge | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories[END_REF], where decidable fragments were identified by noticing that the relevant domains of quantified formulas in these fragments are guaranteed to be finite. In that work, the relevant domain of a quantified formula ∀ x. ψ is computed based on the terms in E and the structure of its body ψ. For example, t is in the relevant domain of function f for all ground terms f (t), the relevant domain of x for a quantified formula containing the term f (x) is equal to the relevant domain of f , and so on. A related approach is to use sort inference [START_REF] Claessen | New techniques that improve MACE-style finite model finding[END_REF][START_REF] Claessen | Sort It Out with Monotonicity[END_REF][START_REF] Korovin | Non-cyclic sorts for first-order satisfiability[END_REF], to compute more precise sort information and thus decrease the number of possible instantiations.

E ∪ Q is equivalent to E s ∪ Q s = {a 1 ≈ b 1 , f 12 (a 1 ) ≈ c 2 } ∪ {P 2 ( f 12 (x 1 ))}, where a 1 , b 1 , x 1 are of sort τ 1 , c 2 is of sort τ 2 , f 12 is of sort τ 1 → τ 2 , and P 2 is a predicate on τ 2 .
Sorts can be inferred in this manner using a linear traversal on the input formula (for details, see for instance Section 3 of [START_REF] Korovin | Non-cyclic sorts for first-order satisfiability[END_REF]). This technique narrows the set of terms considered by enumerative instantiation. In the above example, whereas enumerative instantiation for E ∪ Q might consider the substitutions {x → c} or {x → f (c)}, for E s ∪ Q s it would not consider {x 1 → c 2 } since their sorts are different, nor would it consider {x 1 → f 12 (c 2 )} since f 12 (c 2 ) is not a well-sorted term. Moreover, the Herbrand universe of an inferred subsort may be finite when the universe of its parent sort is infinite. In the above example, the Herbrand universe of τ 1 is {a 1 , b 1 } and τ 2 is { f 12 (a 1 ), f 12 (b 1 ), c 2 }, whereas the Herbrand universe of τ is infinite.

Compound Strategies Since the instantiation strategies from this section have their respective strengths and weaknesses, it is valuable to combine them. We consider two ways of combining strategies which we refer as priority instantiation and interleaved instantiation. For base strategies s 1 and s 2 , priority instantiation (s 1 ; s 2 ) first invokes s 1 . If this strategy returns a non-empty set of substitutions, it returns that set, otherwise it returns the instances returned by s 2 . On the other hand, interleaved instantiation (s 1 +s 2 ) returns the union of the substitutions returned by the two strategies.

Enumerative instantiation is the most effective when used as a complement to heuristic strategies. In particular, we will see in the next section that the strategies c;e;u and c;e+u are the most effective strategies for unsatisfiable problems in CVC4.

Experiments

This section reports on our experimental evaluation of different strategies based on enumerative instantiation as implemented in the SMT solver CVC4. 2 We present an extensive analysis of enumerative instantiation and compare it with implementations of model-based instantiation on both unsatisfiable and satisfiable benchmarks. Experiments were performed on untyped first-order benchmarks from the TPTP library [START_REF] Sutcliffe | The TPTP problem library and associated infrastructure[END_REF] 3 , version 6.4.0, and from SMT-LIB [START_REF] Barrett | The SMT-LIB Standard: Version 2[END_REF], as of October 2017, on logics having quantifiers and either uninterpreted functions or arrays. For the latter, we considered also logics containing other theories such as arithmetic and datatypes. Some benchmarks are solved by all considered configurations of solvers in less than 0.1 seconds. We discarded those 25 580 benchmarks. In total, 42 065 problems were selected, 14 731 from TPTP and 27 334 from SMT-LIB. All results were produced on StarExec [START_REF] Stump | Starexec: A cross-community infrastructure for logic solving[END_REF], a public execution service for running comparative evaluations of solvers, with a timeout of 300 seconds. Fig. 3: CVC4 configurations on unsatisfiable benchmarks with a 300 second timeout.

We follow the convention in Section 4 for identifying configurations based on their instantiation strategy. All configurations of CVC4 use conflict-based instantiation [START_REF] Reynolds | Finding conflicting instances of quantified formulas in SMT[END_REF][START_REF] Barbosa | Congruence closure with free variables[END_REF] with highest priority, so we omit the prefix "c;" from the names of CVC4 configurations e.g. e+u in fact means c;e+u. Sort inference, as discussed in Section 4.1, is also used by all configurations of CVC4.

Impact of Enumerative Instantiation in CVC4

In this section, we highlight the impact of enumerative instantiation in CVC4 for unsatisfiable benchmarks. Where applicable, we contrast the difference in the impact of enumerative instantiation and model-based instantiation on the performance of CVC4 on unsatisfiable benchmarks. 4The comparison of various instantiation strategies supported by CVC4 is summarized in Figure 3. In the table, each row is dedicated to a library and logic. SMT-LIB is shown in more granularity than TPTP to highlight comparisons of individual strategies. The first column identifies the subset and the second shows its total number of benchmarks. The next seven columns show the number of benchmarks found to be unsatisfiable by each configuration. The last three columns show the results of virtual portfolio solvers, with uport combining e, u, e;u, and e+u; and mport combining e, m, e;m, and e+m; while port combines all seven configurations.

First, we can see that u outperforms m, as it solves 3 043 more benchmarks overall. While this is not close to the performance of E-matching (e), it should be noted that u is highly orthogonal to e, solving 1 737 benchmarks that could not be solved by e5 . Combining e with either u or m, using either priority or interleaving instantiation, leads to significant gains in performance. Overall the best configuration is e+u, that is, the interleaving of enumerative instantiation and E-matching, which solves 20 535 benchmarks, that is, 253 more than its counterpart e+m interleaving model-based instantiation and E-matching, and 1 295 more than E-matching alone. In the UFLIA logic, the enumerative techniques are specially effective in comparison with the model-based ones. In particular, they enable CVC4 to solve previously intractable problems, e.g. the family "sexpr" with 32 problems. These are notoriously hard problems involving the verification of C# programs using Spec# [START_REF] Barnett | The Spec# Programming System: Challenges and Directions[END_REF]. Z3 can solve 31 of them thanks to its advanced optimizations of E-matching [START_REF] De Moura | Efficient E-Matching for SMT Solvers[END_REF]. CVC4 previously could solve at most 16 using techniques combining e and m, but u alone could solve 27, and all of 32 are solved by e+u. Another example is the family "vcc-havoc" in UFNIA, stemming from the verification of concurrent C with VCC [START_REF] Cohen | VCC: A Practical System for Verifying Concurrent C[END_REF]. The strategy e+u solves 940 out of 984 problems, outperforming e and its combinations with m, which solve at most 860 problems 6 .

The portfolio columns of the table in Figure 3 highlight the improvement due to enumerative instantiation for CVC4 on the number of solved problems: there are 712 more problems overall solved when adding enumerative instantiation in the strategies (see columns mport and port). The cactus plot of Figure 3 shows that while the priority strategies are initially quicker, the interleaving ones scale better, solving more hard problems than their priority counterparts. Overall, we conclude that in addition to being much simpler to implement7 instantiation strategies that combine E-matching with enumerative instantiation in CVC4 have a noticeable advantage over those that combine E-matching with model-based instantiation on unsatisfiable problems.

Comparison Against Other SMT Solvers

In this section, we compare our implementation of enumerative instantiation in CVC4 against another state-of-the-art SMT solver: Z3 [START_REF] De Moura | Z3: An Efficient SMT Solver[END_REF] (version 4.5.1) which, like CVC4, also relies on E-matching instantiation for handling unsatisfiable problems. Before making the comparison, we first summarize the main differences between Z3 and CVC4 here. Z3 uses several optimizations for E-matching that are not implemented in CVC4, including the use of code trees and techniques for applying instantiation incrementally during the CDCL(T ) search (see Section 5 of [START_REF] De Moura | Efficient E-Matching for SMT Solvers[END_REF]). It also implements techniques for removing previously considered instantiations from its set of known clauses (see Section 7 of [START_REF] De Moura | Efficient E-Matching for SMT Solvers[END_REF]). The main advantage of CVC4 with respect to Z3 is its use of conflictbased instantiation c [START_REF] Reynolds | Finding conflicting instances of quantified formulas in SMT[END_REF], which is enabled by default in all strategies we considered. It also supports interleaved instantiation strategies as described in Section 4.1, whereas Z3 does not. In addition to these differences, Z3 implements model-based instantiation m as described in [START_REF] Ge | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories[END_REF], whereas CVC4 implements model-based instantiation as described in [START_REF] Reynolds | Quantifier Instantiation Techniques for Finite Model Finding in SMT[END_REF]. Finally, CVC4 implements enumerative instantiation as described in this paper, which we compare as an alternative to these implementations.

Figure 4 summarizes the performance of Z3 on our benchmark set. First, like CVC4, using model-based instantiation to complement E-matching leads to significant gains in Z3, as z3 e;m solves a total of 1731 more benchmarks than solved by E-matching alone z3 e. In comparison with CVC4, the configuration z3 e outperforms e in the logics with non-linear arithmetic and other theories, while e is better in the others. Finally, Z3's implementation of model-based quantifier instantiation by itself z3 m is not effective for unsatisfiable benchmarks, solving only 8951 overall.

To further compare Z3 and CVC4, the third column from the left is the number of benchmarks solved by CVC4's E-matching strategy (e), which we gave in Figure 3. The second to last column uport-i gives the number of benchmarks solved by at least one of u, e, or e;u in CVC4, where we intentionally omit the interleaved strategy e+u, since Z3 does not support a similar strategy. The column mport-i is computed similarly. We compare these with the fifth column, z3 mport-i, i.e. the number of benchmarks solved by either z3 m, z3 e or z3 e;m. A comparison of these is given in the cactus plot of Figure 4. We can see that due to Z3's highly optimized implementations, z3 mport-i solves the highest number of problems in less than one second (around 13000), whereas the portfolio strategies of CVC4 solve more for larger timeouts. Overall, the best portfolio strategy is enumerative instantiation in CVC4, which solves a total of 21305 unsatisfiable benchmarks overall, which is 1965 more benchmarks than z3 mport-i, and 470 more benchmarks than mport-i. We thus conclude the use of enumerative instantiation when paired with E-matching and conflict-based instantiation in CVC4 improves the state-of-the-art of instantiation-based SMT solvers for unsatisfiable benchmarks.

Comparison with Automated Theorem Provers Automated theorem provers like Vampire [START_REF] Kovács | First-order theorem proving and vampire[END_REF] and E [START_REF] Schulz | E -a brainiac theorem prover[END_REF] use substantially different techniques based on superposition, hence we do not provide an extensive comparison here. However, we do remark that the gains provided by enumerative instantiation were one of the main reasons for CVC4 being more competitive in the 2017 CASC competition of automatic theorem provers [START_REF] Sutcliffe | The CADE ATP System Competition -CASC[END_REF]. CVC4 placed third in the category with unsatisfiable problems on the empty theory, as in previous years, behind superposition-based theorem provers Vampire and E, which implement complete strategies. There was, however, a 23% reduction in the number of problems that E solves and CVC4 does not, w.r.t. the previous competition, reducing the gap between the two systems.

Satisfiable Benchmarks For satisfiable benchmarks 8 , m solves 1350 benchmarks across all theories. As expected, this is much higher than the number solved by u, which solves 510 benchmarks, all from the empty theory. Nevertheless, there are 13 satisfiable problems solved by u and not by m, which shows that enumerative instantiation has some orthogonality on satisfiable benchmarks as well. We conclude that enumeration not only has superior performance to MBQI on unsatisfiable benchmarks, but also can be an alternative for satisfiable benchmarks in the empty theory.

Artifact

We have produced an artifact [START_REF] Reynolds | Revisiting enumerative instantiation -Artifact[END_REF] to reproduce the experimental results presented in this paper. The artifact contains the binaries of the SMT solvers CVC4 and Z3, the benchmarks on which they were evaluated, and the running scripts for each configuration evaluated. Detailed instructions are given to perform tests on the various benchmark families with all configurations within the time limits, as well as for retrieving the respective results in CSV format. The artifact has been tested in the virtual machine available at [START_REF] Hartmanns | Figshare[END_REF].

Conclusion

We have presented a strengthening of the Herbrand Theorem, used it to devise an efficient technique for enumerative instantiation. The implementation of this technique in the state-of-the-art SMT solver CVC4 increases its success rate and outperforms existing implementations of MBQI on unsatisfiable problems with quantified formulas. Given its relatively simple implementation, this technique is well poised as an alternative to MBQI for being integrated in an instantiation based SMT solver to achieve completeness in first-order logic with the empty theory and equality, as well as perform improvements also when theories are considered.

Future work includes further restricting the enumeration space, for instance with ordering criteria in the spirit of resolution-based theorem proving [START_REF] Bachmair | Resolution theorem proving[END_REF]. Another direction is lifting the techniques seen here to reasoning in higher-order logic. To handle quantification over functions it is often necessary to enumerate expressions, and so performing such an enumeration in a principled manner is paramount for this domain. Techniques from syntax-guided function synthesis [START_REF] Alur | Syntax-guided synthesis[END_REF] could be combined with enumerative instantiation to pursue this goal.

Fig. 2 :

 2 Fig. 2: Quantifier Instantiation strategies: Conflict-based Instantiation (c), E-matching instantiation (e), Model-based Instantiation (m) and Enumerative Instantiation (u).

Example 1 .

 1 Consider the set of ground literals E = {¬P(a), ¬P(b), P(c), ¬R(b)}. For the input (E, ∀x. P(x) ∨ R(x)), the strategies in this section will do the following. 1. Conflict based: Since E, P(b) ∨ R(b) |= ⊥, this strategy will return {{x → b}}. 2. E-matching: This strategy may choose the singleton set of triggers {(P(x))}. Based on this trigger, since E |= P(x){x → t} ≈ P(t) where P(t) ∈ T(E) for t = a, b, c, this strategy may return {{x → a}, {x → b}, {x → c}}. 3. Model-based: This strategy will construct a model M for E, where assume that P M = λx. ite(x ≈ c, , ⊥) and R M = λx. ⊥. Since M does not satisfy P(a) ∨ R(a), this strategy may return {{x → a}}. 4. Enumerative instantiation: This strategy chooses an ordering on tuples of terms, say the lexicographic extension of where a ≺ b ≺ c. Since E does not entail P(a) ∨ R(a), this strategy returns {{x → a}}.

Example 2 .

 2 Consider the set of ground literals E = {¬P(a), R(b), S (c)} and the quantified clauses Q = {∀x. R(x) ∨ S (x), ∀x. ¬R(x) ∨ P(x), ∀x. ¬S (x) ∨ P(x)} in a monosorted signature. Notice that E ∪ Q is unsatisfiable: it suffices to consider the instances of the three quantified formulas in Q with x → a. On such an input, model-based instantiation will first construct a model for E. Assume this model M is such that P M = λx.⊥, R M = λx. ite(x ≈ b, , ⊥), and S M = λx. ite(x ≈ c, , ⊥). Assuming enumerative instantiation chooses the lexicographic extension of a term ordering where a ≺ b ≺ c. The following table summarizes the result of running the two strategies.ϕ x s.t. M |= ϕ x s.t. E |= ϕ m(E, ∀x. ϕ) u(E, ∀x. ϕ) R(x) ∨ S (x) a a {{x → a}} {{x → a}} ¬R(x) ∨ P(x) b a, b, c {{x → b}} {{x → a}} ¬S (x) ∨ P(x) c a, b, c {{x → c}} {{x → a}} The second and third columns show the sets of possible values of x that are considered with model-based and enumerative instantiation respectively, and the third and fourth columns show one possible selection. The instances corresponding to the three substitutions returned by enumerative instantiation R(a)∨S (a), ¬R(a)∨ P(a) and ¬S (a)∨ P(a) when conjoined with ¬P(a) from E are unsatisfiable, whereas the instances produced by model-based instantiation do not suffice to show that E is unsatisfiable. Hence, the latter will consider an extension of E that satisfies the instances R(a) ∨ S (a), ¬R(b) ∨ P(b) and ¬S (c) ∨ P(c) and guess another model for this extension.

Example 4 .

 4 Say E ∪ Q = {a ≈ b, f (a) ≈ c} ∪ {∀x. P( f (x))},where a, b, c, x are of sort τ, f is a unary function τ → τ, and P is a predicate on τ. It can be shown that

Fig. 4 :

 4 Fig.4: Z3 and CVC4 on unsatisfiable benchmarks with a 300 second timeout.

  E, ∀ x. ϕ ): 1. Either return {σ} where E, ϕσ |= ⊥, or return / 0.

	3. Return n i=1 S i .

c( e( E, ∀ x. ϕ ): 1. Select a set of triggers {t 1 , . . . tn } for ∀ x. ϕ. 2. For each i = 1, . . . , n, select a set of substitutions S i such that for each σ ∈ S i , E |= ti σ ≈ ḡi for some tuple ḡi ∈ T(E). m( E, ∀ x. ϕ ): 1. Construct a model M for E. 2. Return {{ x → t}} where t ∈ T(E) and M |= ϕ{ x → t}, or / 0 if none exists. u( E, ∀ x. ϕ ): 1. Choose an ordering on tuples of quantifier-free terms. 2. Return {{ x → t}} where t is a minimal tuple of terms w.r.t such that t ∈ T(E) and E |= ϕ{ x → t}, or / 0 if none exist.

  replace it by . 4. If is t ≈ s and t ≈ s ∈ E where [t ] = t and [s ] = s, replace it by .

The Herbrand Theorem is generally presented in pure first-order logic without equality, but it also holds for equality: it suffices to consider the equality axioms conjunctively with formulas.

For details, see http://matryoshka.gforge.inria.fr/pubs/fol enumerative inst/

In SMT parlance, the logic of these benchmarks is quantified EUF.

There are technical details that influence the comparison of these techniques (see[START_REF] Reynolds | Revisiting enumerative instantiation[END_REF]).

Number of uniquely solved benchmarks between configurations are available in[START_REF] Reynolds | Revisiting enumerative instantiation[END_REF].

A detailed comparison by families can be seen in[START_REF] Reynolds | Revisiting enumerative instantiation[END_REF].

As a rough estimate, the implementation of enumerative instantiation in CVC4 is around 500 lines of code, whereas model-based instantiation is around 4500 lines of code.

For further details, see[START_REF] Reynolds | Revisiting enumerative instantiation[END_REF].

Data Availability Statement and Acknowledgments

The datasets generated and analyzed during the current study are available in the figshare repository: https://doi. org/10.6084/m9.figshare.5917384

This work was partially funded by the National Science Foundation under Award 1656926, by the H2020-FETOPEN-2016-2017-CSA project SC 2 (712689), and by the European Research Council (ERC) starting grant Matryoshka (713999). We would like to thank the anonymous reviewers for their comments. We are grateful to Jasmin C. Blanchette for discussions, encouragements and financial support through his ERC grant.