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.
arXiv comments
Authors' version of a paper which is to appear in the proceedings of CP'2020
Linked by 3 identifiable commenters in 3 comments across 3 threads, from Feb 2022 to Aug 2025. Found in 2 HN submissions from Sep 2020 to Sep 2020. Open submission discussions.
The difference is that SAT/SMT solvers have primarily relied on single-threaded algorithmic improvements [1] and unlike neural networks, we have not [yet] discovered a uniformly effective strategy for leveraging additional computation to accelerate wall-clock runtime. [2] [1]…
Roughly half/half, skewed more towards improvements in algorithms. Measuring the Algorithmic Efficiency of Neural Networks: https://arxiv.org/abs/2005.04305 In this work, we argue that algorithmic progress has an aspect that is both straightforward to measure and interesting…
The difference is that SAT/SMT solvers have primarily relied on single-threaded algorithmic improvements [1] and unlike neural networks, we have not [yet] discovered a uniformly effective strategy for leveraging additional computation to accelerate wall-clock runtime. [2] [1]…
bmc7505View on HNParent context