Modelagem lógica do quebra-cabeça Binairo+

Abstract

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.