| Título: | Modelagem lógica do quebra-cabeça Binairo+ |
| Autor(es): | Moreira, Guilherme Puida |
| Orientador(es): | Ribas, Bruno César |
| Assunto: | Linguagem de modelagem
Modelagem (computação)
Satisfatibilidade booleana |
| Data de apresentação: | 15-Dez-2025 |
| Data de publicação: | 10-Ago-2026 |
| Referência: | MOREIRA, Guilherme Puida. Modelagem lógica do quebra-cabeça Binairo+. 2025. 39 f., il. Trabalho de Conclusão de Curso (Bacharelado em Engenharia de Software) — Universidade de Brasília, Brasília, 2025. |
| Resumo: | Este trabalho investiga a modelagem e a resolução computacional do quebra-cabeça Binairo
e de sua variante Binairo+, que incorpora restrições explícitas de igualdade e desigualdade
entre células. Apresenta três formalizações complementares: uma codificação em Forma
Normal Conjuntiva (CNF) destinada a resolvedores SAT, uma formulação pseudo-Booleana
baseada em inequações lineares e um domínio em PDDL que permite interpretar o problema
como planejamento clássico. Como suporte às análises, foi desenvolvido um gerador de
instâncias guiado por um resolvedor pseudo-Booleano, um validador independente e um
resolvedor próprio com backtracking. A avaliação experimental reúne tabuleiros coletados do
site puzzle-binairo e instâncias adicionais produzidas pelo gerador, cobrindo dimensões
de 6 × 6 a 100 × 100. Os resultados mostram que a formulação pseudo-Booleana oferece o
menor tempo de resolução, a modelagem CNF é prejudicada pelo crescimento do número
de cláusulas na regra de balanceamento, a abordagem em PDDL esbarra no alto fator de
ramificação, mesmo com ajustes no horizonte de busca, e o backtracking serve como linha
de base competitiva apenas para tabuleiros menores. |
| Abstract: | This work addresses the modeling and computational solving of the Binairo puzzle and its
Binairo+ variant, which adds explicit equality and inequality relations between cells. It
introduces three complementary formulations: a Conjunctive Normal Form (CNF) encoding
for SAT solvers, a pseudo-Boolean formulation grounded on linear inequalities, and a
PDDL domain that casts the puzzle as a classical planning task. To support the study, it
also introduces a pseudo-Boolean guided instance generator, an independent validator, and
an in-house backtracking solver. The experimental campaign combines puzzles collected
from puzzle-binairo with additional instances created by the generator, covering board
sizes from 6 × 6 up to 100 × 100. Results highlight the pseudo-Boolean encoding as the
most efficient option, while the CNF formulation suffers from the explosion of clauses
induced by the balancing rule, the PDDL model remains limited by the branching factor
despite horizon-tuning heuristics, and the backtracking baseline stays competitive only on
the smallest boards. |
| Informações adicionais: | Trabalho de Conclusão de Curso (graduação) — Universidade de Brasília, Faculdade de Ciências e Tecnologias em Engenharia, Engenharia de Software, 2025. |
| Licença: | A concessão da licença deste item refere-se ao termo de autorização impresso assinado pelo autor que autoriza a Biblioteca Digital da Produção Intelectual Discente da Universidade de Brasília (BDM) a disponibilizar o trabalho de conclusão de curso por meio do sítio bdm.unb.br, com as seguintes condições: disponível sob Licença Creative Commons 4.0 International, que permite copiar, distribuir e transmitir o trabalho, desde que seja citado o autor e licenciante. Não permite o uso para fins comerciais nem a adaptação desta. |
| Aparece na Coleção: | Engenharia de Software
|
Todos os itens na BDM estão protegidos por copyright. Todos os direitos reservados.
