In SMT solving one generally applies heuristic instantiation to handle quanti ed formulas. This has the side e ect of producing many spurious instances and may lead to loss of performance. Therefore deriving both fewer and more meaningful instances as well as eliminating or dismissing, i.e., keeping but ignoring, those not signi cant for the solving are desirable features for dealing with rst-order problems. This paper presents preliminary work on two approaches: the implementation of an e cient instantiation framework with an incomplete goal-oriented search; and the introduction of dismissing criteria for heuristic instances. Our experiments show that while the former improves performance in general the latter is highly dependent on the problem structure, but its combination with the classic strategy leads to competitive results w.r.t. state-of-the-art SMT solvers in several benchmark libraries.
Heuristic instantiation is kept under control. Given their speed and the di culty of the rst-order reasoning
with interpreted symbols, heuristics are a necessary evil. To reduce side e ects, spurious instances are
dismissed. The criterion is their activity as reported by the ground solver, in a somehow hybrid approach
avoiding both the two-tiered combination of SAT solvers [
We also introduce a lifting of the classic congruence closure procedure to rst-order logic and show its suitability as the basis of our instantiation techniques. Moreover, it is shown how techniques common in rst-order theorem proving are being implemented in an SMT setting, such as using e cient term indexing and performing E uni cation.
Due to space constraints, we refer to the classic notions of many-sorted rst-order logic with equality as the basis for the notation in this paper. Only the most relevant are mentioned.
Given a set of ground terms T and a congruence relation ' on T, a congruence C over T is a set C fs ' t j s; t 2 Tg closed under entailment: for all s; t 2 T, C j= s ' t i s ' t 2 C. The congruence closure of C is the least congruence on T containing C. Given a consistent set of ground equality literals E, two terms t1; t2 are said congruent i E j= t1 ' t2, which amounts to t1 ' t2 being in the congruence closure of the equalities in E, and disequal i E j= t1 6' t2. The congruence class of a given term t, represented by [t], is the partition of T induced by E in which all terms are congruent to t. 2
To better handle the quanti ed formulas during instantiation algorithms we have developed a Congruence Closure
with Free Variables (CCFV, for short), which extends the classic congruence closure procedure [
L; x ' y k U L k U [ fx ' yg
L; x ' t k U L k U [ fx ' tg L; f (u) ' f (v) k U
L; u ' v k U
L; f (u) ' t k U L; f (u) ' f (t1) k U
: : : L; f (u) ' f (tn) k U
L; u ' f (u0) k U L; u ' t1;1; f (u0) ' f (t01) k U
: : : L; u ' t1;m1 ; f (u0) ' f (t01) k U
: : : L; u ' tn;mn ; f (u0) ' f (t0n) k U L k U ? (Close) (Decompose) (Ematch) (i) (ii) (i) (ii) L k U > ' 2 f'; 6'g x or y is free in U , or E [ U j= x ' y ' 2 f'; 6'g either x is free in U or E [ U j= x ' t (Yield) (i)
L = ? or E j= L (i) (ii) (iii) (Euni)
E j= t ' f (ti), for 1 ' 2 f'; 6'g f (ti) are ground terms from E
i n (i) (ii) (iii) ' 2 f'; 6'g ti;j ; f (t0i) are ground terms from E E j= ti;j ' f (t0i), for 1 i n, 1 j
mi (i)
L is inconsistent modulo E or no other rule can be applied
Our procedure implements the rules1 shown in Table 1. To simplify presentation, it is assumed, without loss of generality, that function symbols are unary. Rules are shown only for equality literals, as their extension into uninterpreted predicates is straightforward. The calculus operates on conjunctive sets of equality literals containing free variables, annotated with equality literals between these variables and ground terms or themselves. Initially the annotations are empty, being augmented as the rules are applied and the input problem is simpli ed, embodying its solution.
Given a set of ground equality literals E and a set of non ground equality literals L whose free variables are X, CCFV computes sets of equality literals U1; : : : ; Un, denoted uni ers. Each uni er associates variables from X to ground terms and allows the derivation of ground substitutions 1; : : : ; k such that E j= L i, if any: i = x 7! t x 2 X; U j= x ' t for some ground term t: If x is free in U , t is a ground term selected from its sort class: Since not necessarily all variables in X are congruent to ground terms in a given uni er U (denoted \free in U "), more than one ground substitution may be obtained by assigning those variables to di erent ground terms in their sort classes.
A terminating strategy for CCFV is to apply the rules of Table 1 exhaustively over L, except that Ematch may not be applied over the literals it introduces. There must be a backtracking when a given branch results in Close, until being able to apply Yield. In those cases a uni er is provided from which substitutions solving the given E -uni cation problem can be extracted.
Performing E -uni cation requires dealing with many terms, which makes the use of an e cient indexing technique for fast retrieval of candidates paramount.
The Congruence Closure procedure in veriT keeps a signature table, in which terms and predicate atoms are kept modulo their congruence classes. For instance, if a ' b and both f (a) and f (b) appear in the formula, only f (a) is kept in the signature table. Those are referred to as signatures and are the only relevant terms for indexing, since instantiations into terms with the same signature are logically equivalent modulo the equalities in the current context. The signature table is indexed by top symbol 2, such that each function and predicate symbol points to all their related signatures. Those are kept sorted by congruence classes, to be amenable for binary search. Bitmasks are kept to fast check whether a class contains signatures with a given top symbol, a necessary condition for retrieving candidates from that class.
A side e ect of building the term index from the signature table is that all terms are considered, regardless of
whether they appear or not in the current SAT solver model. To tackle this issue, an alternative index is built
directly from the currently asserted literals while computing on the y the respective signatures. Dealing directly
with the model also has the advantage of allowing its minimization, since the SAT solver generally asserts more
literals than necessary. Computing a prime implicant, a minimal partial model, can be done in linear time [
The main data structure for CCFV is the \uni ers": for a set of variables X, an array with each position representing a valuation for a variable x 2 X, which consists of: a eld for the respective variable; a ag to whether that variable is the representative of its congruence class; a eld for, if the variable is a representative, the ground term it is equal to and a set of terms it is disequal to; otherwise a pointer to the variable it is equal to, the default being itself. 1The calculus still needs to be improved, with a better presentation and the proofs of its properties, which are work in progress. 2Since top symbol indexing is not optimal, the next step is to implement ngerprint indexing. The current implementation keeps the indexing as modular as possible to facilitate eventually changing its structure.
Each uni er represents one of the sets U mentioned above. They are handled with a UNION-FIND algorithm with path-compression. The union operation is made modulo the congruence closure on the ground terms and the current assignments to the variables in that uni er, which maintains the invariant of it being a consistent set of equality literals.
The rules in Table 1 are implemented as an adaptation of the recursive descent E-uni cation algorithm in [
In the classic architecture of SMT solving, a SAT solver enumerates boolean satis able conjunctions of literals
to be checked for ground satis ability by decision procedures for a given set of theories. If these models are not
refuted at the ground level they must be evaluated at the rst-order level, which is not a decidable problem in
general. Therefore one cannot assume to have an e cient algorithm to analyze the whole model and determine
if it can be refuted. This led to the regular heuristic instantiation in SMT solving being not goal-oriented: its
search is based solely on pattern matching of selected triggers [
In [
Since the existence of such substitutions is an NP-complete problem equivalent to Non-simultaneous rigid
E-uni cation [
Currently our implementation applies a breadth- rst search on the conjunction of non-ground literals, computing all uni ers for a given literal l 2 : before considering the next one. Memory consumption is an issue due to the combinatorial explosion that might occur when merging sets of uni ers from di erent literals. A more general issue is simply the time required for nding the uni ers of a given literal, which can have a huge search space depending on the number of indexed terms. To minimize these problems customizable parameters set thresholds both on the number of potential combinations and of terms to be considered. 3.2
Although goal-oriented search avoids heuristic instantiation in many cases, triggers and pattern-matching are still
the backbone of our framework. A well known side e ect of them is the production of many spurious instances
which not only interfere with the performances of both the ground and instantiation modules but also may lead
to matching loops : triggers generating instances which are used solely to produce new instances in an in nite
chain. To avoid this issues, de Moura et al. [
3Since CCFV is non-proof con uent calculus, as choices may need to be made whenever a matching or uni cation must be performed, backtracks are usually necessary for exploring di erent options.
To circumvent this problem, instead of being truly deleted instances are simply dismissed : by labeling them with instantiation levels 4, at a given level n only instances whose level is at most n 1 are considered. This is done by using the term indexing from the SAT model and eliminating literals whose instantiation level is above the threshold. At each instantiation round, the level is de ned as the current level plus one. At the beginning of the solving all clauses are assigned level 0, the starting value for the instantiation level. At the end of an instantiation round, the SAT solver is noti ed that at that point in the decision tree there was an instantiation, so that whenever there is a backtracking to a point before such a mark the instantiation level is decremented, at the same time that all instances which have participated in a con ict are promoted to \level 0". This ensures that those instances will not be dismissed for instantiation, which somehow emulates clause deletion. With this technique, however, the ground solver will still be burdened by the spurious instances, but they also will not need to be regenerated in future instantiation rounds.
: : : ?
I1 ?1 : : :
I2 ?2
I10 : : : : : : I20 ?3
Consider in Figure 1 an example of instance dismissal. I1 marks an instantiation happening at level 1, in which all clauses from the original formula are considered for instantiation. Those lead to a con ict and a backtrack to a point before I1, which decrements the instantiation level to 0. All instances from I1 which were part of the con ict in ?1 are promoted to level 0, the rest kept with level 1. At I10 only terms in clauses with level 0 are indexed. Since subsequently there is no backtracking to a point before I10 , the instantiation level is increased to 1. At I2 all clauses of level 1 are considered, thus including those produced both in I1 and I10 . After a backtrack, the level is decremented to 1 and the instances participating in ?2 are promoted. This way at I20 only the promoted instances from the previous round are considered. Then the ground solver reaches a con ict in ?3 and cannot produce any more models, concluding unsatis ability. 4
The above techniques have been implemented in the SMT solver veriT [
The di erent con gurations of veriT are identi ed in this section according to which techniques they have
activated:
veriT: the solver relying solely on nave trigger instantiation;
veriT i: the solver with CCFV and the signature table indexed;
veriT ig: besides the above, uses the goal-oriented search for con icting instances;
4This is done much in the spirit of [
5A development version is available at http://www.loria.fr/~hbarbosa/veriT-ccfv.tar.gz veriT igd: does the term indexing from the SAT solver and uses the goal-oriented search and instance dismissal.
Our new implementations were also evaluated against the SMT solvers Z3 [
While veriT ig and veriT igd solve a similar number of problems in the same categories (with a small advantage to the latter), it should be noted that they have quite diverse results depending on the benchmark (a comparison is shown in Figure 4 at Appendix A). Each con guration solves 150 problems exclusively. This indicates the potential to use both the term indexes, from the signature table and from the SAT solver model with instance dismissal, during the solving.
Regarding overall performance, CVC4 solves the most problems, being the more robust SMT solver for instantiation and also applying a goal-oriented search for con icting instances. Both con gurations of veriT solve approximately the same number of problems as Z3, although mostly because of the better performance on the sledgehammer benchmarks, which have less theory symbols. There are 124 problems solved by veriT igd that neither CVC4 nor Z3 solve, while veriT ig solves 115 that neither of these two do.
Figure 3 shows how the better veriT con guration, with the goal-oriented search and instance dismissal, performs against the other solvers. There are many problems solved exclusively by each system, which indicates the bene t of combining veriT with those systems them in a portfolio when trying to quickly solve a particular problem: while CVC4 alone solves 92% of the considered benchmarks in 30s, by giving each of the four compared systems 7s is enough to solve 97% of them.
10 0.1 0.1 1 veriT_igd
10 (a) Z3 vs veriT igd 10 0.1 1 veriT_igd
10 (b) CVC4 vs veriT igd
There is still room for improvement in our instantiation framework. Particularly, a better understanding of the instance dismissal e ects is still required. Further analyzing the clauses activity would lead to a more re ned promotion strategy and possibly better outcomes. Nevertheless, we believe that our preliminary results are promising.
Regarding the term indexing, besides improving the data structures our main goal is performing it incrementally : by indexing the literals from the SAT model it is not necessary to thoroughly recompute the index at each instantiation round. It is su cient to simply remove or add terms, as well as update signatures, according to how the model has changed. The same principle may be applied to the memoization of \uni cation jobs": an incremental term index would allow updating the resulting uni ers accordingly, signi cantly reducing the instantiation e ort over rounds with similar indexes.
Our goal-oriented instantiation has a very limited scope: currently con icting instances can only be found
when a single quanti ed formula is capable of refuting the model. As it has been shown in [
Applying di erent strategies in a portfolio approach is highly bene cial for solving more problems, but it could
be even more so if di erent con gurations were to communicate. Attempting pseudo-concurrent architectures
such as described in [
I would like to thank my supervisors Pascal Fontaine and David Deharbe for all their help throughout the development of this work and comments on the article.
Experiments presented in this paper were carried out using the Grid'5000 testbed, supported by a scienti c interest group hosted by Inria and including CNRS, RENATER and several Universities as well as other organizations (see https://www.grid5000.fr). veriT_ig
10