Satisfatibilidade não-clausal restrita às variáveis de entrada

Registro completo de metadados
MetadadosDescriçãoIdioma
Autor(es): dc.contributorSilva, Fabiano-
Autor(es): dc.contributorUniversidade Federal do Paraná. Setor de Ciências Exatas. Programa de Pós-Graduação em Informática-
Autor(es): dc.creatorRibas, Bruno César-
Data de aceite: dc.date.accessioned2019-08-21T22:59:08Z-
Data de disponibilização: dc.date.available2019-08-21T22:59:08Z-
Data de envio: dc.date.issued2018-09-14-
Data de envio: dc.date.issued2018-09-14-
Data de envio: dc.date.issued2011-
Fonte completa do material: dc.identifierhttps://hdl.handle.net/1884/32514-
Fonte: dc.identifier.urihttp://educapes.capes.gov.br/handle/1884/32514-
Descrição: dc.descriptionOrientador : Prof. Dr. Fabiano Silva-
Descrição: dc.descriptionDissertaçã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.descriptionBibliografia: fls. 50-53-
Descrição: dc.descriptionResumo: 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.descriptionAbstract: 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.format53f. : il., grafs., tabs.-
Formato: dc.formatapplication/pdf-
Formato: dc.formatapplication/pdf-
Relação: dc.relationDisponível em formato digital-
Palavras-chave: dc.subjectTeses-
Palavras-chave: dc.subjectLógica de computador-
Palavras-chave: dc.subjectLogica simbolica e matematica-
Palavras-chave: dc.subjectAlgoritmos-
Palavras-chave: dc.subjectCiencia da computação-
Título: dc.titleSatisfatibilidade não-clausal restrita às variáveis de entrada-
Tipo de arquivo: dc.typelivro digital-
Aparece nas coleções:Repositório Institucional - Rede Paraná Acervo

Não existem arquivos associados a este item.