No Cover Image

Journal article 1894 views 285 downloads

The science of brute force

Marijn J. H. Heule, Oliver Kullmann Orcid Logo

Communications of the ACM, Volume: 60, Issue: 8, Pages: 70 - 79

Swansea University Author: Oliver Kullmann Orcid Logo

Check full text

DOI (Published version): 10.1145/3107239

Abstract

We discuss recent advances in the science of brute-force. Very hard problems can now be solved by adding "brute reasoning" to the brute-force method, in the form of SAT solving (satisfiability solving). A key example is the recent solution of the boolean Pythagorean triples problem, which...

Full description

Published in: Communications of the ACM
ISSN: 00010782
Published: 2017
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa31506
Tags: Add Tag
No Tags, Be the first to tag this record!
Abstract: We discuss recent advances in the science of brute-force. Very hard problems can now be solved by adding "brute reasoning" to the brute-force method, in the form of SAT solving (satisfiability solving). A key example is the recent solution of the boolean Pythagorean triples problem, which comes from the mathematical domain. The proof produced here, the largest proof ever constructed (200 TB), had a strong media echo, and scepticism about its "meaning" (or absence thereof) has been raised. We show, that these methods and extracted proofs have indeed meaning, and are indeed useful, when taking the real-world applications into account, the domain of safety and verification.
Keywords: Brute force, brute reasoning, SAT, algorithms
Issue: 8
Start Page: 70
End Page: 79