Papers of the day   All papers

A Time Leap Challenge for SAT-Solving

Comments

Stefan Szeider: Two teams compete. Team A uses modern SAT solvers on a 20-year-old computer. Team B uses 20-year-old SAT solvers on a modern computer. Who solves more problem instances? New @cp2020conf paper ➡️https://arxiv.org/pdf/2008.02215.pdf ➡️https://doi.org/10.1007/978-3-030-58475-7_16 Funded by @FWF_at @WWTF https://t.co/Id2QRsCe55

10 replies, 519 likes


Colin McMillen, Ph.D.: https://arxiv.org/pdf/2008.02215.pdf "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." 1/

3 replies, 73 likes


Lance Fortnow: Out of Vienna the following challenge: Modern SAT solvers on 20 year old hardware vs. Current hardware using 20 year old algorithms. Spoiler: The new algorithms wins but not by much. https://arxiv.org/abs/2008.02215 ht @vardi

1 replies, 55 likes


Alex J. Champandard: "Our findings show that the progress on the algorithmic side [in 20 years] has at least as much impact as the progress on the hardware side."

1 replies, 28 likes


Drew Volpe: Researchers ran modern algorithms on 20 yr old CPUs (467 MHz Pentium III) and 20 yr old algorithms on modern CPUs (2.6 GHz Xeon). Modern algorithms on old hardware (Team SW) won, just barely. Not what I would've guessed. https://arxiv.org/pdf/2008.02215.pdf https://t.co/PcSHoFz8ag

0 replies, 13 likes


HotComputerScience: Most popular computer science paper of the day: "A Time Leap Challenge for SAT-Solving" https://hotcomputerscience.com/paper/a-time-leap-challenge-for-sat-solving https://twitter.com/StefanSzeider/status/1302868135633211392

0 replies, 8 likes


David Manheim: A clever experiment that provides some evidence about the debate about how much hardware vs. software contributes to speeding up an already mature computational domain. cc: @AIImpacts, @ESYudkowsky But note that there has been no outpouring of money for SAT solver ASICs.

0 replies, 3 likes


Stephan Beyer: I wtf'ed: "we compare 20-year-old SAT-solvers on new computer hardware with modern SAT-solvers on 20-year-old hardware" #SAT #algorithms https://arxiv.org/abs/2008.02215

0 replies, 2 likes


Laurent Simon: Very interesting results where we (also) observe that recent solvers focused on recent benchmarks solving only. I enjoyed the idea of the paper. Simple, well conducted and fun.

1 replies, 2 likes


ᴊᴀᴍᴇꜱ ᴊᴜꜱᴛ ᴊᴀᴍᴇꜱ: Fascinating paper that basically shows that modern SAT solver algorithms are as important as modern hardware. Will make me think twice before I use $whatever_sat_algorithm_is_in_that_random_lib, particularly when I care about performance and large problem sizes.

0 replies, 1 likes


Content

Found on Sep 07 2020 at https://arxiv.org/pdf/2008.02215.pdf

PDF content of a computer science paper: A Time Leap Challenge for SAT-Solving