Um algoritmo baseado em programação dinâmica e renomeamento para minimização de formas normais

Abstract

Satisfatibilidade booleana é um problema de grande interesse prático, além de ser o primeiro problema caracterizado como NP-completo. Desde que ganhou atenção, diversos algoritmos para este problema já foram descobertos e alguns deles são baseados em formas normais. As transformações usuais para formas normais podem acarretar aumento exponencial do tamanho da fórmula, o que não é desejável. No entanto, é sabido que técnicas como renomeamento podem auxiliar a reduzir o tamanho da fórmula transformada. Neste trabalho, apresentamos uma heurística para o problema de encontrar renomeamentos que reduzem o tamanho de fórmulas e um algoritmo baseado em programação dinâmica para calcular o renomeamento dado pela heurística, junto com sua prova de correção, análise de complexidade e resultados experimentais. A avaliação experimental inclui a comparação do algoritmo proposto com um algoritmo guloso que é ótimo para uma classe restrita do problema. Os resultados indicam que a heurística proposta, na prática, é tão eficiente quanto a do algoritmo ótimo para esta classe, apresentando em alguns casos resultados ainda melhores quando não há restrições sobre a entrada do problema.