Dissertação

Redundancy in CNF Formulas EVALUATED

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.
Problema de Satisfação Proposicional, Cláusula Redundante, Conjunto de Cláusulas Primais, Algoritmos de Remoção de Redundância

Outubro 2, 2007, 9:0

Publicação

Obra sujeita a Direitos de Autor

Orientação

CO-ORIENTADOR

Francisco Miguel Alves Campos de Sousa Dionísio

Departamento de Matemática (DM)

Professor Auxiliar

ORIENTADOR

Maria Inês Camarate de Campos Lynce de Faria

Departamento de Engenharia Informática (DEI)

Professor Auxiliar