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

Detalles Bibliográficos
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:
Acceso en línea:Ver este registro en EBSCOhost
fields @attributes:
  recordID: 1
pdfLink:
plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=124418723&site=ehost-live
header:
  @attributes:
    shortDbName: hlh
    uiTerm: 124418723
    longDbName: Humanities International Complete
    uiTag: AN
  controlInfo:
    bkinfo:
    jinfo:
      jid:
        00010782
        ACM
      jtl: Communications of the ACM
      issn: 00010782
      maglogo: N
    pubinfo:
      dt: Aug2017
      vid: 60
      iid: 8
      pid: 68
      pub: Association for Computing Machinery
    artinfo:
      ui:
        124418723
        10.1145/3107239
      ppf: 70
      ppct: 10
      formats:
      tig:
        atl: The Science of Brute Force.
      aug:
        au:
          HEULE, MARIJN J. H.
          KULLMANN, OLIVER
        affil:
          Research scientist at The University of Texas, Austin.
          Associate professor in computer science at Swansea University, U.K.
      su:
        Automation
        Mathematics software
        Mathematical proofs
        Ramsey theory
        Cluster analysis software
        Disruptive innovations
        Logic
        Computer software
      sug:
        subj:
          Automation
          Mathematics software
          Mathematical proofs
          Ramsey theory
          Cluster analysis software
          Disruptive innovations
          Logic
          Computer software
      ab: 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.
      pubtype: Periodical
      doctype: Article
      src: R
    language: English
    refInfo:
    copyright:
      @attributes:
        flag: Y
      dt:
        @attributes:
          year: 2017
    holdings:
      @attributes:
        islocal: N