Cientistas da computação e matemáticos da Carnegie Mellon University resolveram o último, peça teimosa da conjectura de Keller, um problema de geometria que os cientistas têm intrigado há 90 anos.

Ao estruturar o quebra-cabeça como o que os cientistas da computação chamam de problema de satisfatibilidade, os pesquisadores resolveram o problema com quatro meses de programação frenética de computador e apenas 30 minutos de computação usando um cluster de computadores.

"Fiquei muito feliz quando o resolvemos, mas depois fiquei um pouco triste porque o problema tinha desaparecido, "disse John Mackey, um professor do Departamento de Ciência da Computação (CSD) e do Departamento de Ciências Matemáticas que perseguia a conjectura de Keller desde que ele era um estudante de graduação há 30 anos. "Mas então eu me senti feliz novamente. Há apenas uma sensação de satisfação."

A solução foi mais um sucesso para uma abordagem iniciada por Marijn Heule, um professor associado de ciência da computação que ingressou no CSD em agosto passado. Heule usou um solucionador SAT - um programa de computador que usa lógica proposicional para resolver problemas de satisificabilidade (SAT) - para vencer vários desafios matemáticos antigos, incluindo o problema dos triplos pitagóricos e o número 5 de Schur.

"O problema intrigou muitas pessoas por décadas, quase um século, "Heule disse sobre a conjectura de Keller." Esta é realmente uma vitrine do que pode ser feito agora e que não era possível anteriormente. "

A conjectura, apresentado pelo matemático alemão Eduard Ott-Heinrich Keller, tem a ver com lado a lado, especificamente, como cobrir uma área com ladrilhos de tamanho igual sem nenhuma lacuna ou sobreposição. A conjectura é que pelo menos dois dos ladrilhos terão que compartilhar uma borda e que isso é verdade para espaços de todas as dimensões.

É fácil provar que é verdade para ladrilhos bidimensionais e cubos tridimensionais. Em 1940, a conjectura foi provada verdadeira para todas as dimensões até seis. Em 1990, Contudo, matemáticos provaram que não funciona na dimensão 10 ou superior.

Foi quando a conjectura de Keller capturou a imaginação de Mackey, em seguida, um estudante da Universidade do Havaí. Com um escritório próximo ao cluster de computação da universidade, ele ficou intrigado porque o problema poderia ser traduzido, usando a teoria dos grafos discretos, em uma forma que os computadores possam explorar. Neste formulário, chamado de gráfico Keller, pesquisadores poderiam pesquisar por "cliques" - subconjuntos de elementos que se conectam sem compartilhar um rosto, desmentindo assim a conjectura.

Em 2002, Mackey fez exatamente isso, descobrindo um clique na dimensão oito. Ao fazê-lo, ele provou que a conjectura falha nessa dimensão e, por extensão, na dimensão nove.

Isso deixou a conjectura sem solução para a dimensão sete.

Quando Heule chegou à CMU da Universidade do Texas no ano passado, ele já tinha a reputação de usar o solucionador SAT para resolver problemas de matemática abertos de longa data.

"Eu refleti para mim mesmo, talvez possamos usar sua técnica, "Mackey lembrou. Em pouco tempo, ele começou a discutir como usar o solucionador SAT na conjectura de Keller com Heule e Joshua Brakensiek, uma dupla especialização em ciências matemáticas e ciência da computação, que agora está cursando o doutorado. em ciência da computação na Universidade de Stanford.

Um solucionador SAT requer a estruturação do problema usando uma fórmula proposicional - (A ou não B) e (B ou C), etc. - então o solucionador pode examinar todas as variáveis ​​possíveis para combinações que irão satisfazer todas as condições.

"Existem muitas maneiras de fazer essas traduções, e a qualidade da tradução normalmente melhora ou prejudica sua capacidade de resolver o problema, "Heule disse.

Com 15 anos de experiência, Heule é perito em realizar essas traduções. Um de seus objetivos de pesquisa é desenvolver raciocínio automatizado para que essa tradução possa ser feita automaticamente, permitindo que mais pessoas usem essas ferramentas em seus problemas.

Mesmo com uma tradução de alta qualidade, o número de combinações a serem verificadas na dimensão sete era alucinante - um número com 324 dígitos - sem uma solução à vista, mesmo com um supercomputador. Mas Heule e os outros aplicaram vários truques para reduzir o tamanho do problema. Por exemplo, se uma configuração de dados se mostrar inviável, eles poderiam rejeitar automaticamente outras combinações que dependiam dele. E como muitos dos dados eram simétricos, o programa poderia descartar imagens espelhadas de uma configuração se ela chegasse a um beco sem saída em um arranjo.

Usando essas técnicas, eles reduziram sua pesquisa para cerca de um bilhão de configurações. Eles se juntaram a este esforço por David Narvaez, um Ph.D. estudante do Rochester Institute of Technology, que foi um pesquisador visitante no outono de 2019.

Depois de executar o código em um cluster de 40 computadores, eles finalmente tiveram uma resposta:a conjectura é verdadeira na dimensão sete.

"O motivo do nosso sucesso é que John tem décadas de experiência e visão sobre esse problema e fomos capazes de transformá-lo em uma pesquisa gerada por computador, "Heule disse.

A prova do resultado é totalmente calculada pelo computador, Heule disse, em contraste com muitas publicações que combinam partes verificadas por computador de uma prova com redações manuais de outras partes. Isso torna difícil para os leitores entenderem, ele notou. A prova de computador para a solução Keller inclui todos os aspectos da solução, incluindo uma parte de quebra de simetria contribuída por Narvaez, Heule enfatizou, de modo que nenhum aspecto da prova precisa depender de esforço manual.

“Podemos ter verdadeira confiança na correção deste resultado, "disse ele. Um artigo descrevendo a resolução de Heule, Mackey, Brakensiek e Narvaez ganharam o prêmio de Melhor Artigo na Conferência Conjunta Internacional sobre Raciocínio Automatizado em junho.

Resolver a conjectura de Keller tem aplicações práticas, Disse Mackey. Esses cliques que os cientistas procuram para refutar a conjectura são úteis na geração de códigos não lineares que podem tornar a transmissão de dados mais rápida. O solucionador SAT, portanto, pode ser usado para localizar códigos não lineares de dimensão superior do que era possível anteriormente.

Heule recentemente propôs usar o solucionador SAT para resolver um problema matemático ainda mais famoso:a conjectura de Collatz. Neste problema, a ideia é pegar qualquer número inteiro positivo e dividir por 2 se for um número par ou multiplicar por 3 e adicionar 1 se for um número ímpar. Em seguida, aplique as mesmas regras ao número resultante e a cada resultado sucessivo. A conjectura é que o resultado eventual será sempre 1.

Resolver Collatz com o solucionador SAT "é um tiro no escuro, "Heule reconheceu. Mas é uma meta aspiracional, ele adicionou, explicando que o solucionador SAT pode ser usado para resolver uma série de problemas matemáticos menos intimidantes, mesmo que Collatz se mostre inatingível.