Uma prova assistida por computador resolve o problema da “coloração da embalagem”

Heule, no entanto, achou revigorante a descoberta de resultados anteriores. Demonstrou que outros pesquisadores acharam o problema importante o suficiente para trabalhar e confirmou para ele que o único resultado que valia a pena obter era resolver o problema completamente.

“Depois que descobrimos que havia 20 anos de trabalho no problema, isso mudou completamente o quadro”, disse ele.

Evitando o Vulgar

Ao longo dos anos, Heule fez carreira encontrando maneiras eficientes de pesquisar entre as vastas combinações possíveis. Sua abordagem é chamada de solução SAT – abreviação de “satisfabilidade”. Envolve a construção de uma fórmula longa, chamada de fórmula booleana, que pode ter dois resultados possíveis: 0 ou 1. Se o resultado for 1, a fórmula é verdadeira e o problema está resolvido.

Para o problema de coloração de embalagem, cada variável na fórmula pode representar se uma determinada célula está ocupada por um determinado número. Um computador procura maneiras de atribuir variáveis ​​para satisfazer a fórmula. Se o computador puder fazer isso, você sabe que é possível empacotar a grade nas condições que você definiu.

Infelizmente, uma codificação direta do problema de coloração de empacotamento como uma fórmula booleana poderia se estender a muitos milhões de termos – um computador, ou mesmo uma frota de computadores, poderia executar para sempre testando todas as diferentes maneiras de atribuir variáveis ​​dentro dele.

“Tentar fazer essa força bruta levaria até que o universo terminasse se você fizesse isso ingenuamente”, disse Goddard. “Então você precisa de algumas simplificações legais para reduzi-lo a algo que seja possível.”

Além disso, toda vez que você adiciona um número ao problema de coloração de embalagem, ele se torna cerca de 100 vezes mais difícil, devido à forma como as combinações possíveis se multiplicam. Isso significa que, se um banco de computadores trabalhando em paralelo pudesse descartar 12 em um único dia de computação, eles precisariam de 100 dias de tempo de computação para descartar 13.

Heule e Subercaseaux consideravam a ampliação de uma abordagem computacional de força bruta vulgar, de certa forma. “Tínhamos várias ideias promissoras, então adotamos a mentalidade de ‘Vamos tentar otimizar nossa abordagem até que possamos resolver esse problema em menos de 48 horas de computação no cluster’”, disse Subercaseaux.

Para fazer isso, eles tiveram que encontrar maneiras de limitar o número de combinações que o cluster de computação tinha que tentar.

“[They] queremos não apenas resolvê-lo, mas resolvê-lo de uma maneira impressionante”, disse Alexander Soifer, da Universidade do Colorado, Colorado Springs.

Heule e Subercaseaux reconheceram que muitas combinações são essencialmente as mesmas. Se você está tentando preencher uma peça em forma de diamante com oito números diferentes, não importa se o primeiro número que você coloca é um para cima e um para a direita do quadrado central, ou um para baixo e outro para a esquerda o quadrado central. Os dois posicionamentos são simétricos entre si e restringem seu próximo movimento exatamente da mesma maneira, então não há razão para verificar os dois.