Uma heurística de decisão baseada na subtração de cubos para solucionadores DPLL do problema de satisfabilidade

AUTOR(ES)

Romanelli Lodron Zuim

DATA DE PUBLICAÇÃO

2007

RESUMO

Este trabalho propõe uma nova heurística de decisão para solucionadores do problema da satisfabilidade (SAT) baseados no algoritmo de Davis Putnam, Logemann e Loveland (DPLL). Essa heurística se baseia na subtração de cubos. Cada cláusula negada é visualizada como um cubo no espaço de procura booleano n-dimensional, denotando um subespaço onde nenhuma atribuição de valores às variáveis, que satisfaça a instância do problema, possa ser encontrada. A subtração dos cubos, sistematicamente subtrai todas as cláusulas-cubo do cubo universal, que representa todo o espaço booleano de procura. Se o resultado for um cubo vazio o problema não admite uma solução que o torne satisfazível, caso contrário, o problema é satisfazível. Esse algoritmo pode ser implementado modificando-se o mecanismo de decisão de solucionadores do problema da satisfabilidade baseados no algoritmo DPLL. Essas modificações restringem a escolha da próxima variável de decisão após um retrocesso cronológico. A intuição do algoritmo é confinar a procura a uma cláusula ou a um grupo de cláusulas, com o objetivo de escapar o mais rapidamente possível de regiões onde a solução não possa ser encontrada, ou uma resposta sim ou não possa ser dada para a instância, ou permitir o aprendizado de cláusulas mais úteis à solução do problema. Inicialmente foram utilizadas duas versões básicas de um solucionador DPLL, sem quaisquer das melhorias atualmente encontradas na literatura e posteriormente em um solucionador no estado-da-arte, o zChaff. Para o teste foram utilizados 1252 instâncias de problemas do DIMACS, IBM CNF BMC e resultados de verificação formal de microprocessadores. Observa-se uma melhoria significativa no tempo de execução e uma redução do número de instâncias não resolvidas dentro de um tempo limite, em todos os casos. Considerando a avaliação experimental, podemos concluir que a subtração de cubos é um algoritmo efetivo para a melhoria do desempenho de solucionadores do problema da satisfabilidade baseados no algoritmo DPLL.

ASSUNTO(S)

processo decisorio teses. computação teses. programação heuristica teses. calculo proposicional teses. algoritmos de computador teses.

Documentos Relacionados

• Uma Heurística Baseada em Programação Dinâmica para o Problema de Corte Bidimensional Guilhotinado 2-Estágios
• Proposta de uma heurística construtiva baseada na TOC para definição de mix de produção
• Uma abordagem heurística para o problema de otimização de distrito postal
• Uma heurística baseada em geração sequencial de padrões para o problema de corte de estoque unidimensional com um número reduzido de padrões
• Uma heurística de busca tabu simples para o problema de carregamento de paletes do produtor