Benchmarking of Unification Indexes

This is an online contperpart of the paper "Comparing Unification Algorithms in First-Order Theorem Proving" that I have written in May 2009 together with my supervisor Andrei Voronkov. Due to paper length limit, only a shortened version was submitter. A full version of the paper can be downloaded here.

If you are interested in results and statistics on all about 700 benchmarks that we have generated and evaluated, you can download a spreadsheet here.

If you are going to implement a benchmarking interface for your own indexing technique, you will probably find the following files useful:

  • compit2.cpp - benchmark file parser
  • compit2.hpp - definition of index interface required by the parser.
  • Timer.hpp - a timer class for measuring time spent by indexing. Needed by compit2.cpp.
  • compit2_impl.cpp - an interface of our index. Will not compile as other Vampire source files are neecessary for that, but one can get an idea how to work with the reversed polish notation from that.

    Data files for benchmarks published in the paper can be downloaded here. Data are stored in the little-endian, so on big-endian machines (SPARC, PowerPC), you might need to modify the readWord function in compit2.cpp in order to get the right byte order.

    The presentation from the KI 2009 conference is available here (pdf).

    Contact

    If you have any questions regarding this, feel free to contact me on my email below.