Clause selection is one of the main heuristic decision points in navigating proof search of saturationbased theorem provers. A recently developed layered clause selection framework allows one to boost a basic clause selection heuristic by organising clauses into groups of more or less promising ones according to a specified numerical feature. In this work, we investigate this framework in depth and introduce, in addition to a previously presented feature (based on the amount of theory reasoning in the derivation of a clause), three new features for clause selection (tracking relatedness to the goal, the number of split dependencies in the Avatar architecture, and closeness to the Horn fragment, respectively). We implemented the resulting clause selection heuristics in the state-of-the-art saturation-based theorem prover Vampire and present an evaluation of these new clause-selection strategies and their combinations over the TPTP and SMTLIB libraries.
In the context of automated theorem proving, saturation refers to the process of iteratively
deriving (according to a particular inference system) logical consequences of a set of given input
clauses until the empty clause is derived, which witnesses unsatisfiability. Modern
saturationbased theorem provers for first-order logic typically employ some variant of a given-clause
algorithm, in which clauses are selected for inferences one by one [
The standard technology for implementing clause selection heuristics relies on two concepts. First, certain numerical clause evaluation criteria are identified, such as the number of symbols in a clause (a.k.a. clause weight) or the iteration when the clause was derived during search (a.k.a. clause age1), such that a small clause in terms of the given criterion is more likely to lead to a refutation than a large one. The prover then maintains a priority queue for each criterion for the eficient extraction of “the current best clause”. Second, the prover alternates picking clauses from these priority queues using a specified ratio. For example, a heuristic may specify that every 10 selections, the prover should pick 9 clauses that are small by weight, i.e. light, and one clause that is small by age, i.e. old.
A recently developed layered clause selection framework [
In [
Finally, 3) we present the results of extensive experiments with the new heuristics over TPTP and SMTLIB and a specific set of benchmarks coming from program verification (Section 7).
We assume the reader to be familiar with the main ideas behind saturation-based theorem
proving [
The de facto standard clause selection heuristic used in modern saturation-based theorem provers is the age-weight clause selection heuristic.
Definition 1 (Age-weight clause selection heuristic). For any clause , define the age age() as the depth of the derivation tree of 2 and define the weight weight() as the number of symbols3 of . Let further : be a list of two positive integer values. Then the age-weight clause selection heuristic aw( : ) alternates between selecting a clause with the smallest age age() and selecting a clause with the smallest weight weight() using the ratio : .
The basic understanding of age-weight selection is that it performs a blend between the breadth-first and the best-first search paradigms. Clauses of small weight are considered better, because they are closer to the ultimate goal—the empty clause of weight zero—than the larger ones. They also tend to produce small clauses as children, on average serve as stronger simplifiers, and are computationally cheaper to process. The age criterion, on the other hand, corresponds to the breadth-first aspect and helps to ensure fairness under which no generated clause (unless shown redundant) waits too long before getting selected.
Definition 2 (Split heuristics). Let be a real-valued clause evaluation feature such that preferable clauses have low value of (), and let the cutofs 1, . . . , be monotonically increasing real numbers with = ∞. Furthermore, let the ratio 1 : . . . : be a list of positive integer values, and let finally be an arbitrary clause selection heuristic.
A split heuristic groups clauses into sets 1, . . . , , and selects clauses by alternating selection from 1, . . . , using the ratio 1 : . . . : . The selection from each such set is performed using . We define two modes of split clause selection heuristic, which difer in how they group clauses: • The monotone split heuristic mono-split(, 1, . . . , , 1 : · · · : , ) uses sets := { | () ≤ } for = 1, . . . , . • The disjoint split heuristic disj-split(, 1, . . . , , 1 : · · · : , ) uses sets 1 := { | () ≤ 1}, and := { | − 1 < () ≤ } for 2 ≤ ≤ .
Example 1. Consider the clause selection heuristic mono-split(, 0, 1, ∞, 3 : 1 : 1, (1 : 1)). This heuristic will select 3 out of 5 times a clause such that () ≤ 0, 1 out of 5 times a clause such that () ≤ 1, and 1 out of 5 times an arbitrary clause. On “layer one”, e.g., 3 out of 10 times the clause with the smallest age among the clauses with () ≤ 0 is selected, or 1 out of 10 times the clause with smallest weight out of all clauses is selected.
2This corresponds to how age is defined in Vampire. More precisely still, one uses only the depth with respect to generating inferences. Reductions do not alter the age of a reduced clause.
3Including multiplicities. As a variation, diferent kinds of symbols (such as the variables, the predicate symbols,
or the constants) may weigh more than others [
Split heuristics allow to adapt an existing clause selection heuristic to take into account the clause feature . We now discuss how to pick the mode, the cutofs, and the ratios. We observed two kinds of clause features:
First, there are features where clauses with low feature value are more likely to contribute to the proof search (this is the case for the features distth, distSInE, and distHorn, discussed in Section 3, Section 5, resp. Section 6). For features of this kind, one should use a monotone split heuristic. A good starting point for cutofs and ratios is 1, ∞ and 1 : 1, resp., where 1 is the feature value we expect to obtain for the empty clause ⊥ (based on domain knowledge and experience). One can extend the cutofs by introducing one or two additional cutofs close to 1, in order to smooth the transition between 1 and ∞, and extend the ratio accordingly. It can also make sense to vary the ratio, although in our experience, it is more important to identify good cutofs, than to fine-tune the ratio.
Secondly, there are features where clauses with low feature value are not necessarily more likely to contribute to the proof search, but are less likely to have low weight (this is the case for the feature distAV discussed in Section 4). As a consequence, it does not make sense to compare clauses, which have diferent feature values, by weight. In such a case, one can use a split heuristic in disjoint mode. Varying the cutofs and ratios of disjoint split heuristics has a less predictable efect than for the monotone split heuristic and needs to be fine-tuned on a case-by-case basis.
As split heuristics are parameterized by an arbitrary clause selection heuristic, we are able to build clause selection heuristics containing nestings of split heuristics. Such clause selection heuristics are powerful, as they allow us to easily combine diferent features.
mono-split( 1, 0, 1, ∞, 15 : 4 : 1, mono-split( 2, 1, ∞, 5 : 1,
(1 : 1))).
The resulting clause groupings and frequencies to pick from these groups are visualized in Figure 1. The nested split heuristics form a tree. Each leaf node of the tree represents a set of clauses, from which clauses are selected using (1 : 1). We can see that the leftmost leaf node of the tree represents all clauses with 1() ≤ 0 and 2() ≤ 1. We pick clauses from this leaf using (1 : 1) in 15/20 · 5/6 = 5/8 of the cases.
Note that each split heuristic ℎ provides a horizontal dimension consisting of the groups of ℎ. The nesting of diferent split heuristics itself provides a vertical dimension.
In this subsection we briefly discuss how to implement clause selection heuristics. As typical runs of saturation algorithms can include several million clause selections, we strive to implement these heuristics eficiently. 15/20
1/20 all clauses 4/20 1() ≤ 1 5/6 1/6
all clauses 5/6 1/6 1() ≤ 0 2() ≤ 1 1() ≤ 0 1() ≤ 1 2() ≤ 1
An -heuristic with ratio : ℎ can be implemented as a container as follows. The container internally keeps two priority queues4 , , where both and store all the clauses of , keeps its clauses ordered by age and keeps its clauses ordered by weight. The container determines whether it should select the next clause from or ℎ using a weighted round-robin scheme with ratio : , and selection from the chosen queue proceeds by popping the first element (i.e. a clause) from that queue and deleting the corresponding record (of that clause) from the other queue.
The heuristic mono-split(, 1, . . . , , 1 : · · · : , ), resp. disj-split(, 1, . . . , , 1 : · · · : , ), can be implemented as a container SH as follows. Assume that is implemented using a container CS. The container SH keeps instances CS1, . . . , CS of CS, where container CS contains all clauses of group of SH. The container SH determines from which of the subcontainers CS1, . . . , CS it should select the next clause using a weighted round-robin scheme with ratio 1 : · · · : and then delegates clause selection to that CS.
We believe that the nesting of split heuristics is a great conceptual tool for composing independent ideas on how to improve clause selection into a single compound heuristic. This can be already seen with the two layers, where the time-tested age-weight selection serves as a building block for more powerful refined heuristics, and can get further pronounced with additional nestings, as demonstrated by our experiments (see Section 7).
Nevertheless, in retrospect it is not hard to see that computationally, the layered scheme
can be essentially “compiled down” to multiple level-one queues. More precisely, one needs
an extension of the typical level-one queue arrangement, such as the one implemented in E
[
be able to set up a clause queue to only contain those clauses that satisfy a given property . Such property could be, e.g., () = 1() ≤ 0 ∧ 2() ≤ 1 to define the age and weight level-one queues corresponding to the left-most leaf in Figure 1. The reason why clause queue content filtering has until now not been used (to the best of our knowledge) in saturation-based provers is probably that in the standard perspective each clause queue is meant to provide an independent view of the whole set of passive clauses and not just a subset thereof (which would complicate reasoning about completeness if left further unconstrained).5
Recently, saturation-based theorem provers have increasingly been used to reason about
problems requiring quantified theory reasoning [
In the remainder of this section, we give an extended presentation of the solution to this
challenge already presented in [
We start by formalizing the amount of theory reasoning in the derivation of a clause as the ratio of the number of theory axioms and the number of all axioms in the derivation-DAG of . Computing these numbers exactly for the derivation of each clause is potentially expensive, since it requires for each clause a traversal of the derivation-DAG of the clause. We instead approximate those numbers by treating the derivation-DAG as a tree, for which we can compute the numbers using running sums, as follows: Definition 3. For a theory axiom , define both thAx() and allAx() as 1. For a non-theory axiom , define thAx() as 0 and allAx() as 1. For a derived clause with parent clauses 1, . . . , , define thAx() as ∑︀ thAx() and allAx() as ∑︀ allAx(). Finally, we set frac() := thAx()/allAx().
5We note that clause priority functions of E [
With these notations at hand, we identify proofs that only need a small amount of theory reasoning with the proofs where frac(⊥) is at most 1/, for some small positive integer value (⊥ here denotes the empty clause).
Next, we present a clause feature distth which approximates the likeliness that a given clause occurs in a proof where frac(⊥) is at most 1/. The clause selection feature distth is parameterized by the value and measures the number of non-theory axioms which the derivation of would need to contain additionally in order to achieve a ratio of at most 1 : . Definition 4. Let be a positive integer value. Then distth : Clauses → N is defined as distth() := max(thAx() · − allAx(), 0).
The feature distth satisfies several properties, which we think are favorable: (i) if the derivation of a clause consists only of several axioms, then distth() is small, (ii) if derivations of clauses 1, 2 are combined into a derivation of clause , and if both distth(1) > 0 and distth(2) > 0, then distth() > distth(1) and distth() > distth(2), and (iii) if derivations of clauses 1, 2 are combined into a derivation of clause , and if frac(1) = 1/, then distth() = distth(2). Note that frac itself does not fulfill these properties.
Example 3. Consider a clause 1, such that thAx(1) = 3 and allAx(1) = 5. Consider further a clause 2, such that thAx(2) = 100 and allAx(2) = 200. Intuitively, 1 is much more likely to occur in a proof with frac(⊥) = 1/4. We have distt4h(1) = 7 < 200 = distt4h(2), but frac(1) = 0.6 > 0.5 = frac(2).
Finally, we are able to construct a clause selection heuristic, which addresses the challenges presented at the beginning of this section, using the split heuristic from Section 2.2 as mono-split(distth, 1, . . . , − 1, ∞, 1 : · · · : , ), where is the positive integer such that 1/ is the expected fraction of the proof which we want to find, is some clause selection strategy, 1, . . . , − 1, ∞ are cutof values, and 1 : · · · : is a ratio. In our experience, varying has a bigger efect than varying cutofs and ratios, and setting to 8 is a reasonable starting point for fine-tuning . In our experiments, other useful values of were between 4 and 50.
AVATAR [
While the exact details of how AVATAR works are out of the scope of this paper, the key aspect important here is easy to explain. First-order clauses in AVATAR need to keep track of the dependencies on splits from which they were derived. This is done by assigning to each clause a set of dependencies , denoted ← , where a dependency ∈ is some identifier of a performed split registered elsewhere in the architecture. Clauses from the input have their dependency set initialised as empty and the dependency set of a derived clause is computed as the union of the dependencies of its parents. Then, when a clause such as 1 ∨ 2 ← is split, with 1 and 2 variable-disjoint, the prover may continue reasoning with 1 ← ∪ {[1]} where [1] is the identifier of the dependency on the performed split. Intuitively, each dependency ∈ is a choice point for which the prover might need to consider alternatives in the future. This means that a clause with many dependencies corresponds to a logically weaker fact than a clause with fewer ones.
Because the basic setup of AVATAR is oblivious to the size of the dependency set of a clause, there is a danger of a strong preference for clauses of small weight (which arise easily with splitting) that nevertheless depend on many splits and are therefore not the best for closing the overall search fast. In order to potentially mitigate this efect, we propose here to use the size of the dependency set of a clause, distAV( ← ) = | |, as a feature for split heuristics.
We then construct a clause selection heuristic using the split heuristic from Section 2 as disj-split(distAV, 1, . . . , − 1, ∞, 1 : · · · : , ), for a given clause selection function , cutofs 1, . . . , − 1, ∞ and ratio 1 : · · · : .
The Sumo Inference Engine (SInE) [
So far, we defined SInE-levels only for the input axioms and the goal. To be able to use them as a feature of general clauses in proof search, we further define distSInE() of a derived clause as the minimum of distSInE() over the parents of . While the choice of the minimum operation may appear arbitrary, note that it has the nice property that distSInE() = 0 if and only if has a goal among its ancestors. This is an important “flag” of a clause, typically tracked by a theorem prover for use in various goal-directed heuristics, and SInE-levels therefore naturally generalise this flag. Finally, we derive a clause selection heuristic using the split heuristic from Section 2 as mono-split(distSInE, 1, . . . , − 1, ∞, 1 : · · · : , ), for a given clause selection function , cutofs 1, . . . , − 1, ∞ and ratio 1 : · · · : . For instance, we can use cutofs 0, ∞ and ratio 1 : 2 to ensure that from 2 + 1 clauses at least one clause is selected which has a goal among its ancestors.
Saturation-based theorem provers are known to work well on benchmarks where each axiom is a Horn clause, that is, a clause with at most one positive literal. We would like to extend the eficiency of these provers to problems which are nearly Horn, in the sense that there exists a proof of the conjecture of the problem, where the number of positive literals for each clause is small. We can formalize this as follows: The Horn-distance distHorn() is defined as where posLits() denotes the number of positive literals of . For a given proof define distHorn() := (posLits() − 1, 0), distHorn( ) :=
∑︁ clause in distHorn().
We claim that for many application domains, most examples are provable using a proof with a small Horn-distance. But if we run a saturation-based theorem prover on such a problem, it can still generate a lot of consequences which contain several positive literals. Such consequences would typically be classified as highly unlikely to contribute to the refutation by human inspection.
We are able to guide clause selection towards finding proofs with small Horn-distance by instantiating the split heuristic from Section 2 as
disj-split(distHorn, 1, . . . , − 1, ∞, 1 : · · · : , ), for a given clause selection function , cutofs 1, . . . , − 1, ∞ and ratio 1 : · · · : .
We implemented the heuristics described in Sections 3–6 in the state-of-the-art theorem prover
Vampire (version 4.4) [
We evaluated the extended implementation of Vampire on two sets of problems coming
from the TPTP library [
Our experiments were run on our local server with two Intel Xeon Gold 6140 Processors (i.e., with 72 processor threads) and 188GB RAM. We were running 30 instances of Vampire in parallel with no other significant load on the server. To obtain a baseline strategy, denoted as base, we modified the default Vampire strategy (which uses Avatar) to use the Discount saturation loop (for stability of results6) and the clause selection heuristic (1 : 10) (which in our experience leads in Vampire to a good performance with Discount). All other tested strategies extend base by applying one or more split heuristics for clause selection on top of this setup. With the exception of Experiment 4 we used a time limit of 10 s per problem.7
Searching for good values of the cutofs, the ratio and other parameters of split heuristics is
rewarding, but requires some experience and a certain amount of experimental “tuning”. In
our previous work on layered clause selection [
Table 1 assigns a tag, typeset in the typewriter font, to each of our four heuristics when understood as Vampire options used for defining a strategy. Thanks to the possibility of nesting split heuristics, these options can be turned on and of independently from one another. Although a particular fixed order is employed in Vampire to build up the nestings (namely the order, from inside out: th, av, sl, pl), we use the operator + to denote possible combinations to suggest that this order is actually irrelevant for the proof search (cf. Section 2.5).
The results of the first experiment are shown in Table 2, separately for TPTP and for SMTLIB.
We observe that in the case of TPTP all the four new heuristics lead to an improvement in
the number of solved problems. This is easiest to see from the always positive column Δbase,
which shows the diference of the number of problems solved between the current strategy and
6The default Limited Resource Strategy [
7A list of the selected problems along with other information needed to reproduce our experiments can be found at https://github.com/quickbeam123/LCS4SbTP-materials. base. The same success is not fully repeated on SMTLIB where th shows a great improvement, but av performs worse than base. (Note that we did not run sl on SMTLIB, since the format used in the library does not support specifying the goal.8)
It should be pointed out that even a strategy which does not improve over base in terms of the number of solved problems could be valuable for the potential participation in strategy schedules, because of the problems it solves uniquely (as reported in the last column in the tables). For another view of this efect, the last line in the two tables shows the number of problems solved by at least one of the listed strategies, again also compared against base. We can see that the use of split heuristics allows us to solve almost 1200 TPTP problems (and more than 3200 SMTLIB problems) not solved by base.
When looking in Table 2 at the performance of the combination of the four heuristics (strategy th+av+sl+pl) one can ask why it does not get better at achieving a combined benefit of its constituents. In Experiment 2, we look at this trend closer and especially try to estimate how much time is typically spent on computing the clause selection heuristic and how this depends on the number of heuristics combined.
The report in Table 3 is based on TPTP runs of all the 16 possible strategies which combine between zero to four of the heuristics introduced in this paper. The middle part of the table reports on their performance in terms of the number of solved problems and is comparable to (in fact, a super-set of) the results in Table 2 (left). One can notice here that combinations indeed sometimes do not outcompete their constituents. E.g., *+av+pl is always worse than just *+pl, which could indicate some unfavourable interactions of the two heuristics. (We leave a more detailed study of this phenomenon for future work.)
Our main focus in this experiment, however, is on the right part of the table. There, we took
the runs on those problems which none of the strategies could solve9 (i.e., on which they ran
for the full 10 s) and measured how much time was spent (on average) on interacting with the
passive clause container (this includes insertions, deletions and the popping of the selected
8There is, however, interesting work on “guessing the goal” for SMTLIB problems [
9There were 7808 such problems. clauses). This average time is reported in the last column, from which we can see that, indeed, the more complex combined strategies are more expensive to execute.
Additionally, for comparison, the #queues column in the table reminds us how many “layer one” clause queues each strategy maintains (recall Section 2.3 and the number of “horizontal” splits each heuristic uses, as shown in Table 1). The multiplier (*2) corresponding to av and pl is rendered in brackets, because these two heuristics use the disjoint split mode. This means that when deciding on distAV (or distHorn), each clause is strictly inserted only into one of two possible sub-containers (rather than possibly to more than one, as with the monotone mode). Correspondingly, the strategies are clearly separated into four groups in terms of average interaction time, where the monotone splits of sl and th are the costly ones (and maintaining the 4 queues of th costs more than the 3 queues of sl) whereas the disjoint split of the other two heuristics does not seem to be adding any measurable overhead.
We remark that the reported average times are not directly proportional to speed of clause processing as each run was terminated after 10 s no matter how many selections were performed. Moreover, quite diferent search spaces could have been traversed by each of the strategies.
In this section, we shed some light on how the performance of our heuristics varies under
the two possible modes of split and under changing the ratios. We focus here on the
SInElevels, AVATAR-splits, and the number of positive literals, referring the reader to [
Although we do not spend much efort on exploring the multi-value “horizontal” splits (since the risk of overfitting to the benchmark increases, and the parameter space becomes both too large to sample eficiently and hard to visualise), we explain how we discovered the successful default for sl with cutofs (0, 1, ∞) and suggest a multi-value cutof setting for pl. Tuning SInE-levels Figure 2 shows the result of varying the ratio while splitting on distSInE with the cutofs (0, ∞). We can observe that with distSInE, the monotone mode is clearly more successful than the disjoint one.
For a comparison, the figure also includes marks for the base strategy and the base strategy
enhanced by setting the non-goal weight coeficient (nwc) to values 2.0, 5.0, and 10.0. Changing
the non-goal weight coeficient is a diferent way of making clause selection goal oriented
which relies on multiplying the weight of each clause not derived from the goal by the given
nwc, making it artificially larger and thus less likely to be selected [
The method we used to further improve the SInE level split heuristic is as follows. We took the best ratio 1 : 5 for the monotone split as shown in Figure 2. Let us recall that this strategy tries to select once out of every 6 selections a clause with distSInE() ≤ 0, the remaining 5 selections being unconstrained by distSInE. After adding a second cutof (of value 1), we can speculate how to split these 5 selections into those with distSInE() ≤ 1 and the remaining, again unconstrained ones. This led us to an experiment with the fixed cutofs (0, 1, ∞) and the varied ratios 1:4:1, 1:3:2, 1:2:3, and 1:1:4, and with the resulting number of problems solved: 9112 (+4 over base), 9410 (+302), 9512 (+404), and 9501 (+393), respectively. Based on this experiment we selected the cutofs (0, 1, ∞) and ratio 1:2:3 as the default for sl.10 Tuning AVATAR-splits Figure 3 visualizes the changes in performance when varying the ratios for the AVATAR-based split heuristic with the distAV() ≤ 0 cutof and compares them to base. We can see that the trends are similar for TPTP and SMTLIB and that here the highest values are reached for the disjoint mode of split. Although the best ratio on TPTP is 2:3, we chose the ratio 1:1 for the default in av given its much better performance on SMTLIB. Tuning the positive literals feature The situation with the positive literals feature is a bit harder to understand. Let us first have a look at the distHorn() ≤ 0 cutof, i.e. the perspective in which the “good” clauses are the clauses with no positive literals.
The performance development for this setup is visualised in Figure 4, again both for TPTP (left) and SMTLIB (right). Here, the two behaviours are quite diferent. Most notably, the disjoint mode, which we selected for the default of pl, is only dominant for SMTLIB, whereas for TPTP, better values can be achieved with the monotone mode. Moreover, the monotone mode on TPTP remains to be very successful (as compared to base) for up to high values of the ratio. In contrast, on SMTLIB the performance of the monotone mode is close to that of base from the ratio 1:5 onwards (and reaches it “from below” with the smaller values). Note that for the monotone mode, increasing in a ratio 1: efectively converges to turning the heuristic of. This makes the observation that this mode is still very successful on TPTP for the ratio 1:30 even more surprising. We currently do not have a good explanation for this phenomenon.
Let us with Figure 5 move on to the distHorn() ≤ 1 cutof, under which we recognise as “good” those clauses that have at most one positive literal. This “Horn fragment” perspective is 10Table 2 reports a slightly diferent number of solved problems for the default sl. The variation, i.e., the 9512 vs 9525 solved problems, is an artefact of rerunning the experiment (in an inherently non-deterministic environment) whose magnitude should be taken into account when interpreting the results in this whole section. both for TPTP and for SMTLIB dominated by the monotone mode of split. When looking at the actual number of problems solved, however, we observe that on neither of the two benchmarks is the improvement over base as pronounced as for the distHorn() ≤ 0 cutof. The best measured improvement for SMTLIB is +78 problems over base achieved for the ratio 1:1. On TPTP, we gain +103 problems over base with the ratio 6:1.
We used the same strategy for extending a good ratio from one non-trivial cutof to two as with the SInE-levels. Focusing on the TPTP benchmark, which seems to be more “responsive” to the heuristic based on positive literals, we started from the successful ratio 1:20 from the distHorn() ≤ 0 cutof with the monotone mode of split and tested variations in which the 20 selections are distributed between a certain amount of those with distHorn() ≤ 1 and the remaining, unconstrained ones. This way, we tested strategies with the cutof (0, 1, ∞) and ratios 1:15:5, 1:16:4, 1:17:3, 1:18:2, and 1:19:1, obtaining, respectively, 9365, 9383, 9368, 9368, 9277 problems solved. The best of these, 1:16:4, improves over the 1:20-ratio (0, ∞)cutof monotone-mode strategy by additional 87 problems. For comparison, however, this new strategy does not fare very well on SMTLIB, where it scores 181 fewer problems than base. Our tentative conclusion from tuning the positive literals feature is that the ensuing “Horn fragment” perspective is not very useful for improving the performance on SMTLIB.
A recent stream of work (started in [
These encodings are extremely challenging, since they include quantifier alternations and quantified theory reasoning over both integers and diference logic and require proofs of nontrivial size. We conjecture that the key ingredient to reason in this domain eficiently is to equip the prover with domain-specific knowledge: From experience we know that proofs in this domain require only light-weight theory reasoning and light-weight reasoning with case distinctions. We furthermore know that it pays of to explore consequences related to the conjecture. Our work measures the amount of theory reasoning in a derivation of a clause using distth, measures the amount of case-distinctions in a derivation of a clause using distHorn, and keeps track of whether the conjecture occurred in the derivation of a clause using distSInE. We therefore are able to use nested split-heuristics with those features to guide proof search on these examples.
As a third experiment, we investigated the efect of guiding proof search using nested split
heuristics with features distt8h, distHorn, and distSInE on 103 benchmarks obtained from
unpublished work extending and improving [
aw(1 : 1)))),
consisting of three nested monotone split heuristics with features distt8h, distHorn and distSInE,
where the cutofs and ratios of the split heuristics are varied in the portfolio. For each
configuration, we imposed a timeout of 60 s. The results of the experiment are listed in Table 4. While
Vampire was only able to prove 18 out of 103 examples with aw, it was able to prove 78 out of
103 examples while using split-heuristics. These results are significant, and suggest that
adding domain-specific knowledge using clause selection heuristics based on the split heuristic
is a key ingredient to eficient automation of the challenging software verification benchmarks
obtained from extensions of [
We investigated the framework of layered clause selection and split heuristics for clause selection and generalized it to support arbitrary nestings and both disjoint and monotone groups. We then revisited the existing feature distth and introduced three new features distAV, distSInE, and distHorn. Finally, we instantiated the framework of split heuristics with these four features and presented a thorough experimental evaluation. Our results suggest that split heuristics heavily improve the performance for both general domains as well as for a specific application to software verification.
Bernhard Gleiss was supported by the ERC Starting Grant 2014 SYMCAR 639270, the ERC Proof of Concept Grant 2018 SYMELS 842066, and the Austrian FWF research project W1255-N23. Martin Suda was supported by the ERC Consolidator grant AI4REASON no. 649043 under the EU-H2020 programme and the Czech Science Foundataion project 20-06390Y.
We thank the anonymous reviewers for their useful comments and suggestions. We also thank Sibylle Ortner for a careful proofreading of a preliminary version of this paper.