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

Abstract

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.