Ao traduzir a conjectura de Keller em uma busca amigável por um tipo de gráfico, os pesquisadores finalmente resolveram um problema sobre a cobertura de espaços com blocos.
Uma equipe de matemáticos finalmente acabou com a conjectura de Keller, mas não resolvendo por conta própria. Em vez disso, eles ensinaram uma frota de computadores a fazer isso por eles.
A conjectura de Keller, apresentada há 90 anos por Ott-Heinrich Keller, é um problema sobre a cobertura de espaços com azulejos idênticos. Ele afirma que, se você cobrir um espaço bidimensional com ladrilhos quadrados bidimensionais, pelo menos dois dos ladrilhos devem compartilhar uma borda. Ele faz a mesma previsão para espaços de todas as dimensões – que ao cobrir, digamos, um espaço 12-dimensional usando ladrilhos “quadrados” 12-dimensionais, você acabará com pelo menos dois ladrilhos que se encostam exatamente um ao outro.
Com o passar dos anos, os matemáticos eliminaram a conjectura, provando que era verdadeira para algumas dimensões e falsa para outras. No outono passado, a questão permaneceu sem solução apenas para o espaço de sete dimensões.
Mas uma nova prova gerada por computador finalmente resolveu o problema. A prova, postada online em outubro passado, é o exemplo mais recente de como a engenhosidade humana, combinada com o poder bruto da computação, pode responder a alguns dos problemas mais complicados da matemática.
Os autores do novo trabalho – Joshua Brakensiek da Stanford University, Marijn Heule e John Mackey da Carnegie Mellon University e David Narváez do Rochester Institute of Technology – resolveram o problema usando 40 computadores. Depois de apenas 30 minutos, as máquinas produziram uma resposta de uma palavra: Sim, a conjectura é verdadeira em sete dimensões. E não temos que tirar suas conclusões com base na fé.
A resposta vem embalada com uma longa prova explicando por que está certa. O argumento é muito amplo para ser entendido por seres humanos, mas pode ser verificado por um programa de computador separado como correto.
Em outras palavras, mesmo que não saibamos o que os computadores fizeram para resolver a conjectura de Keller, podemos ter certeza de que eles fizeram corretamente.
A misteriosa sétima dimensão
É fácil ver que a conjectura de Keller é verdadeira no espaço bidimensional. Pegue um pedaço de papel e tente cobri-lo com quadrados de tamanhos iguais, sem espaços entre os quadrados e sem sobreposição. Você não vai longe antes de perceber que pelo menos dois dos quadrados precisam compartilhar uma borda. Se você tem blocos espalhados, é igualmente fácil ver que a conjectura é verdadeira no espaço tridimensional. Em 1930, Keller conjecturou que essa relação vale para espaços e ladrilhos correspondentes de qualquer dimensão.
Os primeiros resultados apoiaram a previsão de Keller. Em 1940, Oskar Perron provou que a conjectura é verdadeira para espaços nas dimensões de um a seis. Porém, mais de 50 anos depois, uma nova geração de matemáticos encontrou o primeiro contra-exemplo para a conjectura: Jeffrey Lagarias e Peter Shor provaram que a conjectura é falsa na dimensão 10 em 1992.
Um argumento simples mostra que, uma vez que a conjectura é falsa em uma dimensão, ela é necessariamente falsa em todas as dimensões superiores. Assim, depois de Lagarias e Shor, as únicas dimensões não estabelecidas foram sete, oito e nove. Em 2002, Mackey provou que a conjectura de Keller era falsa na dimensão oito (e, portanto, também na dimensão nove).
Isso deixou apenas a dimensão sete aberta – ou era a dimensão mais alta onde a conjectura se sustentava ou a dimensão mais baixa onde falhava.
“Ninguém sabe exatamente o que está acontecendo lá”, disse Heule.
Ligue os pontos
À medida que os matemáticos eliminaram o problema ao longo das décadas, seus métodos mudaram. Perron calculou as primeiras seis dimensões com lápis e papel, mas na década de 1990, os pesquisadores aprenderam como traduzir a conjectura de Keller de uma forma completamente diferente – uma que lhes permitiu aplicar computadores ao problema.
A formulação original da conjectura de Keller é sobre um espaço liso e contínuo. Dentro desse espaço, existem infinitas maneiras de colocar um número infinito de peças. Mas os computadores não são bons em resolver problemas que envolvem opções infinitas – para fazer sua mágica, eles precisam de algum tipo de objeto finito e discreto para pensar.
Em 1990, Keresztély Corrádi e Sándor Szabó surgiram com esse objeto discreto. Eles provaram que você pode fazer perguntas sobre este objeto que são equivalentes à conjectura de Keller – de modo que se você provar algo sobre esses objetos, você necessariamente prova a conjectura de Keller também. Isso efetivamente reduziu uma questão sobre o infinito a um problema mais fácil sobre a aritmética de alguns números.
É assim que funciona.
Digamos que você queira resolver a conjectura de Keller na dimensão dois. Corrádi e Szabó descobriram um método para fazer isso, construindo o que chamaram de gráfico de Keller.
Para começar, imagine 16 dados em uma mesa, cada um posicionado de forma que o rosto com dois pontos fique voltado para cima. (O fato de serem dois pontos reflete o fato de que você está abordando a conjectura para a dimensão dois; veremos por que são 16 dados em um momento.) Agora, pinte cada ponto usando qualquer uma das quatro cores: vermelho, verde, branco ou Preto.
As posições dos pontos em um único dado não são intercambiáveis: pense em uma posição como representando uma coordenada x e a outra como representando uma coordenada y. Assim que os dados estiverem coloridos, começaremos a desenhar linhas, ou bordas, entre os pares de dados, se houver duas condições: Os dados têm pontos em uma posição que são de cores diferentes, e na outra posição eles têm pontos cujas cores não são apenas diferentes, mas emparelhados, com vermelho e verde formando um par e preto e branco o outro.
Então, por exemplo, se um dado tem dois pontos vermelhos e o outro tem dois pontos pretos, eles não estão conectados: embora atendam aos critérios para uma posição (cores diferentes), eles não atendem aos critérios para a outra ( cores emparelhadas). No entanto, se um dado for vermelho-preto e o outro verde-verde, eles estão conectados, pois têm cores emparelhadas em uma posição (vermelho-verde) e cores diferentes na outra (preto-verde).
Existem 16 maneiras possíveis de usar quatro cores para colorir dois pontos (é por isso que estamos trabalhando com 16 dados). Organize todas as 16 possibilidades à sua frente. Conecte todos os pares de dados que se enquadram na regra. Agora, a questão crucial: você pode encontrar quatro dados que estão todos conectados entre si?
Esses subconjuntos de dados totalmente conectados são chamados de clique. Se você puder encontrar um, você provou que a conjectura de Keller é falsa na dimensão dois. Mas você não pode, porque não existirá. O fato de que não há clique de quatro dados significa que a conjectura de Keller é verdadeira na dimensão dois.
Os dados não são literalmente as peças em questão na conjectura de Keller, mas você pode pensar em cada dado como representando uma peça. Pense nas cores atribuídas aos pontos como coordenadas que situam os dados no espaço. E pense na existência de uma borda como uma descrição de como dois dados são posicionados em relação um ao outro.
Se dois dados tiverem exatamente as mesmas cores, eles representam peças que estão exatamente na mesma posição no espaço. Se não tiverem cores em comum e não houver pares de cores (um dado é preto-branco e o outro é verde-vermelho), eles representam ladrilhos que se sobreporiam parcialmente – o que, lembre-se, não é permitido no ladrilho. Se os dois dados tiverem um conjunto de cores emparelhadas e um conjunto da mesma cor (um é vermelho-preto e o outro é verde-preto), eles representam peças que compartilham uma face.
Finalmente, e mais importante, se eles têm um conjunto de cores emparelhadas e outro conjunto de cores que são meramente diferentes – isto é, se eles estão conectados por uma borda – isso significa que os dados representam as peças que estão se tocando, mas deslocadas um do outro ligeiramente, de modo que seus rostos não se alinhem exatamente. Esta é a condição que você realmente deseja investigar. Os dados que são conectados por uma borda representam ladrilhos que estão conectados sem compartilhar uma face – exatamente o tipo de arranjo de ladrilhos necessário para refutar a conjectura de Keller.
“Eles precisam se tocar, mas não podem se tocar totalmente”, disse Heule.
Ampliando
Trinta anos atrás, Corrádi e Szabó provaram que os matemáticos podem usar esse procedimento para abordar a conjectura de Keller em qualquer dimensão, ajustando os parâmetros do experimento. Para provar a conjectura de Keller em três dimensões, você pode usar 216 dados com três pontos em uma face e talvez três pares de cores (embora haja flexibilidade neste ponto). Em seguida, você deve procurar oito dados (2³) entre eles que estão totalmente conectados entre si usando as mesmas duas condições que usamos antes.
Como regra geral, para provar a conjectura de Keller na dimensão n, você usa dados com n pontos e tenta encontrar um clique de tamanho 2n. Você pode pensar neste clique como uma espécie de “superladrilho” (composto de 2n ladrilhos menores) que poderia cobrir todo o espaço n-dimensional.
Então, se você puder encontrar este superladrilho (que por si só não contém ladrilhos de compartilhamento de face), você pode usar cópias traduzidas ou deslocadas dele para cobrir todo o espaço com ladrilhos que não compartilham um rosto, refutando assim a conjectura de Keller.
“Se você tiver sucesso, poderá cobrir todo o espaço com a tradução. O bloco sem face comum vai se estender por toda a telha”, disse Lagarias, que agora está na Universidade de Michigan.
Mackey refutou a conjectura de Keller na dimensão oito ao encontrar um clique de 256 dados (28), portanto, responder à conjectura de Keller para a dimensão sete exigiu procurar um clique de 128 dados (27). Encontre aquele clique e você provou que a conjectura de Keller é falsa na dimensão sete. Prove que tal clique não pode existir, por outro lado, e você provou que a conjectura é verdadeira.
Infelizmente, encontrar um clique de 128 dados é um problema particularmente espinhoso. Em trabalhos anteriores, os pesquisadores poderiam usar o fato de que as dimensões oito e 10 podem ser “fatoradas”, em certo sentido, em espaços de dimensões inferiores que são mais fáceis de trabalhar. Não tive essa sorte aqui.
“A dimensão sete é ruim porque é principal, o que significa que você não pode dividi-la em coisas de dimensões inferiores”, disse Lagarias. “Portanto, não havia escolha a não ser lidar com toda a combinatória desses gráficos.”
Buscar um clique de tamanho 128 pode ser uma tarefa difícil para o cérebro humano desassistido, mas é exatamente o tipo de pergunta que um computador é bom em responder – especialmente se você ajudar um pouco.
A linguagem da lógica
Para transformar a busca por cliques em um problema com o qual os computadores podem lidar, você precisa de uma representação do problema que use a lógica proposicional. É um tipo de raciocínio lógico que incorpora um conjunto de restrições.
Digamos que você e dois amigos estejam planejando uma festa. Vocês três estão tentando montar a lista de convidados, mas vocês têm interesses conflitantes. Talvez você queira convidar Avery ou excluir Kemba. Um de seus co-planejadores deseja convidar Kemba ou Brad ou os dois. Seu outro co-planejador, com um machado para moer, quer deixar de fora Avery ou Brad, ou os dois. Dadas essas restrições, você poderia perguntar: Existe uma lista de convidados que satisfaça todos os três planejadores de festas?
Em termos de ciência da computação, esse tipo de questão é conhecido como problema de satisfatibilidade. Você o resolve descrevendo-o no que é chamado de fórmula proposicional que, neste caso, se parece com isto, onde as letras A, K e B representam os hóspedes potenciais: (A OU NÃO K) E (K OU B) E (NÃO A OU NÃO B).
O computador avalia essa fórmula inserindo 0 ou 1 para cada variável. Um 0 significa que a variável é falsa ou está desligada e 1 significa que é verdadeira ou está ligada. Então, se você colocar um 0 para “A”, significa que Avery não foi convidada, enquanto um 1 significa que ela é. Existem muitas maneiras de atribuir 1s e 0s a esta fórmula simples – ou construir a lista de convidados – e é possível que, depois de examiná-los, o computador conclua que não é possível satisfazer todas as demandas concorrentes. Neste caso, porém, existem duas maneiras de atribuir 1s e 0s que funcionam para todos: A = 1, K = 1, B = 0 (significando convidar Avery e Kemba) e A = 0, K = 0, B = 1 (significa convidar apenas o Brad).
Um programa de computador que resolve declarações de lógica proposicional como este é chamado de solucionador SAT, onde “SAT” significa “satisfazibilidade”. Ele explora todas as combinações de variáveis e produz uma resposta de uma palavra: Ou SIM, há uma maneira de satisfazer a fórmula, ou NÃO, não há.
“Você apenas decide se cada variável é verdadeira ou falsa de forma a tornar toda a fórmula verdadeira, e se você pode fazer isso, a fórmula é satisfatória, e se você não pode, a fórmula é insatisfatória”, disse Thomas Hales, da Universidade de Pittsburgh.
A questão de saber se é possível encontrar um clique de tamanho 128 é um tipo de problema semelhante. Ele também pode ser escrito como uma fórmula proposicional e conectado a um solucionador SAT. Comece com um grande número de dados com sete pontos cada e seis cores possíveis. Você pode colorir os pontos de forma que 128 dados possam ser conectados uns aos outros de acordo com as regras especificadas? Em outras palavras, existe uma maneira de atribuir cores que possibilite o clique?
A fórmula proposicional que captura essa questão sobre cliques é bastante longa, contendo 39.000 variáveis diferentes. Cada um pode receber um de dois valores (0 ou 1). Como resultado, o número de permutações possíveis de variáveis, ou maneiras de organizar as cores nos dados, é 239.000 – um número muito, muito grande.
Para responder à conjectura de Keller para a dimensão sete, um computador teria que verificar cada uma dessas combinações – ou eliminando todas (significando que nenhum clique de tamanho 128 existe, e Keller é verdadeiro na dimensão sete) ou encontrando apenas um que funcione (significando Keller é falso).
“Se você tivesse um computador ingênuo para verificar todas as configurações possíveis, seria esse número de caixas de 324 dígitos”, disse Mackey. Levaria os computadores mais rápidos do mundo até o fim dos tempos antes que eles esgotassem todas as possibilidades.
Mas os autores do novo trabalho descobriram como os computadores poderiam chegar a uma conclusão definitiva sem realmente ter que verificar todas as possibilidades. A eficiência é a chave.
Eficiências ocultas
Mackey se lembra do dia em que, aos seus olhos, o projeto realmente deu certo. Ele estava em frente a um quadro negro em seu escritório na Carnegie Mellon University discutindo o problema com dois de seus co-autores, Heule e Brakensiek, quando Heule sugeriu uma forma de estruturar a pesquisa para que pudesse ser concluída em uma quantidade razoável de Tempo.
“Havia um verdadeiro gênio intelectual trabalhando lá em meu escritório naquele dia”, disse Mackey. “Foi como assistir Wayne Gretzky, como assistir LeBron James nas finais da NBA. Estou arrepiado agora [só de pensar nisso].”
Existem muitas maneiras de aumentar a busca por um gráfico de Keller específico. Imagine que você tem muitos dados em uma mesa e está tentando organizar 128 deles de uma forma que satisfaça as regras de um gráfico de Keller. Talvez você organize 12 deles corretamente, mas não consegue encontrar uma maneira de adicionar o próximo dado. Nesse ponto, você pode descartar todas as configurações de 128 dados que envolvem aquela configuração inicial impraticável de 12 peças.
“Se você sabe que as cinco primeiras coisas que você atribuiu não se encaixam, não precisa olhar para nenhuma das outras variáveis, e isso geralmente diminui muito a busca”, disse Shor, que agora é no Instituto de Tecnologia de Massachusetts.
Outra forma de eficiência envolve simetria. Quando os objetos são simétricos, pensamos neles como sendo, em certo sentido, iguais. Essa semelhança permite que você compreenda um objeto inteiro apenas estudando uma parte dele: vislumbre metade de um rosto humano e você pode reconstruir todo o rosto.
Atalhos semelhantes funcionam para gráficos de Keller. Imagine, novamente, que você está organizando os dados em uma mesa. Talvez você comece no centro da mesa e construa uma configuração à esquerda. Você lança quatro dados e, em seguida, atinge um obstáculo. Agora você descartou uma configuração inicial – e todas as configurações baseadas nela. Mas você também pode descartar a imagem espelhada dessa configuração inicial – o arranjo dos dados que você obtém quando posiciona os dados da mesma maneira, mas construindo para a direita.
“Se você puder encontrar uma maneira de resolver os problemas de satisfatibilidade que leve em consideração as simetrias de uma forma inteligente, então você tornou o problema muito mais fácil”, disse Hales.
Os quatro colaboradores tiraram proveito desses tipos de eficiência de pesquisa de uma nova maneira – em particular, eles automatizaram considerações sobre simetrias, onde trabalhos anteriores haviam contado com matemáticos trabalhando praticamente à mão para lidar com elas.
No final das contas, eles simplificaram a busca por um clique de tamanho 128 para que, em vez de verificar 239.000 configurações, seu solucionador SAT só tivesse que pesquisar cerca de 1 bilhão (230). Isso transformou uma busca que poderia ter levado eras em uma tarefa matinal. Finalmente, depois de apenas meia hora de cálculos, eles tiveram uma resposta.
“Os computadores disseram não, então sabemos que a conjectura se mantém?, disse Heule. Não há como colorir 128 dados de modo que todos estejam conectados uns aos outros, então a conjectura de Keller é verdadeira na dimensão sete: qualquer arranjo de ladrilhos que cubra o espaço inevitavelmente inclui pelo menos dois ladrilhos que compartilham um rosto.
Na verdade, os computadores entregaram muito mais do que uma resposta de uma palavra. Eles o apoiaram com uma longa prova – 200 gigabytes de tamanho – justificando sua conclusão.
A prova é muito mais do que uma leitura de todas as configurações de variáveis verificadas pelos computadores. É um argumento lógico que estabelece que o clique desejado não poderia existir. Os quatro pesquisadores alimentaram a prova de Keller em um verificador de prova formal – um programa de computador que rastreou a lógica do argumento – e confirmaram seu funcionamento.
“Você não apenas examina todos os casos e não encontra nada, você examina todos os casos e é capaz de escrever uma prova de que essa coisa não existe”, disse Mackey. “Você pode escrever uma prova de insatisfação.”
Publicado em 20/08/2020 18h06
Artigo original:
Achou importante? Compartilhe!
Assine nossa newsletter e fique informado sobre Astrofísica, Biofísica, Geofísica e outras áreas. Preencha seu e-mail no espaço abaixo e clique em “OK”: