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 | Mello, Arthur Renato | - |
Data de aceite: dc.date.accessioned | 2025-09-01T12:26:39Z | - |
Data de disponibilização: dc.date.available | 2025-09-01T12:26:39Z | - |
Data de envio: dc.date.issued | 2024-11-03 | - |
Data de envio: dc.date.issued | 2024-11-03 | - |
Data de envio: dc.date.issued | 2010 | - |
Fonte completa do material: dc.identifier | https://hdl.handle.net/1884/26705 | - |
Fonte: dc.identifier.uri | http://educapes.capes.gov.br/handle/1884/26705 | - |
Descrição: dc.description | Orientador: Prof. 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, 10/09/2010 | - |
Descrição: dc.description | Inclui bibliografia | - |
Descrição: dc.description | Resumo: Este estudo apresenta a criação de uma plataforma para o desenvolvimento e a avaliação de algoritmos que visam resolver o problema de definir a satisfatibilidade de uma fórmula em lógica proposicional. Muitos estudos já foram realizados sobre o problema da satisfatibilidade, principalmente sobre fórmulas na Forma Normal Conjuntiva. Com isso, muitas técnicas foram desenvolvidas baseadas nas características exclusivas desse formato. O algoritmo conhecido como DPLL é utilizado como base técnica para os principais resolvedores atuais. Heurísticas de aprendizado sobre erros e melhores estruturas de representação são os pontos fortes dos algoritmos mais modernos. Porém, a utilização de um formato de representação menos restritivo, não clausal, permite aos resolvedores atuarem sobre um número maior de domínios. Testes automatizados de circuitos são um bom exemplo de aplicação para um resolvedor não clausal. Dada a diversidade de aplicações, o processo de desenvolvimento de tais algoritmos exige a decisão de qual conjunto de técnicas e heurísticas deve ser utilizado para um melhor desempenho. Nesse cenário, uma plataforma de desenvolvimento robusta, que permita a implementação de estruturas e heurísticas específicas, facilita esse processo de decisão, possibilitando, assim, análises comparativas mais precisas entre diversas soluções. | - |
Descrição: dc.description | Abstract: This study presents a platform for the development and evaluation of algorithms designed to solve the problem of defining the satisfiability of a propositional logic formula. Many studies have been conducted on the problem of satisfiability, acting mainly on formulas in Conjunctive Normal Form. With this, many techniques were developed based on the unique characteristics of this format. The algorithm known as DPLL is mainly used as the technical basis for current solvers. Heuristics forlearning from errors and better representation structures are one of the most important characteristics of modern solvers. However, the use of a representation format less restrictive, non-clausal, allows solvers act upon a larger number of domains. Automated circuit testing is a good example of application for a non-clausal solver. Given the diversity of applications, the process of developing such algorithms requires decisions on which a set of techniques and heuristics must be used for better performance. In this scenario, a robust development platform, which allows the implementation of structures and heuristics for specific domains, eases the process of those decisions. This can make analysis between different solutions more accurate. | - |
Formato: dc.format | v, 78 p. : il. ; 30 cm. | - |
Formato: dc.format | application/pdf | - |
Formato: dc.format | application/pdf | - |
Relação: dc.relation | Disponível em formato digital | - |
Palavras-chave: dc.subject | Algorítmos de computador | - |
Palavras-chave: dc.subject | Algorítmos | - |
Palavras-chave: dc.subject | Lógica simbólica e matemática | - |
Palavras-chave: dc.subject | Calculo proposicional | - |
Palavras-chave: dc.subject | Ciência da computação | - |
Título: dc.title | Plataforma para desenvolvimento e avaliação de resolvedores SAT | - |
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: