A poderosa tecnologia de resolução SAT pode funcionar com a infame hipótese de Collatz. No entanto, as chances de isso acontecer não são muito altas.
Nos últimos anos, Mariin Hijul usou uma tecnologia de pesquisa de provas computadorizada chamada SAT solver (SAT para satisfatibilidade) para conquistar uma lista impressionante de problemas matemáticos. Os triplos pitagóricos em 2016, Schur em 5 em 2017 e, recentemente, a hipótese de Keller na sétima dimensão, sobre a qual escrevemos há pouco tempo no artigo " A pesquisa por computador ajudou a lidar com um problema matemático de 90 anos ."
Agora, no entanto, Hijul, um cientista da computação da Carnegie Mellon University, tem como objetivo um objetivo ainda mais ambicioso: a conjectura de Collatz, considerada por muitos como o problema aberto mais difícil em matemática (e provavelmente o mais simples de formular). Outros matemáticos, aprendendo comigo que Khiyul estava fazendo essa tentativa, ficaram céticos a respeito.
“Não vejo como esse problema pode ser resolvido completamente com o solucionador SAT”, disse Thomas Hales, da Universidade de Pittsburgh, um dos principais especialistas em evidências computacionais. Essa tecnologia ajuda essencialmente os matemáticos a resolver problemas - alguns dos quais têm um número infinito de opções - transformando-os em problemas discretos e finitos.
No entanto, Hales, como os outros, tinha medo de subestimar Khiyul. “Ele é muito bom em encontrar maneiras inteligentes de formular problemas na linguagem SAT. Ele é muito bom nisso. "
Scott Aaronsonda Universidade do Texas em Austin, trabalhando com Hiyul na conjectura de Collatz, acrescentou: “Marin é um homem com um martelo, isto é, com um solucionador de SAT, e é provavelmente o portador mais digno desse martelo em todo o mundo. E ele tenta aplicá-lo a quase tudo. " Mas só o tempo dirá se ele pode transformar a hipótese de Collatz em um prego.
A solução SAT requer reformular os problemas em uma linguagem compreensível por computador que usa lógica proposicional e, em seguida, conectar computadores para decidir se há uma maneira de tornar essas declarações verdadeiras. Aqui está um exemplo simples.
Digamos que você seja um pai que está tentando organizar uma creche. Uma de suas babás pode trabalhar a semana toda, exceto terça e quinta-feira. O outro é além de terça e sexta-feira. O terceiro - exceto quinta e sexta-feira. Você precisa se sentar com seu filho na terça, quinta e sexta-feira. Isso pode ser alcançado?
Uma maneira de testar isso é transformar as restrições da babá em uma fórmula e alimentá-la para o solucionador SAT. O programa buscará uma maneira de distribuir os dias entre as babás para que a fórmula seja verdadeira, ou "satisfeita" - ou seja, para que você obtenha os três dias de que precisa. Se for bem-sucedido, esse método existirá.
Infelizmente, não está imediatamente claro como reformular muitas das questões matemáticas mais importantes para a linguagem SAT. Mas às vezes podem ser reformuladas como perguntas de satisfação de maneiras inesperadas.
“É difícil prever quando a tarefa será reduzida a uma computação enorme, mas finita”, disse Aaronson.
A conjectura de Collatz é uma daquelas questões matemáticas que, à primeira vista, nem parece um problema de babá. Ela sugere o seguinte: pegue qualquer número (inteiro, diferente de zero). Se for ímpar, multiplique por 3 e some 1. Se for par, divida por 2. Como resultado, você obtém um novo número. Aplique as mesmas regras e continue. A hipótese prevê que, independentemente do número inicial, você termina com 1 e fica preso em um loop: 1, 4, 2, 1.
E, apesar de essa hipótese ter sido trabalhada por quase 100 anos, os matemáticos não chegaram perto de prová-la.
Mas isso não impediu Khiyul. Em 2018, ele e Aronson - embora fossem colegas de universidade - receberam uma bolsa da National Science Foundation para aplicar o solucionador SAT à conjectura de Collatz.
Pegue qualquer número. Se for ímpar, multiplique por 3 e some 1. Se for par, divida por 2. Como resultado, você obtém um novo número. Aplique as mesmas regras e continue. Você consegue encontrar um número que não leve a 1? Você pode tentar você mesmo .
Para começar, Aaronson, um cientista da computação, propôs uma formulação alternativa da hipótese de Collatz, a assim chamada. Um "sistema de regras de substituição" que tornava mais fácil o trabalho dos computadores.
Em um sistema de regra de substituição, você trabalha com um conjunto de caracteres, como as letras A, B e C. Você os usa para formar sequências: ACACBACB. Você também tem regras para converter essas sequências. Uma regra pode dizer que quando você encontra um AC, você o substitui por BC. Outros podem substituir a aeronave por AAA. Você pode definir qualquer número de regras que definem quaisquer transformações.
Os cientistas da computação geralmente precisam saber se uma determinada JV sempre termina. Isto é, independentemente de qual linha começar e em que ordem aplicar as regras, é verdade que a linha acabará por se transformar em um estado em que nenhuma regra pode ser aplicada?
Aaronson criou um SP com sete símbolos e 11 regras, semelhante à hipótese de Collatz. Se eles puderem provar que sua JV sempre termina, eles irão provar que a hipótese está correta.
Para transformar a conjectura de Collatz em um problema de solucionador de SAT, Aaronson e Hiyul tiveram que dar outro passo envolvendo matrizes, ou arranjos de números. Eles precisavam atribuir uma matriz única para cada símbolo em seu SP. Essa abordagem - uma maneira comum de procurar provas de que o SP está terminando o trabalho - permitiria que eles raciocinassem sobre as transformações de números por meio da multiplicação de matrizes. Sete matrizes denotando sete símbolos com SP tiveram que satisfazer todo um conjunto de restrições, refletindo a correspondência de 11 regras entre si.
“Primeiro, você tenta encontrar matrizes que satisfaçam essas restrições”, disseEmre Yolchu , uma estudante de doutorado na Carnegie Mellon University, trabalhando neste problema com Hijul. “Se você tiver sucesso, você prova que a execução para” e, portanto, que a hipótese de Collatz está correta.
O solver SAT pode responder à questão da existência de matrizes que satisfaçam essas restrições. Aaronson e Hijul primeiro executaram o solucionador SAT em matrizes 2x2 pequenas. Eles não encontraram opções de trabalho. Em seguida, eles tentaram matrizes 3x3. E novamente sem sucesso. Eles continuaram a aumentar o tamanho das matrizes na esperança de que pudessem ser encontradas.
No entanto, essa abordagem não pode evoluir indefinidamente, uma vez que a complexidade da busca por matrizes adequadas aumenta exponencialmente com seu tamanho. Hijul sugere que os computadores modernos simplesmente não conseguem lidar com matrizes maiores do que 12x12.
“Quando as matrizes ficam muito complexas, você não consegue resolver o problema”, disse ele.
Hijul ainda está trabalhando na otimização da pesquisa, tentando torná-la mais eficiente para que o solucionador SAT possa verificar matrizes cada vez maiores. Ela e seus colegas estão trabalhando em um artigo resumindo suas descobertas atuais, mas eles estão quase sem ideias e provavelmente terão que desistir em breve - pelo menos por um tempo.
Afinal, o apelo do solucionador SAT é que, se você pudesse descobrir como verificar outro caso, ligar para outra babá, estender a busca por mais algum tempo, provavelmente poderia encontrar o que estava procurando. Nesse sentido, a principal vantagem de Khiyul pode não ser sua experiência com solucionadores de SAT, mas seu amor pela busca de resultados.
“Sou apenas um otimista”, disse ele. "Muitas vezes sinto que tenho sorte, então tento ver até onde consigo chegar."