• Entrar
    Ver item 
    •   Página inicial
    • BIBLIOTECA DIGITAL: Teses & Dissertações
    • 40001016034P5 Programa de Pós-Graduação em Informática
    • Teses
    • Ver item
    •   Página inicial
    • BIBLIOTECA DIGITAL: Teses & Dissertações
    • 40001016034P5 Programa de Pós-Graduação em Informática
    • Teses
    • Ver item
    JavaScript is disabled for your browser. Some features of this site may not work without it.

    Arco consistência generalizada em codificações SAT relativas

    Thumbnail
    Visualizar/Abrir
    R - T - RICARDO TAVARES DE OLIVEIRA.pdf (991.6Kb)
    Data
    2017
    Autor
    Oliveira, Ricardo Tavares de
    Metadata
    Mostrar registro completo
    Resumo
    Resumo: Várias codificações de problemas relevantes para SAT ou suas variações são conhecidas e estudadas pela comunidade. Uma possível maneira de mensurar a eficiência destas codificações consiste em avaliar a manutenção da Arco Consistência Generalizada (ACG) da fórmula resultante pelo resolvedor SAT. Ao melhor de nosso conhecimento, não há estudos sobre a manutenção de tal consistência para codificações relativas, que descrevem relações binárias sobre um dado conjunto de elementos do problema. Neste trabalho, é apresentado um estudo sobre a Arco Consistência Generalizada em codificações SAT relativas. É mostrado que, dependendo das propriedades da relação codificada, as fórmulas obtidas por estas codificações são mantidas ACG pelo procedimento da Propagação Unitária. Conjectura-se também que estas codificações não podem ser polinomialmente restritas para mantê-las ACG. Neste trabalho, é também apresentado um método para manter uma consistência parcial nas fórmulas obtidas pelas codificações relativas. O método é baseado na manutenção da árvore de dominantes do grafo induzido pela relação codificada, durante o processo de busca do resolvedor SAT. Resultados experimentais indicam que o método pode reduzir o número de decisões realizadas pelo resolvedor e, logo, o espaço de busca explorado. Outras contribuições deste trabalho incluem codificações relativas para conectividade em grafos e para o problema da Árvore de Steiner, um framework genérico para unificar as codificações relativas conhecidas, um algoritmo polinomial para SAT para fórmulas mantidas ACG, e a implementação de algoritmos que mantêm árvores de dominantes para grafos dinâmicos dentro do código-fonte de um resolvedor SAT no estado-da-arte.
     
    Abstract: Many encodings from relevant problems to SAT or its variants are known and studied by the community. One possible way to measure the efficiency of these encodings consists on evaluating the maintenance of the Generalized Arc Consistency (GAC) of the resulting formula by the SAT solver. To the best of our knowledge, there is no study about such consistency for relative encodings, that describe binary relations over a given set of elements from the problem. In this work, it is presented a study about the Generalized Arc Consistency for relative SAT encodings. It is shown that, depending on the properties of the encoded relation, the formulae obtained by such encodings are maintened GAC by the Unit Propagation procedure. It is also conjectured that these encodings cannot be polynomially restricted in order to maintain them GAC. In this work, it is also presented a method to maintain a partial consistency on the formulae obtained by relative encoding. The method is based on the maintenance of the dominator tree of the underlying graph, during the search procedure of the SAT solver. Experimental evaluations indicate that the method may reduce the number of decisions made by the solver, and, thus, the search space it explores. Other contributions of this work include relative encodings for graph connectivity and for the Steiner Tree problem, a generic framework unifying known relative encodings, a polynomial-time algorithm for SAT for formulae maintened GAC, and the implementation of algorithms that maintain dominator trees for dynamic graphs inside the source code of a state-of-the-art SAT solver.
     
    URI
    https://hdl.handle.net/1884/46292
    Collections
    • Teses [132]

    DSpace software copyright © 2002-2022  LYRASIS
    Entre em contato | Deixe sua opinião
    Theme by 
    Atmire NV
     

     

    Navegar

    Todo o repositórioComunidades e ColeçõesPor data do documentoAutoresTítulosAssuntosTipoEsta coleçãoPor data do documentoAutoresTítulosAssuntosTipo

    Minha conta

    EntrarCadastro

    Estatística

    Ver as estatísticas de uso

    DSpace software copyright © 2002-2022  LYRASIS
    Entre em contato | Deixe sua opinião
    Theme by 
    Atmire NV