Solver Isomap for QF_IDL

In this diagram two solvers are close if they are similar with respect to their solving times at the competitions. See below for a detailed explanation. The trail connects the annual versions of a solver.

  1. Fetch all the competition results for the given logic.
  2. If requested (it is), remove the solvers that have less than 100 benchmarks in common with 50% of the other solvers.
  3. Compute the distance between each solver pair. It is the cosine distance between the wall-clock time of the common benchmarks. More precisely, when if two solvers have n benchmarks in common, we use an n-dimensional space. The coordinate of each solver is the wall-clock time for each benchmarks regardless of the result. The cosine distance is then the angle between the two solvers at the origin.
  4. Compute a standard Isomap from the cosine distances.

Solvers removed in step 2:

  • Yices 2005 (2005-07-12)
  • Barcelogic 2005 (2005-07-12)
  • HTP 2005 (2005-07-12)
  • MathSAT 2005 (2005-07-12)
  • SVC 2005 (2005-07-12)
  • Sammy 2005 (2005-07-12)
  • ARIO 2005 (2005-07-12)
  • CVC Lite 2005 (2005-07-12)
  • CVC 2005 (2005-07-12)
  • SBT 2005 (2005-07-12)
  • Sateen 2005 (2005-07-12)
  • Yices 2006 (2006-08-21)
  • Barcelogic 2006 (2006-08-21)
  • HTP 2006 (2006-08-21)
  • MathSAT 2006 (2006-08-21)
  • ARIO 2006 (2006-08-21)
  • Sateen 2006 (2006-08-21)
  • CVC3 2006 (2006-08-21)
  • ExtSAT 2006 (2006-08-21)
  • Yices 2007 (2007-07-03)
  • Barcelogic 2007 (2007-07-03)
  • MathSAT 2007 (2007-07-03)
  • Sateen 2007 (2007-07-03)
  • Z3 2007 (2007-07-03)
  • Yices 2008 (2008-07-07)
  • Barcelogic 2008 (2008-07-07)
  • MathSAT 2008 (2008-07-07)
  • Sateen 2008 (2008-07-07)
  • CVC3 2008 (2008-07-07)
  • Z3 2008 (2008-07-07)
  • clsat 2008 (2008-07-07)
  • Yices2 2008 (2008-07-07)
  • Barcelogic 2009 (2009-08-02)
  • MathSAT 2009 (2009-08-02)
  • CVC3 2009 (2009-08-02)
  • Z3 2009 (2009-08-02)
  • clsat 2009 (2009-08-02)
  • Yices2 2009 (2009-08-02)
  • OpenSMT 2009 (2009-08-02)
  • veriT 2009 (2009-08-02)
  • Barcelogic 2010 (2010-07-15)
  • Sateen 2010 (2010-07-15)
  • CVC3 2010 (2010-07-15)
  • OpenSMT 2010 (2010-07-15)
  • veriT 2010 (2010-07-15)
  • MathSAT 2011 (2011-07-14)
  • Yices2 2011 (2011-07-14)
  • OpenSMT 2011 (2011-07-14)
  • veriT 2011 (2011-07-14)