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 | - |
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 | Ribas, Bruno César | - |
Data de aceite: dc.date.accessioned | 2019-08-21T22:59:08Z | - |
Data de disponibilização: dc.date.available | 2019-08-21T22:59:08Z | - |
Data de envio: dc.date.issued | 2018-09-14 | - |
Data de envio: dc.date.issued | 2018-09-14 | - |
Data de envio: dc.date.issued | 2011 | - |
Fonte completa do material: dc.identifier | https://hdl.handle.net/1884/32514 | - |
Fonte: dc.identifier.uri | http://educapes.capes.gov.br/handle/1884/32514 | - |
Descrição: dc.description | Orientador : Prof. Dr. Fabiano Silva | - |
Descrição: dc.description | Dissertação (mestrado) - Universidade Federal do Paraná, Setor de Ciencias Exatas, Programa de Pós-Graduação em Informática. Defesa: Curitiba, 13/04/2011 | - |
Descrição: dc.description | Bibliografia: fls. 50-53 | - |
Descrição: dc.description | Resumo: Resolve dores de satisfatibilidade Booleana (SAT) são amplamente utilizados em verificação de software e hardware. A maioria dos resolve dores SAT modernos são baseados no algoritmo Davis-Putnam-Logemann-Loveland (DPLL) e precisam que a fórmula de entrada esteja na forma normal conjuntiva (CNF). No entanto para muitos problemas de verificação a representação em CNF não _e a forma mais natural de representação. Tipicamente os problemas são escritos em um modelo proposicional irrestrito e devem ser convertidos para CNF antes de aplicar o resolve dor SAT. A conversão do problema para CNF causa uma perda considerável de informação sobre a estrutura do problema. Apresentamos um novo resolve dor SAT que opera diretamente na forma proposicional irrestrita chamada ISCAS. O procedimento de busca proposto restringe as decisões _as variáveis da fórmula e propaga os efeitos da valoração para os operadores lógicos, diferente das abordagens que associam a decisão de valores a qualquer componente da fórmula. A avaliação experimental do resolve dor desenvolvido mostra um desempenho competitivo com o de outros resolve dores atuais para instâncias em representações irrestritas. | - |
Descrição: dc.description | Abstract: Boolean satis_ability (SAT) solvers are heavily used in hardware and software veri- _cation. Most state-of-art SAT solvers are base on Davis-Putnam-Logemann-Loveland (DPLL) algorithm and require the input formula to be in conjuctive normal form (CNF). However for most problems CNF is not a very natural representation. Typically these problems are more easily expressed using unrestricted propositional formulae and hence must be converted to CNF before SAT solvers can be applied. This conversion entails a considerable loss of information about the problem's structure. We present a new SAT solver that operates directly in an unrestricted propositional formulae named ISCAS. We consider branching from the inputs of the formula instead of choosing any node. We present empirical evidence showing that exploiting the original structure with branching restriction is competitive to current state-of-art SAT solvers of non-clausal benchmarks. | - |
Formato: dc.format | 53f. : il., grafs., tabs. | - |
Formato: dc.format | application/pdf | - |
Formato: dc.format | application/pdf | - |
Relação: dc.relation | Disponível em formato digital | - |
Palavras-chave: dc.subject | Teses | - |
Palavras-chave: dc.subject | Lógica de computador | - |
Palavras-chave: dc.subject | Logica simbolica e matematica | - |
Palavras-chave: dc.subject | Algoritmos | - |
Palavras-chave: dc.subject | Ciencia da computação | - |
Título: dc.title | Satisfatibilidade não-clausal restrita às variáveis de entrada | - |
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: