Os cientistas da computação e matemáticos da Carnegie Mellon University resolveram a última e teimosa peça da conjectura de Keller, um problema de geometria que os cientistas têm intrigado por 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 e apenas 30 minutos de computação usando um cluster de computadores.
“Fiquei muito feliz quando o resolvemos, mas fiquei um pouco triste porque o problema havia sumido”, disse John Mackey, professor do Departamento de Ciência da Computação (CSD) e do Departamento de Ciências Matemáticas que seguiu a conjectura de Keller desde então ele era um estudante graduado há 30 anos. “Mas então 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, professora associada de ciência da computação que ingressou na 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”, disse Heule 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, apresentada pelo matemático alemão Eduard Ott-Heinrich Keller, tem a ver com os ladrilhos – especificamente, como cobrir uma área com ladrilhos do mesmo tamanho, 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, no entanto, os 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, então 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 pudessem explorar. Nessa forma, chamada de gráfico de Keller, os pesquisadores podiam pesquisar “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 fazer isso, ele provou que a conjectura falha naquela 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 vindo 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 pensei comigo mesmo, talvez possamos usar sua técnica”, lembrou Mackey. 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á fazendo 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. – para que o solucionador possa 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 geralmente melhora ou prejudica sua capacidade de resolver o problema”, disse Heule.
Com 15 anos de experiência, Heule é especialista 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 utilizem 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 estonteante – um número com 324 dígitos – sem uma solução em nenhum lugar à 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 mostrasse impraticável, eles poderiam rejeitar automaticamente outras combinações que dependiam dela. 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 a cerca de um bilhão de configurações. Eles se juntaram a esse esforço por David Narvaez, um Ph.D. estudante do Rochester Institute of Technology, que foi pesquisador visitante no outono de 2019.
Assim que executaram seu 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 este problema e fomos capazes de transformá-lo em uma busca gerada por computador”, disse Heule.
A prova do resultado é totalmente calculada pelo computador, disse Heule, 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, observou ele. 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 forma que nenhum aspecto da prova precise 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 ganhou 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 encontrar códigos não lineares de dimensão superior do que era possível anteriormente.
Heule propôs recentemente 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”, reconheceu Heule. Mas é uma meta aspiracional, acrescentou ele, 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.
Achou útil essa informação? Compartilhe com seus amigos! 
Deixe-nos a sua opinião aqui nos comentário.
