Atenção: Todas as denúncias são sigilosas e sua identidade será preservada.
Os campos nome e e-mail são de preenchimento opcional
Metadados | Descrição | Idioma |
---|---|---|
Autor(es): dc.contributor | Silva, Fabiano | - |
Autor(es): dc.contributor | Universidade Federal do Paraná. Setor de Ciencias Exatas. Programa de Pós-Graduaçao em Informática | - |
Autor(es): dc.creator | Oliveira, Ricardo Tavares de | - |
Data de aceite: dc.date.accessioned | 2019-08-22T00:28:17Z | - |
Data de disponibilização: dc.date.available | 2019-08-22T00:28:17Z | - |
Data de envio: dc.date.issued | 2013-05-09 | - |
Data de envio: dc.date.issued | 2013-05-09 | - |
Data de envio: dc.date.issued | 2013-05-09 | - |
Fonte completa do material: dc.identifier | http://hdl.handle.net/1884/30035 | - |
Fonte: dc.identifier.uri | http://educapes.capes.gov.br/handle/1884/30035 | - |
Descrição: dc.description | Resumo: 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. | - |
Formato: dc.format | application/pdf | - |
Formato: dc.format | application/pdf | - |
Palavras-chave: dc.subject | Teses | - |
Palavras-chave: dc.subject | Programação logica | - |
Palavras-chave: dc.subject | Teoria dos grafos | - |
Título: dc.title | Reduçõ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 obtidas | - |
Tipo de arquivo: dc.type | livro digital | - |
Aparece nas coleções: | Repositório Institucional - Rede Paraná Acervo |
O Portal eduCAPES é oferecido ao usuário, condicionado à aceitação dos termos, condições e avisos contidos aqui e sem modificações. A CAPES poderá modificar o conteúdo ou formato deste site ou acabar com a sua operação ou suas ferramentas a seu critério único e sem aviso prévio. Ao acessar este portal, você, usuário pessoa física ou jurídica, se declara compreender e aceitar as condições aqui estabelecidas, da seguinte forma: