Dissertação
Max-SAT Algorithms For Real World Instances EVALUATED
O problema de satisfiabilidade Booleana (SAT) é a base de estudo da classe de problemas NP-Completos e NP-Difíceis. Muitos problemas do mundo real como automatização de desenho electrónico, desenho de hardware entre outros, pertencem a esta classe de problemas. O estudo do problema SAT e outros problemas semelhantes contribui para a compreensão e resolução destes problemas reais. O problema da máxima satisfiabilidade Booleana (Max-SAT) é uma versão do problema SAT de optimização e não decisão. Max-SAT é portanto mais indicado para resolver problemas de optimização, como distribuição de FPGA, depuração de desenho, bioinformática, entre outros. Ainda assim muitos dos resolvedores de Max-SAT encontram-se atrasados em relação à eficiência dos resolvedores de SAT. O crescente número de problema do mundo real que podem ser traduzidos para Max-SAT é o motor deste trabalho. Analisamos o problema de Max-SAT e avaliamos o estado da arte dos resolvedores actuais, incluindo as duas principais abordagens para a resolução deste problema: ramifica-e-limita (do Inglês "branch-and-bound"), uma técnica muito usada para resolver problemas de optimização, e tradução para outros problemas, em concreto para SAT. Propomos neste trabalho combinar estas duas abordagens, ramifica-e-limita, melhor para resolver instâncias aleatórias e homogéneas, com a abordagem baseada em tradução, mais eficiente para instâncias reais e heterogéneas.
novembro 5, 2010, 10: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