Análise das distribuições do número de operaçõies de resolvedores SAT (2012)
- Autores:
- Autor USP: REIS, POLIANA MAGALHÃES - IME
- Unidade: IME
- Sigla do Departamento: MAC
- Assunto: INTELIGÊNCIA ARTIFICIAL
- Idioma: Português
- Resumo: No estudo da complexidade de problemas computacionais destacam-se duas classes conhecidas como P e NP. A questão P=NP é um dos maiores problemas nãp resolvidos em Ciência da Computação teórica e Matemática contemporânea. O problema SAT foi o primeiro reconhecido como NP-completo e consiste em verificar se uma detrminada fórmula da lógica proporcional clássica é ou não satisfazível. As implementações de algoritmos para resolver problemas SAT são conhecidas como resolvedores SAT (STA solvers). Existem diversas aplicações em Ciência da Computação 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 coloração de grafos, problemas de agendamento e problemas de planejamento. Dentre os mais eficientes algoritmos para resolvedores de SAT estão Sato, Grasp, Chaff, MiniSat e Berkmin. O algoritmo Chaff é baseado no algoritmo DPLL o qual existe há mais de 40 anos e é a estratégia mais utilizada para os Sat solvers. Essa dissertação apresenta um estudo aprofundado do comportamento do zChaff (uma implementação muito eficiente do Chaff) para saber o que esperar de suas execuções em geral.
- Imprenta:
- Data da defesa: 28.02.2012
-
ABNT
REIS, Poliana Magalhães. Análise das distribuições do número de operaçõies de resolvedores SAT. 2012. Dissertação (Mestrado) – Universidade de São Paulo, São Paulo, 2012. Disponível em: http://www.teses.usp.br/teses/disponiveis/45/45134/tde-21012013-220441. Acesso em: 24 abr. 2024. -
APA
Reis, P. M. (2012). Análise das distribuições do número de operaçõies de resolvedores SAT (Dissertação (Mestrado). Universidade de São Paulo, São Paulo. Recuperado de http://www.teses.usp.br/teses/disponiveis/45/45134/tde-21012013-220441 -
NLM
Reis PM. Análise das distribuições do número de operaçõies de resolvedores SAT [Internet]. 2012 ;[citado 2024 abr. 24 ] Available from: http://www.teses.usp.br/teses/disponiveis/45/45134/tde-21012013-220441 -
Vancouver
Reis PM. Análise das distribuições do número de operaçõies de resolvedores SAT [Internet]. 2012 ;[citado 2024 abr. 24 ] Available from: http://www.teses.usp.br/teses/disponiveis/45/45134/tde-21012013-220441
Como citar
A citação é gerada automaticamente e pode não estar totalmente de acordo com as normas
