💻 computer science

The QBF Gallery 2023

O artigo "The QBF Gallery 2023" documenta o estado da arte na resolução de fórmulas booleanas quantificadas (QBFs) ao apresentar uma nova coleção de benchmarks consolidados, realizar uma análise comparativa dos solucionadores submetidos e disponíveis publicamente, e discutir o futuro da avaliação e do apoio à comunidade de pesquisa em QBF.

Autores originais: Simone Heisinger, Luca Pulina, Martina Seidl

Publicado 2026-04-20

📖 4 min de leitura☕ Leitura rápida

CC BY 4.0

Autores originais: Simone Heisinger, Luca Pulina, Martina Seidl

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 que você está organizando uma Olimpíada de Quebra-Cabeças Lógicos, mas em vez de peças de madeira, os participantes estão tentando resolver mistérios matemáticos complexos chamados Fórmulas Booleanas Quantificadas (QBFs).

Este documento é o relatório oficial da edição de 2023 dessa competição, chamada "QBF Gallery 2023". Ele foi escrito por pesquisadores da Universidade Johannes Kepler (na Áustria) e da Universidade de Sassari (na Itália).

Aqui está o resumo da história, explicado de forma simples:

1. O Que é essa Competição?

Pense no QBF como um jogo de xadrez onde, além de você fazer um movimento, você precisa prever todas as respostas possíveis do seu oponente para cada uma das suas jogadas, e assim por diante, em camadas infinitas. É um problema muito difícil para computadores.

O objetivo da "QBF Gallery" não é apenas dar medalhas, mas ajudar a comunidade a entender quais ferramentas (solvers) são melhores e criar novos desafios para que os computadores fiquem mais inteligentes. É como um laboratório de testes gigante.

2. As "Pistas" (Tracks) da Competição

A competição foi dividida em diferentes categorias, como se fossem diferentes tipos de labirintos:

A Pista Clássica (PCNF): Aqui, os quebra-cabeças vêm em um formato padrão, organizado e rígido (como uma lista de regras bem escrita). É a categoria mais popular.
A Pista Livre (PNCNF): Aqui, os quebra-cabeças são mais bagunçados e criativos. Eles não seguem a estrutura rígida da pista anterior, o que é mais difícil para os computadores, mas mais próximo da realidade.
A Pista de Dependência (DQBF): Um nível ainda mais avançado, onde algumas regras dependem de outras de formas estranhas. Foi um desafio para os especialistas.
A Pista de "Artesanato" (Crafted): Aqui, os organizadores criaram problemas do zero, baseados em jogos (como Hex ou Connect4) ou em lógica pura, para testar os limites exatos das máquinas.
A Pista de "Pré-Processamento": Imagine que, antes de resolver o quebra-cabeça, você pode usar uma ferramenta para organizar as peças, tirar as que não servem ou pintar as importantes. Os participantes trouxeram essas ferramentas de organização.

3. Os Participantes (Solvers)

Os "atletas" aqui são programas de computador (solvers). Alguns são veteranos, outros são novatos.

Os Campeões: Os programas CAQE (em suas três versões diferentes) foram os grandes vencedores. Eles conseguiram resolver a maioria dos quebra-cabeças, especialmente na pista clássica. Foi como se eles tivessem um superpoder de organização.
Os Especialistas: Outros programas, como o Pedant e o dynQBF, foram muito bons em tipos específicos de problemas, mesmo que não tenham vencido o geral.
A Surpresa: O relatório mostrou que, às vezes, dar mais memória (RAM) para o computador ajuda muito, mas nem sempre. É como dar um carro mais potente: às vezes ele corre mais, mas às vezes o motor superaquece e não faz diferença.

4. O Grande Desafio: A "Limpeza"

Um dos pontos mais interessantes foi o uso de Pré-processadores.
Imagine que você recebe uma caixa de legos cheia de peças soltas, poeira e peças quebradas. Antes de tentar construir o castelo (resolver o problema), você usa uma máquina para limpar a caixa e separar as peças boas.

