Cover Image
QR Code

The Science of Brute Force.

The article examines "Satisfiability" solving (SAT), an automated reasoning technology that can be applied to mathematics to develop new proofs. It discusses how the disruptive technology was used with the proof of the Boolean Pythagorean Triples problem, and open problem in Ramsey Theory. Particula...

Full description

Published in:Communications of the ACM Vol. 60; no. 8; pp. 70 - 80
Main Authors: HEULE, MARIJN J. H., KULLMANN, OLIVER
Format: Article
Published: Association for Computing Machinery Aug2017
Subjects:
Automation
Mathematics software
Mathematical proofs
Ramsey theory
Cluster analysis software
Disruptive innovations
Logic
Computer software
Online Access:View this record in EBSCOhost
Summary:The article examines "Satisfiability" solving (SAT), an automated reasoning technology that can be applied to mathematics to develop new proofs. It discusses how the disruptive technology was used with the proof of the Boolean Pythagorean Triples problem, and open problem in Ramsey Theory. Particular attention is given to the combination of SAT with high-performance computing clusters.