🔢 mathematics

Queen Domination by SAT Solving

Este artigo apresenta um framework SAT de alto desempenho e produtor de provas que resolve o caso anteriormente em aberto da dominação de rainhas para $n=19$ e corrige a enumeração para $n=16$ ao alavancar uma codificação geometricamente informada, quebra de simetria e um pipeline de verificação unificado para garantir corretude independentemente verificável.

Autores originais: Taha Rostami, Curtis Bright

Publicado 2026-07-30

📖 4 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Taha Rostami, Curtis Bright

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine um mundo onde a matemática não é apenas sobre números em uma página, mas sobre resolver quebra-cabeças tão complexos que até os cérebros humanos mais inteligentes ficam tontos. Este é o reino da busca combinatória, um ramo da ciência da computação e da matemática dedicado a encontrar a melhor maneira de organizar as coisas. Pense nisso como tentar encontrar o mapa de assentos perfeito para um casamento massivo onde cada convidado tem regras específicas sobre com quem pode sentar ao lado, ou descobrir o número absoluto mínimo de seguranças necessários para vigiar cada canto de um museu sem deixar um ponto cego.

Um dos quebra-cabeças mais famosos neste campo é o Problema da Dominação da Rainha. Imagine um tabuleiro de xadrez. Uma rainha é uma peça poderosa que pode atacar tudo em sua linha, sua coluna e em ambos os seus caminhos diagonais. A questão é simples, mas traiçoeira: qual é o menor número de rainhas que você precisa colocar em um tabuleiro $n \times n$ para que cada quadrado esteja sob ataque? Parece fácil para um tabuleiro pequeno, mas à medida que o tabuleiro aumenta, o número de arranjos possíveis explode para bilhões, trilhões e além. Por mais de um século, matemáticos têm tentado resolver isso, não apenas para encontrar o número, mas para contar exatamente de quantas maneiras diferentes você pode organizar essas rainhas. Por que isso importa? Porque resolver esses quebra-cabezas ajuda-nos a entender como organizar sistemas complexos, desde o agendamento de voos até o design de chips de computador. Mas há um porém: quando os computadores fazem a matemática, eles podem cometer erros, e às vezes deixam de encontrar a resposta inteiramente.

É aqui que Taha Rostami e Curtis Bright entram com seu artigo, "Queen Domination by SAT Solving". Eles enfrentaram o problema de contar todas as maneiras únicas de colocar o número mínimo de rainhas em tabuleiros de xadrez de até tamanho 19. Em vez de escrever um programa personalizado para caçar soluções como pesquisadores anteriores fizeram, eles traduziram todo o quebra-cabeça do tabuleiro de xadrez para uma linguagem que um SAT solver (uma máquina de lógica superinteligente) entende. Pense em um SAT solver como um detetive que verifica se um conjunto de regras pode ser verdadeiro. Se o detetive disser "não", ele pode provar isso com um certificado que qualquer outra pessoa possa verificar para garantir que o detetive não mentiu.

Os autores construíram uma "tradução" especial do tabuleiro de xadrez que destacava a geometria do jogo, usando um truque inteligente chamado curva de Hilbert para organizar as pistas para que o detetive pudesse encontrar a resposta mais rápido. Eles também usaram uma estratégia chamada Cube-and-Conquer, que é como dividir um bolo gigante e impossível de comer em milhares de fatias pequenas e gerenciáveis que diferentes computadores podem comer ao mesmo tempo. O resultado? Eles não apenas resolveram o quebra-cabeça; eles provaram que sua solução era 100% correta.

O trabalho deles descobriu um erro surpreendente na história deste problema. Para um tabuleiro de 16x16, especialistas anteriores pensavam que havia apenas 43 maneiras únicas de posicionar as rainhas. Rostami e Bright provaram que existem, na verdade, 371 maneiras — uma diferença massiva que sugere que o programa de computador antigo tinha um erro oculto que estava perdendo a maioria das soluções. Além disso, eles resolveram um caso que estava aberto há muito tempo: o tabuleiro de 19x19. Eles descobriram que existem exatamente 11 maneiras únicas de dominar esse tabuleiro com o número mínimo de rainhas. Ao gerar "certificados de prova" para cada um dos resultados, eles deram à comunidade matemática um nível de confiança que era anteriormente impossível, mostrando que, quando você combina codificação inteligente com verificação de prova rigorosa, pode resolver problemas que até o melhor software especializado pode deixar passar.

Resumo Técnico: Dominação de Rainhas por Resolução de SAT

Definição do Problema
O problema da dominação de rainhas busca o número mínimo de rainhas, denotado por $\gamma(Q_n)$ , necessárias para atacar cada casa em um tabuleiro de xadrez $n \times n$ . Além de determinar este valor mínimo, um desafio significativo reside na enumeração de todas as soluções distintas até o isomorfismo (levando em conta as simetrias do tabuleiro, como rotação e reflexão). Embora os valores ótimos para $\gamma(Q_n)$ tenham sido estabelecidos para $n \le 25$ usando ferramentas de busca especializadas como o UNIDOM, a enumeração de soluções não isomórficas para tabuleiros maiores permanece computacionalmente intensiva. Uma preocupação crítica neste domínio é a confiabilidade dos resultados computacionais; discrepâncias anteriores em outras provas combinatórias (ex: o problema de Lam) e a descoberta de bugs em solvers especializados destacam a necessidade de certificados de correção verificáveis de forma independente.

