• JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
 
  Bookmark and Share
 
 
Dissertação de Mestrado
DOI
10.11606/D.45.2012.tde-21012013-220441
Documento
Autor
Nome completo
Poliana Magalhães Reis
E-mail
Unidade da USP
Área do Conhecimento
Data de Defesa
Imprenta
São Paulo, 2012
Orientador
Banca examinadora
Finger, Marcelo (Presidente)
Cozman, Fabio Gagliardi
Silva, Flavio Soares Correa da
Título em português
Análise da distribuição do número de operações de resolvedores SAT
Palavras-chave em português
Chaff
NP-complete
P=NP
SAT
SAT Solvers
zChaff.
Resumo em português
No estudo da complexidade de problemas computacionais destacam-se duas classes conhecidas como P e NP. A questao P=NP e um dos maiores problemas nao resolvidos em Ciencia da Compu- tacao teorica e Matematica contemporanea. O problema SAT foi o primeiro problema reconhecido como NP-completo e consiste em verificar se uma determinada formula da logica proposicional clas- sica e ou nao satisfazivel. As implementacoes de algoritmos para resolver problemas SAT sao conhe- cidas como resolvedores SAT (SAT Solvers). Existem diversas aplicacoes em Ciencia da Computacao que podem ser realizadas com SAT Solvers e com outros resolvedores de problemas NP-completos que podem ser reduzidos ao SAT como por exemplo problemas de coloracao de grafos, problemas de agendamento e problemas de planejamento. Dentre os mais eficientes algoritmos para resolvedores de SAT estao Sato, Grasp, Chaff, MiniSat e Berkmin. O Algoritmo Chaff e baseado no Algoritmo DPLL o qual existe a mais de 40 anos e e a estrategia mais utilizada para os Sat Solvers. Essa dissertacao apresenta um estudo aprofundado do comportamento do zChaff (uma implementacao muito eficiente do Chaff) para saber o que esperar de suas execucoes em geral .
Título em inglês
Distribution's analysis of operations's number of SAT solvers
Palavras-chave em inglês
Chaff
NP-completo
P=NP
SAT
SAT Solvers
zChaff.
Resumo em inglês
In the study of computational complexity stand out two classes known as P and NP. The question P = NP is one of the greatest unsolved problems in theoretical computer science and contemporary mathematics. The SAT problem was first problem recognized as NP-complete and consists to check whether a certain formula of classical propositional logic is satisfiable or not. The implementations of algorithms to solve SAT problems are known as SAT solvers. There are several applications in computer science that can be performed with SAT solvers and other solvers NP- complete problems can be reduced to SAT problems such as graph coloring, scheduling problems and planning problems. Among the most efficient algorithms for SAT solvers are Sato, Grasp, Chaf, MiniSat and Berkmin. The Chaff algorithm is based on the DPLL algorithm which there is more than 40 years and is the most used strategy for Sat Solvers. This dissertation presents a detailed study of the behavior of zChaff (a very efficient implementation of the Chaff) to know what to expect from their performance in general.
 
AVISO - A consulta a este documento fica condicionada na aceitação das seguintes condições de uso:
Este trabalho é somente para uso privado de atividades de pesquisa e ensino. Não é autorizada sua reprodução para quaisquer fins lucrativos. Esta reserva de direitos abrange a todos os dados do documento bem como seu conteúdo. Na utilização ou citação de partes do documento é obrigatório mencionar nome da pessoa autora do trabalho.
tesepoliana.pdf (12.80 Mbytes)
Data de Publicação
2013-01-23
 
AVISO: Saiba o que são os trabalhos decorrentes clicando aqui.
Todos os direitos da tese/dissertação são de seus autores
Centro de Informática de São Carlos
Biblioteca Digital de Teses e Dissertações da USP. Copyright © 2001-2019. Todos os direitos reservados.