O relatório descobriu que nenhum pré-processador é o melhor para todos.
Às vezes, o pré-processador "Bloqqer" ajuda um computador a resolver rápido.
Outras vezes, o "HQSpre" é o melhor.
E em alguns casos, limpar o problema demora tanto que o computador perde tempo e não ganha nada.

5. O Que Aprendemos? (As Conclusões)

Não existe "o melhor de tudo": Assim como um nadador pode ser ótimo em nado livre, mas péssimo em nado borboleta, nenhum programa de computador vence em todos os tipos de problemas QBF.
A Importância da Diversidade: Os organizadores perceberam que precisavam de problemas mais variados. Se todos os problemas forem fáceis, ninguém aprende nada. Se forem todos impossíveis, ninguém ganha. O equilíbrio é a chave.
Formato Importa: O mesmo problema, quando apresentado de formas diferentes (formatos diferentes), pode ser fácil para um computador e impossível para outro. É como tentar ler um livro em uma língua que você não conhece; mudar o idioma (o formato) pode fazer toda a diferença.

6. O Legado

No final, os organizadores liberaram todos os quebra-cabeças novos e os resultados para que qualquer pessoa no mundo possa baixar e testar. Eles criaram um "banco de dados" público para que os cientistas continuem a melhorar essas ferramentas.

Em resumo: A QBF Gallery 2023 foi uma festa de testes onde computadores tentaram resolver os maiores mistérios lógicos da atualidade. Os vencedores foram os programas CAQE, mas a verdadeira vitória foi entender melhor como essas máquinas pensam e como podemos ajudá-las a pensar melhor no futuro.

Título: The QBF Gallery 2023: Avaliação e Análise de Estado da Arte em Fórmulas Booleanas Quantificadas

1. O Problema

O problema central abordado é a decisão de Fórmulas Booleanas Quantificadas (QBFs), reconhecido como o problema canônico PSPACE-completo. Diferente do SAT (Satisfatibilidade Booleana), que lida apenas com variáveis existenciais, as QBFs incluem quantificadores universais ( $\forall$ ) e existenciais ( $\exists$ ), tornando-as fundamentais para redução de problemas complexos e aplicações em verificação formal, síntese e inteligência artificial. O desafio reside na eficiência dos solucionadores (solvers) para lidar com a complexidade computacional exponencial e na necessidade de benchmarks robustos para avaliar o progresso da tecnologia.

2. Metodologia

O relatório documenta a edição de 2023 do QBF Gallery, um evento de avaliação virtual e offline que segue a tradição de coletar novos solucionadores e fórmulas para benchmarking. A metodologia envolveu:

Trilhas (Tracks) de Avaliação: O evento foi dividido em cinco categorias distintas para cobrir diferentes formatos e complexidades:
1. PCNF (Prenex CNF): Fórmulas na forma normal conjuntiva pré-nexa (formato QDIMACS).
2. PNCNF (Prenex Non-CNF): Fórmulas pré-nexas sem a restrição de CNF (formato QCIR).
3. DQBF (Dependency QBF): Uma generalização de QBF usando quantificadores Henkin (formato DQDIMACS).
4. Crafted Instances: Instâncias geradas a partir de problemas de complexidade de prova para testar limites inferiores e superiores.
5. Preprocessor Track: Ferramentas que reescrevem fórmulas para facilitar a resolução sem alterar seu valor de verdade.
Ambiente Computacional: Os experimentos foram executados em um cluster da Universidade Johannes Kepler (Linz), utilizando nós com processadores AMD EPYC. O limite de tempo (timeout) foi de 15 minutos por instância, com 8 GB de memória (exceto em testes adicionais com 100 GB para análise de sensibilidade).
Seleção de Benchmarks: As fórmulas submetidas foram filtradas para garantir um equilíbrio entre dificuldade e solvabilidade. Fórmulas resolvidas por todos os solvers em menos de um segundo foram descartadas. O conjunto final combina instâncias novas com fórmulas bem avaliadas de anos anteriores.
Métricas de Desempenho:
- Número de instâncias resolvidas (SAT/UNSAT).
- PAR-2 Score: Uma métrica que penaliza tempos de execução e falhas (timeout), onde um score menor é melhor.
- Análise de Similaridade: Uso de coeficientes de correlação de Spearman para visualizar a similaridade de desempenho entre diferentes solvers.

