Revisiting Incremental Linearization for Nonlinear Integer Arithmetic

Imagine que você é um detetive tentando resolver um mistério, mas as pistas que lhe são dadas estão escritas em uma linguagem que muda seu significado dependendo de como você as observa. Este é o mundo da Satisfatibilidade Modular de Teorias (SMT), um ramo da ciência da computação onde o software tenta descobrir se um conjunto de regras lógicas pode ser verdadeiro ao mesmo tempo. Pense nisso como um solucionador de quebra-cabeças superinteligente que verifica se um programa irá travar, se um código secreto pode ser decifrado ou se o caminho de um robô é seguro.

Na maioria das vezes, esses quebra-cabeças são fáceis porque envolvem apenas linhas retas e adições simples (como $x + y = 5$). Os computadores são incríveis nisso. Mas a vida fica complicada quando você introduz a aritmética não linear — regras onde as coisas são multiplicadas entre si ou elevadas a potências (como $x \times y$ ou $x^3$). De repente, as regras tornam-se curvas e sinuosas, e a matemática torna-se incrivelmente difícil de resolver. Na verdade, para números inteiros, é matematicamente impossível criar um método perfeito e 100% completo que resolva todos esses quebra-cabeças. Por causa disso, cientistas da computação constroem detetives "bons o suficiente" que usam atalhos inteligentes para encontrar respostas rapidamente, mesmo que não possam prometer resolver todos os casos impossíveis.

O artigo que você está prestes a ler apresenta um novo detetive, chamado qfn2l, que é melhor em resolver esses quebra-cabeças complicados e curvos do que os que tínhamos antes. Os autores, pesquisadores da Universidade Técnica Checa em Praga, perceberam que os antigos atalhos estavam tendo dificuldades com um tipo específico de quebra-cabeça difícil: aqueles que envolvem potências (como $x^3$) e produtos mistos (como $x^2y$). Eles decidiram atualizar o kit de ferramentas do detetive com um novo conjunto de regras que agem como uma rede mais apertada, capturando os palpites ruins que costumavam escapar.

O Jeito Antigo: Adivinhando com Funções Não Interpretadas

Para entender a atualização, vamos ver como os detetives anteriores trabalhavam. Imagine que você tem uma caixa misteriosa rotulada como $f(x, y)$. Você não sabe o que há dentro, mas sabe que, se colocar os mesmos números, obterá o mesmo número. O método antigo tratava cada multiplicação, como $x \times y$, como essa caixa misteriosa. O computador adivinhava um valor para a caixa, verificava se fazia sentido e, se não fizesse, adicionava uma regra para corrigir o palpite.

Isso funcionava bem para casos simples, mas era como tentar adivinhar o peso de uma melancia sabendo apenas que ela é "pesada". Era muito vago. Quando o quebra-cabeça envolvia potências altas, como $x^3$, as regras antigas eram muito frouxas. O detetive adivinhava um valor, o computador dizia: "Não, isso não se encaixa", e então adicionava uma regra muito fraca para corrigir o erro. O detetive teria que adivinhar, falhar e adivinhar novamente centenas de vezes, muitas vezes ficando sem tempo antes de encontrar a resposta.

O Novo Truque: Apertando a Rede com Secantes

Os autores deste artigo decidiram parar de tratar essas potências como caixas misteriosas e passar a tratá-las como constantes frescas — apenas números simples e comuns que representam o resultado da potência. Mas a verdadeira magia está nas novas regras que eles adicionaram para verificar esses números.

Eles descobriram que, para qualquer número inteiro, digamos $v$, a função $x^k$ (como $x^3$) comporta-se de uma forma muito previsível entre $v$ e $v+1$. Eles criaram um novo conjunto de regras baseado em retas secantes. Imagine uma curva em um gráfico. Uma reta secante é uma linha reta que conecta dois pontos nessa curva. Os autores perceberam que, se você desenhar uma linha reta entre o ponto $(v, v^k)$ e o próximo ponto inteiro, essa linha cria uma "cerca" muito apertada ao redor da curva.

Aqui está a analogia:

