Análise da distribuição do número de operações de resolvedores SAT / Distribution\ s analysis of operations\ s number of SAT solvers

AUTOR(ES)

Poliana Magalhães Reis

FONTE

IBICT - Instituto Brasileiro de Informação em Ciência e Tecnologia

DATA DE PUBLICAÇÃO

28/02/2012

RESUMO

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 .

ASSUNTO(S)

chaff chaff np-complete np-completo p=np p=np sat sat sat solvers sat solvers zchaff. zchaff.

Documentos Relacionados

• Do número de Milnor ao número de Milnor de Lê
• ANALYSIS OF RESERVOIR ROCKS PLUGGING DURING WATER INJECTION OPERATIONS
• Um núcleo inteligente para processamento distribuído de resolvedores SAT em verificação por equivalências
• Análise de eventos em redes de distribuição por meio das transformadas Wavelet e S
• "Estudo anatômico da distribuição, tamanho e número dos linfonodos mediastinais em brasileiros adultos"