Imagen de Portada
Código QR

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...

Descripción completa

Publicado en:Communications of the ACM Vol. 60; no. 8; pp. 70 - 80
Autores principales: HEULE, MARIJN J. H., KULLMANN, OLIVER
Formato: Artículo
Publicado: Association for Computing Machinery Aug2017
Materias:
Automation
Mathematics software
Mathematical proofs
Ramsey theory
Cluster analysis software
Disruptive innovations
Logic
Computer software
Acceso en línea:Ver este registro en EBSCOhost
Sumario: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.