Show simple item record

dc.contributor.authorOliveira, Ricardo Tavares dept_BR
dc.contributor.otherSilva, Fabianopt_BR
dc.contributor.otherUniversidade Federal do Paraná. Setor de Ciencias Exatas. Programa de Pós-Graduaçao em Informáticapt_BR
dc.date.accessioned2013-05-09T19:47:40Z
dc.date.available2013-05-09T19:47:40Z
dc.date.issued2013-05-09
dc.identifier.urihttp://hdl.handle.net/1884/30035
dc.description.abstractResumo: São apresentadas neste trabalho reduções de problemas de grafos para SAT ou Max- SAT. Reduções dos problemas da Árvore de Steiner, Ciclo Hamiltoniano e Ciclo Hamiltoniano Mínimo são apresentadas, assim como uma redução de Clique para SAT (embora uma redução mais simples de MaxClique para MaxSAT seja conhecida). Todas essas reduções são lineares ou quadráticas no tamanho do grafo dado. Essas reduções usam um operador de cardinalidade que não está entre os operadores tradicionais da lógica proposicional. Entretanto, este operador pode ser convertido para uma fórmula em CNF em tempo linear, de forma que é possível utilizar um resolvedor SAT no estado-da-arte para resolver as instâncias geradas. Também é válido tentar resolver essas instâncias com um resolvedor SAT não clausal que suporte o operador. Desta forma, o operador pode ser utilizado diretamente, sem a necessidade de sua conversão para uma fórmula em CNF. Assim, este trabalho também apresenta uma versão modificada de um resolvedor SAT não clausal que reconhece o operador e resolve as instâncias de SAT e MaxSAT não clausal obtidas pelas reduções apresentadas. Além disso, este resolvedor é auxiliado por dois novos módulos. Um destes módulos é capaz de antecipar os retrocessos do resolvedor através da análise de sua valoração parcial com o grafo original. O outro, mais genérico, é capaz de armazenar as cláusulas aprendidas durante o processo e inferir valores verdade de acordo com a valoração parcial. As reduções apresentadas são comparadas com outras reduções publicadas anteriormente para os mesmos problemas, tanto no tamanho das fórmulas geradas quanto no desempenho de um resolvedor SAT as resolvendo. Além disso, o desempenho do resolvedor SAT não clausal modificado e seus módulos também é testado.pt_BR
dc.format.mimetypeapplication/pdfpt_BR
dc.languagePortuguêspt_BR
dc.subjectTesespt_BR
dc.subjectProgramação logicapt_BR
dc.subjectTeoria dos grafospt_BR
dc.titleReduções de problemas em grafos com soluções conexas para (MAX)SAT e adaptação de um resolvedor SAT e MAXSAT não clausal para as instâncias obtidaspt_BR
dc.typeDissertaçãopt_BR


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record