Winners of the SAT Competition from 2002 - 2020

This page describes how we selected the winners of SAT competition for our show-case plots on the progress of SAT solving feature at the Kissat webpage.

We selected winners of the SAT competitions, races and one challenge from 2002 until 2019 based on the following criteria. First if there was seperation between crafted or handmade benchmarks from industrial or application benchmarks, then we always picked the industrial or application track winner. We did not include portfolio solvers nor parallel solvers. If there were two stages or phases in the competition we picked the winners of the second phase. With these criterias the selection was pretty straight forward, except for 2019, 2012, 2004, 2003, and 2002.

In 2019 'CaDiCaL' solved more instances than the winner but with a lower score. On our slower cluster 'CaDiCaL' solved less instances than the winner from 2019. Thus we sticked to the winner.

In 2012 the 2011 version of 'Lingeling' was running "hors concours". Thus we selected the 'glucose' solver, which was the fastest non-portfolio solver. Note, again that we ignored portfolio solvers.

In 2004 (see Table 1 on page 8 of the competition proceedings), 'Forklift' comes first before 'zchaff_rand'. Unfortunately we could not get hold of Forklift. We only have access to a binary of its predecessor 'Berkmin561'. We neither have much information about 'zchaff_rand'.

We decided to include the second cleaned up version of 'zchaff' from 2004 available on the 'zchaff' page. The relation of that version to the 'zchaff_rand' and 'zchaff' versions used in the competition in 2004 is unclear though. But it completes the picture.

Already in 2003 (see Fig.1 on page 8 of the competition paper) 'Forklift' dominated, followed by 'Berkmin561' (banner says dated to October 2002) and 'siege' (version v1 according to the authors siege home page). We only have binaries for 'Berkmin' and 'siege' and thus decided to choose 'Berkmin' (it solved one instance more).

Note that the 2002 version of 'zchaff' available from the authors webpage, which apparently took also part in the competition, shows discrepancies even after porting some of the fixes from the 2004 and 2007 version. The 2002 version we were running produced two discrepancies, all claimed by 'zchaff' to be 'satisfiable', while two of them are provably 'unsatisfiable'. All 9 models produced by that 'zchaff' version are incorrect. Therefore we do not include that version for the offical plot but use 'Limmat' instead.