Metodologia
Os autores propõem uma estrutura de Satisfatibilidade Booleana (SAT) produtora de provas para abordar o problema da dominação de rainhas. Em vez de implementar um algoritmo de busca customizado, o problema é codificado em uma fórmula proposicional em Forma Normal Conjuntiva (CNF). A metodologia baseia-se em várias inovações técnicas fundamentais:

Codificação de Variáveis de Linha: A inovação central é a introdução de variáveis booleanas auxiliares que representam se linhas geométricas específicas (linhas, colunas, diagonais e anti-diagonais) contêm pelo menos uma rainha.
- Variáveis de Rainha ( $Q_i$ ): Indicam se uma rainha é colocada na casa $i$ .
- Variáveis de Linha ( $L_\ell$ ): Indicam se uma linha $\ell$ está "ativa" (contém uma rainha).
- Restrições: Cláusulas garantem que, se uma linha estiver ativa, existe uma rainha nela. A dominação é expressa exigindo que, para cada casa, pelo menos uma de suas quatro linhas que a interceptam esteja ativa. Restrições de cardinalidade limitam o número total de rainhas ( $\sum Q_i \le \gamma$ ) e o número total de linhas ativas ( $\sum L_\ell \le 4\gamma$ ).
Codificação de Cardinalidade e Ordenação de Literais:
- As restrições de cardinalidade são codificadas usando métodos baseados em totalizer. A restrição de rainha usa um totalizer padrão compatível com o framework Cube-and-Conquer, enquanto a restrição de linha usa um modulo totalizer para desempenho.
- Ordenação pela Curva de Hilbert: Uma estratégia de ordenação de literais inovadora é aplicada à restrição de cardinalidade de rainha. Ao percorrer o tabuleiro via uma curva de Hilbert, quadrados espacialmente adjacentes são agrupados juntos na árvore de contagem. Isso preserva a localidade espacial, levando a uma propagação de unidade mais forte. Experimentos mostraram que esta ordenação resolveu a instância de $n=14$ aproximadamente 31,5 vezes mais rápido que a ordenação padrão.
Quebra de Simetria: Para eliminar a exploração redundante de soluções simétricas, o framework impõe restrições de ordenação lexicográfica (baseadas no método de Warwick Harvey) entre a configuração original de rainhas e suas sete transformações geométricas de não-identidade. Isso reduziu significamente os tempos de resolução em testes preliminares (ex: aceleração de 6,64× para $n=15$ ).
Cube-and-Conquer: Para instâncias maiores, o espaço de busca é particionado em subproblemas independentes (cubos) através do ramificar (branching) em variáveis auxiliares da codificação do totalizer. Isso permite a resolução paralela e melhora a escalabilidade sem depender de posicionamentos individuais de rainhas para o particionamento.
Geração de Provas e Verificação: O framework utiliza o cadical-exhaust para enumerar todos os modelos, adicionando iterativamente cláusulas de bloqueio. Ele gera provas DRAT com "cláusulas confiáveis" para certificar a completude. Essas provas são verificadas independentemente usando o drat-trim-t, garantindo que os resultados não dependam da correção interna da lógica de busca do solver, mas apenas da codificação e do verificador de provas.

Principais Resultados
O estudo enumerou com sucesso as soluções não isomórficas de dominação mínima de rainhas para todo $n \le 19$ . Os resultados incluem:

Correção da Literatura: Para $n=16$ , o artigo identifica uma discrepância em relatórios anteriores. Enquanto o solver especializado UNIDOM reportou 43 soluções não isomórficas, o framework SAT prova que existem exatamente 371. Os autores atribuem isso a um bug no UNIDOM que faz com que soluções válidas sejam perdidas sob configurações específicas.
Resolução de Caso Aberto: O caso anteriormente aberto de $n=19$ foi resolvido, estabelecendo que existem exatamente 11 soluções mínimas não isomórficas.
Desempenho: O framework SAT superou consistentemente o solver especializado UNIDOM em instâncias não triviais. Para $n=19$ , a abordagem SAT levou aproximadamente 171.575 segundos (tempo de CPU) para a enumeração, comparado aos 714.733 segundos do UNIDOM. A inclusão das variáveis de linha foi crucial; uma versão preliminar sem elas levou 22,8 vezes mais tempo para resolver e verificar a instância de $n=19$ .

Significância e Alegações
O artigo alega que sua principal contribuição é fornecer uma solução de alto desempenho e independentemente verificável para o problema de enumeração da dominação de rainhas. Ao mudar de um código de busca especializado para um framework SAT produtor de provas, os autores reduzem a "confiança" necessária no processo computacional. A correção dos resultados agora depende exclusivamente da codificação SAT e do verificador de provas externo, em vez da complexa lógica customizada de um solver especializado.

O trabalho demonstra que o design cuidadoso da codificação — especificamente a introdução de variáveis auxiliares para expor a estrutura geométrica, o uso de restrições globais e a ordenação de literais consciente da geometria — pode tornar o solving SAT produtor de provas competitivo com, e superior a, solvers altamente otimizados de domínio específico. Os autores disponibilizam seu código-fonte e dados de solução publicamente para facilitar a verificação e pesquisa posteriores.

Mais como este