• O Jeito Antigo: O detetive desenhava um círculo enorme e frouxo ao redor das respostas possíveis. Era fácil de desenhar, mas deixava entrar muitos palpites errados.
• O Novo Jeito: O detetive desenha uma série de cercas retas e apertadas que abraçam a curva da resposta muito de perto. Se um palpite cair fora dessas cercas apertadas, o detetive sabe imediatamente que está errado e adiciona uma regra para empurrar o palpite de volta para dentro.

Como essas cercas são tão apertadas, o detetive não precisa adivinhar tantas vezes. Ele converge para a resposta certa muito mais rápido, especialmente para quebra-cabeças envolvendo cubos e produtos mistos.

O Desafio da "Soma de Três Cubos"

Para provar que seu novo detetive estava funcionando, os autores testaram-no em uma classe famosa de quebra-cabeças chamada "soma de três cubos". Estes são problemas que perguntam: "Você consegue encontrar três números inteiros que, quando elevados ao cubo e somados, resultam em um número específico?"

Por exemplo, o quebra-cлуbica pode ser: $x^3 + y^3 + z^3 = 79$.

Isso é um pesadelo para os solucionadores padrão. Os números podem ser enormes e as relações são complexas. Os autores testaram seu novo solucionador, qfn2l, contra os melhores solucionadores existentes (como Z3, cvc5 e MathSAT).

• Os outros solucionadores tentaram resolver o quebra-cabeça $x^3 + y^3 + z^3 = 79$, mas desistiram após 3 minutos (eles "esgotaram o tempo").
• O novo solucionador, qfn2l, encontrou a resposta — $x = -19, y = 35, z = -33$ — em apenas 20 segundos.

Os Resultados: Um Novo Desafiante Competitivo

Os pesquisadores rodaram seu solucionador em uma coleção massiva de 25.444 quebra-cabeças de uma biblioteca padrão chamada SMT-LIB. Aqui está o que eles descobriram:

1. Desempenho Geral: O novo solucionador é competitivo com as melhores ferramentas disponíveis. Ele resolveu cerca de 14.000 quebra-cabeças no total, o que é próximo dos melhores desempenhos, embora não tenha superado os melhores (como o Z3) em todos os tipos de quebra-cabeças.
2. O Ponto Ideal: O novo solucionador brilha absolutamente nos quebra-cabeças dominados por potências e produtos mistos. Na família "MathProblems" (que inclui a soma de cubos), ele resolveu cerca de 53% das instâncias (585 a 587 de 1.100). Os outros solucionadores tiveram muito mais dificuldade com esses tipos específicos de problemas.
3. A Troca (Trade-off): Os autores testaram uma versão de seu solucionador que tentava ser extra cuidadosa ao verificar se diferentes partes do quebra-cabeça eram consistentes (chamado de "axiomas de congruência"). Eles descobriram que essa verificação extra na verdade retardava o solucionador em quebra-cabeças gerais, resolvendo cerca de 1.600 instâncias a menos no total. Isso sugere que, para a maioria dos problemas, as cercas apertadas (limites de secantes) são suficientes, e você não precisa do trabalho pesado adicional de verificar cada regra de consistência.

Por Que Isso Importa

O artigo não afirma ter resolvido o insolúvel. Eles admitem que, como o problema é matematicamente indecidível, nenhum computador pode resolver todos os casos. No entanto, eles mostraram que, ao mudar a forma como aproximamos essas regras não lineares e curvas — especificamente usando essas cercas apertadas baseadas em secantes — podemos tornar os detetives "bons o suficiente" muito mais inteligentes.

Eles construíram uma ferramenta que é de código aberto e roda sobre um motor existente (Z3), provando que uma estratégia mais inteligente pode vencer uma abordagem de força bruta nos tipos mais difíceis de quebra-cabeças inteiros. Para qualquer pessoa tentando verificar se um software não irá travar ou se um protocolo criptográfico é seguro, este novo método oferece uma maneira mais rápida e confiável de verificar a matemática por trás dos bastidores.

Em resumo, os autores pegaram um problema desordenado e curvo e desenharam linhas mais apertadas ao redor dele, permitindo que os computadores encontrem a verdade muito mais rápido do que antes.