Solver Geometry Heatmaps

These plots have the goal of identifying solvers that are promising because they do something different, that work when other solvers fail, even if they do not achieve the best ranking in a competition.

More preciely, these are heatmap plots of parwise asymmetric distances between the solvers that participated in recent SAT competitions. Given a metric \(m\) such as solved instances or PAR2 score, the asymmetric distance from solver 1 to solver 2 is $$\sum_{i\in\mathrm{instances}} \max(0,m_2(i) - m_1(i))$$, that is the sum of the differences over instances where solver 2 is better than solver 1.

In the plots, solver 1 ("worse") and solver 2 ("better") correspond to columns and rows respectively. This means that we can see by how much a solver beats others by looking at its row, and we can see by how much a solver gets beaten by looking at its column (hover over the plots to see names). Entries are sorted so that the best solver takes the bottom row and the rightmost column.

For instance, in the plots corresponding to 2018, we see how even if the local search solver YalSAT is usually a terrible choice, it is well worth to keep handy in one's toolbox for the not-so-odd case when it beats every other option. We can also see how it is very infrequent for any solver to completely dominate any other solver.

Source: solver_geometry.py.

SAT Competition 2016

Main track

Solved

PAR2

SAT Competition 2017

Main track

Solved

PAR2

SAT Competition 2018

Main track

Solved

PAR2

SAT Race 2019

Main track

Solved

PAR2

SAT Competition 2020

Main track

Solved

PAR2

SAT Competition 2021

Main track

Solved

PAR2

SAT Competition 2022

Main track

Solved

PAR2

SAT Competition 2023

Main track

Solved

PAR2