Atenção:
O eduCAPES é um repositório de objetos educacionais, não sendo responsável por materiais de terceiros submetidos na plataforma. O usuário assume ampla e total responsabilidade quanto à originalidade, à titularidade e ao conteúdo, citações de obras consultadas, referências e outros elementos que fazem parte do material que deseja submeter. Recomendamos que se reporte diretamente ao(s) autor(es), indicando qual parte do material foi considerada imprópria (cite página e parágrafo) e justificando sua denúncia.
Caso seja o autor original de algum material publicado indevidamente ou sem autorização, será necessário que se identifique informando nome completo, CPF e data de nascimento. Caso possua uma decisão judicial para retirada do material, solicitamos que informe o link de acesso ao documento, bem como quaisquer dados necessários ao acesso, no campo abaixo.
Todas as denúncias são sigilosas e sua identidade será preservada. Os campos nome e e-mail são de preenchimento opcional. Porém, ao deixar de informar seu e-mail, um possível retorno será inviabilizado e/ou sua denúncia poderá ser desconsiderada no caso de necessitar de informações complementares.
Metadados | Descrição | Idioma |
---|---|---|
Autor(es): dc.contributor | Silva, Fabiano, 1972- | - |
Autor(es): dc.contributor | Universidade Federal do Paraná. Setor de Ciências Exatas. Programa de Pós-Graduação em Informática | - |
Autor(es): dc.creator | Oliveira, Ricardo Tavares de | - |
Data de aceite: dc.date.accessioned | 2025-09-01T11:47:31Z | - |
Data de disponibilização: dc.date.available | 2025-09-01T11:47:31Z | - |
Data de envio: dc.date.issued | 2024-11-04 | - |
Data de envio: dc.date.issued | 2024-11-04 | - |
Data de envio: dc.date.issued | 2013 | - |
Fonte completa do material: dc.identifier | https://hdl.handle.net/1884/30035 | - |
Fonte: dc.identifier.uri | http://educapes.capes.gov.br/handle/1884/30035 | - |
Descrição: dc.description | Orientador: Prof. Dr. Fabiano Silva | - |
Descrição: dc.description | Dissertação (mestrado) - Universidade Federal do Paraná, Setor de Ciências Exatas, Programa de Pós-Graduação em Informática. Defesa: Curitiba, 26/02/2013 | - |
Descrição: dc.description | Bibliografia : fls.97-102 | - |
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. | - |
Descrição: dc.description | Abstract: It's presented in this work some new reductions from problems in graphs to SAT or MaxSAT. Reductions from Steiner Tree, Hamiltonian Cycle and Minimum Hamiltonian Cycle are shown, as well a reduction from Clique to SAT (although there's a simpler known reduction from MaxClique to MaxSAT). All these reductions are linear or quadratic in the size of the given graph. These reductions use a cardinality operator that is not among the traditional ones from the propositional logic. However, this operator can be translated to a CNF formula in linear time, so one can use a state-of-art clausal SAT solver to solve the generated instances. It's also worth trying to solve these instances with a non-clausal SAT solver that supports the operator. By doing this, one can use the operator directly, without converting it to a CNF formula. Thus, this work also presents a modified version of a non-clausal SAT solver that can handle this operator and solve the non-clausal SAT and MaxSAT instances obtained from the new reductions. Also, this new solver is helped by two new modules. One of these modules is able to anticipate the solver's backtracks by analyzing its current partial assignment on the original graph. The other, more generic one, is able to store the clauses learnt during the process and to infer truth values according to the partial assignment. The new reductions are compared against some other known reductions for the same problems, both in the size of the generated formulae and in the performance of a SAT solver working on them. Also, the performance of the modified non-clausal SAT solver and its new modules is tested. | - |
Formato: dc.format | 102f. : il., tabs. | - |
Formato: dc.format | application/pdf | - |
Formato: dc.format | application/pdf | - |
Relação: dc.relation | Disponível em formato digital | - |
Palavras-chave: dc.subject | Programação logica | - |
Palavras-chave: dc.subject | Teoria dos grafos | - |
Palavras-chave: dc.subject | Ciência da computação | - |
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: