Efficient Implementation of Large-Scale Watchlists

           Constantin Ruhdorfer and Stephan Schulz

In this work, we explore techniques for improving the performance of
the automated theorem proving system E when dealing with large
\emph{watchlists}. A watchlist can focus the proof search towards
so-called \emph{hints}, likely useful intermediate results provided
externally. Recently, hints have been automatically extracted from
previous proofs, creating massive watchlists and thus making
evaluation of new clauses against the wachtlist a performance
bottleneck.  We introduce a new index for the frequent special case of
unit clause hints, taking advantage of the fact that subsumption can
be implemented much more efficiently for unit clauses than for the
general case.  We implement several strategies for exploiting the
structure and properties of equational unit clauses.  Additionally, we
have added a new \emph{soft subsumption} mechanism to E that can
abstract away differences of constant or Skolem symbols, effectively
allowing a less precise match when evaluating a given clause against
the watchlist.  We have tested the new mechanisms on a large set of
problems taken from the Mizar 40 project, using a large watchlist
containing over 300~000 clauses. We show that the usage of the unit
clause index significantly increases performance with this given
watchlist. The use of soft subsumption shows more mixed results. We
believe that most watchlists can take advantage of these techniques
and have made them available to the user via E's command line
interface.