HackerPapers

arXiv:2008.02215cs.AI

A Time Leap Challenge for SAT Solving

Johannes K. Fichte, Markus Hecher, Stefan Szeider

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.

arXiv comments
Authors' version of a paper which is to appear in the proceedings of CP'2020
Journal reference
DOI
Subjects
cs.AIArtificial Intelligence cs.ARHardware Architecture cs.DSData Structures and Algorithms

On Hacker News

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.

Comments linking this paper, per year.

Discussed in comments3 threads

    • 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

  1. The Silent (R)evolution of SAT 1 comment
    • You may want to read "A Time Leap Challenge for SAT Solving". It's just a really fun paper: https://arxiv.org/abs/2008.02215

      sanxiynView on HNParent context

    • 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…

      IsinlorView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.