A Time Leap Challenge for SAT Solving

TL;DR

This paper compares the effects of hardware and algorithm improvements on SAT solving over two decades, revealing that algorithmic progress is as impactful as hardware advancements.

Contribution

It provides a systematic comparison of old and new SAT-solvers and hardware, highlighting the significance of algorithmic improvements in SAT solving.

Findings

Algorithmic progress matches hardware improvements in impact.

Modern SAT-solvers outperform older ones on new hardware.

Hardware advancements alone do not fully explain SAT solver performance gains.

Abstract

We compare the impact of hardware advancement and algorithm advancement for SAT solving over the last two decades. In particular, we compare 20-year-old SAT-solvers on new computer hardware with modern SAT-solvers on 20-year-old hardware. Our findings show that the progress on the algorithmic side has at least as much impact as the progress on the hardware side.