Dissertação

O Impacto da Modelação na Resolução de Problemas de Satisfação Proposicional 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. Esta dissertação tem por objectivo contribuir para o estudo do impacto da modelação na resolução de problemas de SAT. Para tal, iremos estudar diferentes codificações para quatro problemas distintos: Social Golfer, Round Robin, Completação de Quasigroups e Torres de Hanói. No problema do Social Golfer apresentamos duas codificações que são baseadas em diferentes tipos de variáveis, e efectuamos um estudo experimental onde comparamos as diferentes abordagens. No Round Robin melhoramos uma codificação já existente, quebrando as simetrias globais. Em seguida iremos comparar esta codificação com outra elaborada por nós, que tem como base a codificação apresentada para o problema do Social Golfer. Relativamente ao problema da Completação de Quasigroups, estudamos o impacto da quebra de simetrias locais, visto que este problema não apresenta simetrias globais. Por fim, no problema das Torres de Hanói apresentamos duas codificações conhecidas para o problema e mostramos como as podemos melhorar. Apresentamos também uma nova codificação que permite resolver este problema sem ser necessário a utilização de um algoritmo de procura. Após a análise dos resultados obtidos nos quatro problemas estudados, concluímos que apesar da importância da evolução das ferramentas de SAT, o uso de modelações adequadas a cada problema é igualmente importante para a resolução eficiente dos mesmos.
Satisfação Proposicional, Modelação em SAT, Problema do Social Golfer, Round Robin, Completação de Quasigroups, Torres de Hanói

Outubro 3, 2007, 14:0

Publicação

Obra sujeita a Direitos de Autor

Orientação

CO-ORIENTADOR

Carlos Manuel Costa Lourenço Caleiro

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