Dissertação

Local Search for Unsatisfiable Propositional Formulae EVALUATED

Nos últimos anos assistimos a um progresso notável na área de satisfação proposicional (SAT), com contribuições tanto a nível teórico como prático. Apesar das ferramentas de SAT requererem tempo de execução exponencial no pior caso, estas conseguem actualmente resolver instâncias de problemas difíceis. A habilidade para provar a não satisfação de fórmulas proposicionais tem estado interdita a procedimentos de procura local estocástica (SLS) até recentemente. Esta dissertação tem como objectivo contribuir para o estudo das duas ferramentas que provam a não satisfação em vez da satisfação: RANGER e GUNSAT. Dá-se uma descrição detalhada de cada ferramenta e apresentam-se vários exemplos. Com o objectivo de melhorar o RANGER, adicionam-se-lhe dois métodos usados pelo GUNSAT: propagação unitária por antevisão e resolução estendida. Apresentam-se e explicam-se as vantagens e desvantagens de cada método quando aplicado ao RANGER e chega-se a resultados deveras interessantes. A descrição é complementada correndo a ferramenta com várias baterias de testes de instâncias não satisfazíveis. Após a análise dos resultados obtidos e dos princípios teóricos aplicados, conclui-se que a propagação unitária por antevisão é uma técnica muito promissora e recomenda-se vivamente a sua adição a futuras versões do RANGER, enquanto a resolução estendida sofre de uma dependência muito forte das poderosas heurísticas do GUNSAT. Estas não são compatíveis com a simplicidade do RANGER.
Satisfação Proposicional, Provar a Não Satisfação, Procura Local, RANGER, GUNSAT, Propagação Unitária por Antevisão, Resolução Estendida

Outubro 28, 2008, 9:0

Publicação

Obra sujeita a Direitos de Autor

Orientação

ORIENTADOR

Maria Inês Camarate de Campos Lynce de Faria

Departamento de Engenharia Informática (DEI)

Professor Auxiliar