3. Principais Contribuições

Novo Conjunto de Benchmarks Consolidado: A criação e disponibilização pública de um conjunto de dados unificado que combina fórmulas de alta qualidade de anos anteriores com novas instâncias submetidas pela comunidade.
Expansão para Formatos Não-CNF: Destaque significativo para a trilha PNCNF, onde quase metade das fórmulas submetidas estava em formato não-CNF (QCIR), refletindo uma tendência de mover-se além das limitações da forma normal conjuntiva.
Análise de Pré-processadores: Avaliação detalhada de como diferentes pré-processadores (Bloqqer, HQSpre, QRATPre+) impactam o desempenho dos solvers, demonstrando que não existe um pré-processador universalmente superior para todos os casos.
Visualização de Resultados: Introdução de mapas de calor (heatmaps) para correlação de solvers e gráficos de aranha (spiderplots) para análise de desempenho por conjunto de fórmulas, permitindo uma compreensão mais granular das forças e fraquezas de cada ferramenta.

4. Resultados Chave

Trilha PCNF (QDIMACS):
- As três variantes do solver CAQE (CAQE-pre, CAQE-Bloqqer, CAQE-HQSpre) dominaram a categoria, resolvendo o maior número de instâncias.
- O solver dynQBF (baseado em expansão) mostrou-se único ao resolver um número significativo de instâncias SAT que outros solvers não conseguiram.
- A análise de sensibilidade à memória (8GB vs 100GB) revelou que solvers como RAReQS e miniQU-q beneficiaram-se significativamente de mais memória, enquanto dynQBF apresentou inconsistências nos resultados entre execuções.
Trilha PNCNF (QCIR):
- O solver QuAbS-CAQE liderou em número total de instâncias resolvidas.
- O solver CQESTO (baseado em circuitos) destacou-se com o maior número de instâncias resolvidas exclusivamente (uniquely solved).
- Diferente da trilha PCNF, onde muitos solvers resolveram mais instâncias UNSAT, na trilha QCIR a maioria dos solvers resolveu mais instâncias SAT.
Trilha DQBF:
- O solver Pedant (baseado em CEGIS - Síntese Indutiva Guiada por Contraexemplo) foi o mais eficaz, resolvendo a maioria das instâncias e as instâncias exclusivas.
Trilha Crafted:
- CAQE-Bloqqer foi o único solver a resolver todas as instâncias de todas as famílias de fórmulas testadas.
Impacto dos Pré-processadores: A maioria dos solvers melhorou seu desempenho com pré-processamento, mas a escolha do pré-processador ideal depende do solver específico (ex: o Qute teve melhor desempenho com Bloqqer, enquanto outros se beneficiaram mais do HQSpre).

5. Significância e Impacto

O relatório "The QBF Gallery 2023" é fundamental para a comunidade de pesquisa em QBF por:

Estabelecer um Padrão de Referência: O novo conjunto de benchmarks consolidado fornece uma base sólida e diversificada para futuras comparações e desenvolvimento de novos algoritmos.
Direcionar o Desenvolvimento Futuro: A análise de similaridade e os resultados das trilhas não-CNF indicam que a comunidade precisa focar em solvers que lidem melhor com estruturas complexas e não-CNF, além de investigar a estabilidade de solvers como o dynQBF.
Transparência e Reprodutibilidade: Ao documentar detalhadamente as configurações, ambientes e resultados, o relatório facilita a reprodutibilidade dos experimentos e a comparação justa entre diferentes abordagens (CEGAR, QCDCL, Expansão, CEGIS).
Integração de Tecnologias: Demonstra a importância da sinergia entre pré-processadores e solvers, mostrando que a otimização da cadeia de ferramentas é tão crucial quanto o algoritmo de resolução em si.

Em suma, o QBF Gallery 2023 não apenas avalia o estado atual da arte, mas também define a direção para os próximos avanços na resolução de fórmulas booleanas quantificadas, incentivando a diversidade de formatos e a robustez dos benchmarks.