Uma Abordagem Híbrida de SAT e Busca Tabu para o Problema da Programação de Hoários Escolares

Abstract:

O Problema da Programação de Horários Escolares (PPHE) é classificado como NP-Difícil e heurísticas para sua solução são alvo de diversas pesquisas na área de computação, matemática e pesquisa operacional. Normalmente, o problema é resolvido através de abordagens metaheurísticas como Algoritmos Genéticos, Simulated Annealing e GRASP. O presente trabalho propõe uma abordagem alternativa. Pretende-se reduzir do problema ao problema da Satisfazibilidade Proposicional (SAT) e resolvê-lo usando um resolvedor SAT para geração de uma solução inicial. Como não é viável tratar todos os requisitos PPHE através de satisfazibilidade, posteriormente, aplicar-se-á uma Busca Tabu para otimização da solução obtida. A eficiência da abordagem é avaliada comparando-a a abordagens conhecidas na literatura.