Use este identificador para citar ou linkar para este item: http://hdl.handle.net/1843/RVMR-79SPCP
Tipo: Tese de Doutorado
Título: Uma heurística de decisão baseada na subtração de cubos para solucionadores DPLL do problema de satisfabilidade
Autor(es): Romanelli Lodron Zuim
Primeiro Orientador: Claudionor Jose Nunes Coelho Junior
Primeiro Coorientador: José João Henriques de Sousa
Primeiro membro da banca : Henrique Pacca L. Luna
Segundo membro da banca: Marco Túlio de Oliveira Valente
Terceiro membro da banca: Antonio Otavio Fernandes
Quarto membro da banca: Newton Jose Vieira
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.
Abstract: This work proposes a new decision heuristic for Davis Putnam, Loveland and Logemann algorithm (DPLL)-based satisfiability (SAT) solvers based on cube subtraction. Each negated clause is viewed as a cube in the n-dimensional Boolean search space denoting a subspace where no satisfying assignments can be found. Cube subtraction, systematically subtracts all clause-cubes from the universal cube that represents the entire n-dimensional Boolean search space. If the result is an empty cube, then the problem is unsatisfiable; else the problem is satisfiable. This algorithm can be implemented by modifying the decision engine of a DPLL-based SAT solver. This modification restricts the choice of the next decision variable after a chronological backtrack step. Intuitively, the idea is to confine the search to a clause or a group of clauses, in the hope of getting out of non-solution regions, or regions where we can not find a yes or no answer to the instance, faster and/or learning more useful clauses. This idea is implemented in the well-known zChaff solver. The test suite includes 1252 instances from the DIMACs, IBM-CNF bounded model checking and microprocessor formal verification benchmarks. Significant improvements in execution time and number of timed-out instances have been observed in all cases. Given the breadth of the experimental evaluation, the disjoint cube subtraction search is claimed to be an effective algorithm for improving the performance of DPLL-based SAT solvers.
Assunto: Calculo proposicional
Processo decisorio
Algoritmos de computador
Computação
Programação heuristica
Idioma: Português
Editor: Universidade Federal de Minas Gerais
Sigla da Instituição: UFMG
Tipo de Acesso: Acesso Aberto
URI: http://hdl.handle.net/1843/RVMR-79SPCP
Data do documento: 21-Nov-2007
Aparece nas coleções:Teses de Doutorado

Arquivos associados a este item:
Arquivo TamanhoFormato 
zuim_tese.pdf2.75 MBAdobe PDFVisualizar/Abrir


Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.