Solver Isomap for QF_DT

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:

• CVC4 2017 (2017-07-23)
• Z3 2018 (2018-07-14)
• CVC4 2018 (2018-07-14)
• Alt-Ergo 2019 (2019-07-07)
• CVC4 2019 (2019-07-07)
• Z3 2020 (2020-07-06)
• Alt-Ergo 2020 (2020-07-06)
• CVC4 2020 (2020-07-06)
• Z3 2021 (2021-07-18)
• SMTInterpol 2021 (2021-07-18)
• Z3 2022 (2022-08-10)
• cvc5 2022 (2022-08-10)
• Z3 2023 (2023-07-06)
• SMTInterpol 2023 (2023-07-06)
• cvc5 2023 (2023-07-06)
• SMTInterpol 2024 (2024-07-22)
• cvc5 2024 (2024-07-22)
• Z3alpha 2024 (2024-07-22)
• Algaroba 2024 (2024-07-22)