FenixEdu™

Dissertação

Redundancy in CNF Formulas EVALUATED

Detalhes: O Problema de Satisfação Proposicional (SAT) é um dos problemas mais estudados em Ciências da Computação e Inteligência Artificial. Recentemente têm surgido muitas inovações no que diz respeito a resolvedores e a novas técnicas de simplificação, e, apesar de SAT ser um problema NP-completo, existem muitas instâncias que podem ser resolvidas em tempo polinomial. Esta dissertação é o resultado da investigação acerca de uma dessas técnicas: a eliminação de redundância. Uma cláusula diz-se redundante se puder ser deduzida através de outras cláusulas, isto é, uma cláusula que não contém informação relevante. A eliminação de cláusulas deste tipo pode reduzir consideravelmente o tamanho das fórmulas. Uma cláusula que não é redundante é chamada cláusula primal. Estas cláusulas constituem um conjunto com características muito especiais, o conjunto das cláusulas primais, que é minimal, em que não existem cláusulas redundantes, e que pode não ser único. São apresentados também alguns resultados experimentais com a finalidade de perceber se a remoção de redundância contribui ou não para reduzir o tempo necessário para resolver uma fórmula CNF.
Keywords: Problema de Satisfação Proposicional, Cláusula Redundante, Conjunto de Cláusulas Primais, Algoritmos de Remoção de Redundância

Discussão: outubro 2, 2007, 9:0