Mathematics solves problems by pen and paper. CS helps us to go far beyond that. Long-standing open problems in mathematics can now be solved completely automatically resulting in clever though potentially gigantic proofs. Our time requires answers to hard questions regarding safety and security. In these cases knowledge is more important than understanding as long as we can trust the answers. Powerful SAT-solving heuristics facilitate linear speedups even when using thousands of cores. Combined with the ever-increasing capabilities of highperformance computing clusters they enable solving challenging problems.
%0 Journal Article
%1 HeuleKullmann17cacm
%A Heule, Marijn J. H.
%A Kullmann, Oliver
%D 2017
%J Communications of the ACM
%K 01821 acm paper science theory algorithm test tool
%N 8
%P 70--79
%R 10.1145/3107239
%T The Science of Brute Force
%V 60
%X Mathematics solves problems by pen and paper. CS helps us to go far beyond that. Long-standing open problems in mathematics can now be solved completely automatically resulting in clever though potentially gigantic proofs. Our time requires answers to hard questions regarding safety and security. In these cases knowledge is more important than understanding as long as we can trust the answers. Powerful SAT-solving heuristics facilitate linear speedups even when using thousands of cores. Combined with the ever-increasing capabilities of highperformance computing clusters they enable solving challenging problems.
@article{HeuleKullmann17cacm,
abstract = {Mathematics solves problems by pen and paper. CS helps us to go far beyond that. Long-standing open problems in mathematics can now be solved completely automatically resulting in clever though potentially gigantic proofs. Our time requires answers to hard questions regarding safety and security. In these cases knowledge is more important than understanding as long as we can trust the answers. Powerful SAT-solving heuristics facilitate linear speedups even when using thousands of cores. Combined with the ever-increasing capabilities of highperformance computing clusters they enable solving challenging problems.},
added-at = {2017-10-30T12:22:24.000+0100},
author = {Heule, Marijn J. H. and Kullmann, Oliver},
biburl = {https://www.bibsonomy.org/bibtex/2d0217d5c38ef31af28536d3aa4e86531/flint63},
doi = {10.1145/3107239},
file = {ACM Digital Library:2017/HeuleKullmann17cacm.pdf:PDF},
groups = {public},
interhash = {0a3824944de0f09c1e56c73f0c3a35c2},
intrahash = {d0217d5c38ef31af28536d3aa4e86531},
issn = {0001-0782},
journal = {Communications of the ACM},
keywords = {01821 acm paper science theory algorithm test tool},
month = {#aug#},
number = 8,
pages = {70--79},
timestamp = {2018-04-16T11:59:00.000+0200},
title = {The Science of Brute Force},
username = {flint63},
volume = 60,
year = 2017
}