No Cover Image

Journal article 1736 views 267 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!
first_indexed 2016-12-16T05:54:19Z
last_indexed 2020-07-16T18:48:05Z
id cronfa31506
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2020-07-16T15:08:35.0912385</datestamp><bib-version>v2</bib-version><id>31506</id><entry>2016-12-15</entry><title>The science of brute force</title><swanseaauthors><author><sid>2b410f26f9324d6b06c2b98f67362d05</sid><ORCID>0000-0003-3021-0095</ORCID><firstname>Oliver</firstname><surname>Kullmann</surname><name>Oliver Kullmann</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2016-12-15</date><deptcode>SCS</deptcode><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.</abstract><type>Journal Article</type><journal>Communications of the ACM</journal><volume>60</volume><journalNumber>8</journalNumber><paginationStart>70</paginationStart><paginationEnd>79</paginationEnd><publisher/><issnPrint>00010782</issnPrint><keywords>Brute force, brute reasoning, SAT, algorithms</keywords><publishedDay>31</publishedDay><publishedMonth>8</publishedMonth><publishedYear>2017</publishedYear><publishedDate>2017-08-31</publishedDate><doi>10.1145/3107239</doi><url/><notes/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><degreesponsorsfunders>University of Austin Texas</degreesponsorsfunders><apcterm/><lastEdited>2020-07-16T15:08:35.0912385</lastEdited><Created>2016-12-15T19:21:43.5440645</Created><authors><author><firstname>Marijn J. H.</firstname><surname>Heule</surname><order>1</order></author><author><firstname>Oliver</firstname><surname>Kullmann</surname><orcid>0000-0003-3021-0095</orcid><order>2</order></author></authors><documents><document><filename>0031506-20122016041441.pdf</filename><originalFilename>CACM.pdf</originalFilename><uploaded>2016-12-20T04:14:41.0770000</uploaded><type>Output</type><contentLength>256920</contentLength><contentType>application/pdf</contentType><version>Accepted Manuscript</version><cronfaStatus>true</cronfaStatus><embargoDate>2018-08-20T00:00:00.0000000</embargoDate><copyrightCorrect>true</copyrightCorrect></document></documents><OutputDurs/></rfc1807>
spelling 2020-07-16T15:08:35.0912385 v2 31506 2016-12-15 The science of brute force 2b410f26f9324d6b06c2b98f67362d05 0000-0003-3021-0095 Oliver Kullmann Oliver Kullmann true false 2016-12-15 SCS 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. Journal Article Communications of the ACM 60 8 70 79 00010782 Brute force, brute reasoning, SAT, algorithms 31 8 2017 2017-08-31 10.1145/3107239 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University University of Austin Texas 2020-07-16T15:08:35.0912385 2016-12-15T19:21:43.5440645 Marijn J. H. Heule 1 Oliver Kullmann 0000-0003-3021-0095 2 0031506-20122016041441.pdf CACM.pdf 2016-12-20T04:14:41.0770000 Output 256920 application/pdf Accepted Manuscript true 2018-08-20T00:00:00.0000000 true
title The science of brute force
spellingShingle The science of brute force
Oliver Kullmann
title_short The science of brute force
title_full The science of brute force
title_fullStr The science of brute force
title_full_unstemmed The science of brute force
title_sort The science of brute force
author_id_str_mv 2b410f26f9324d6b06c2b98f67362d05
author_id_fullname_str_mv 2b410f26f9324d6b06c2b98f67362d05_***_Oliver Kullmann
author Oliver Kullmann
author2 Marijn J. H. Heule
Oliver Kullmann
format Journal article
container_title Communications of the ACM
container_volume 60
container_issue 8
container_start_page 70
publishDate 2017
institution Swansea University
issn 00010782
doi_str_mv 10.1145/3107239
document_store_str 1
active_str 0
description 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.
published_date 2017-08-31T03:38:30Z
_version_ 1763751714767241216
score 11.016235

Similar Items