Reduções de problemas em grafos com soluções conexas para (MAX)SAT e adaptação de um resolvedor SAT e MAXSAT não clausal para as instâncias obtidas

Abstract

Resumo: São apresentadas neste trabalho reduções de problemas de grafos para SAT ou Max- SAT. Reduções dos problemas da Árvore de Steiner, Ciclo Hamiltoniano e Ciclo Hamiltoniano Mínimo são apresentadas, assim como uma redução de Clique para SAT (embora uma redução mais simples de MaxClique para MaxSAT seja conhecida). Todas essas reduções são lineares ou quadráticas no tamanho do grafo dado. Essas reduções usam um operador de cardinalidade que não está entre os operadores tradicionais da lógica proposicional. Entretanto, este operador pode ser convertido para uma fórmula em CNF em tempo linear, de forma que é possível utilizar um resolvedor SAT no estado-da-arte para resolver as instâncias geradas. Também é válido tentar resolver essas instâncias com um resolvedor SAT não clausal que suporte o operador. Desta forma, o operador pode ser utilizado diretamente, sem a necessidade de sua conversão para uma fórmula em CNF. Assim, este trabalho também apresenta uma versão modificada de um resolvedor SAT não clausal que reconhece o operador e resolve as instâncias de SAT e MaxSAT não clausal obtidas pelas reduções apresentadas. Além disso, este resolvedor é auxiliado por dois novos módulos. Um destes módulos é capaz de antecipar os retrocessos do resolvedor através da análise de sua valoração parcial com o grafo original. O outro, mais genérico, é capaz de armazenar as cláusulas aprendidas durante o processo e inferir valores verdade de acordo com a valoração parcial. As reduções apresentadas são comparadas com outras reduções publicadas anteriormente para os mesmos problemas, tanto no tamanho das fórmulas geradas quanto no desempenho de um resolvedor SAT as resolvendo. Além disso, o desempenho do resolvedor SAT não clausal modificado e seus módulos também é testado.

Abstract: It's presented in this work some new reductions from problems in graphs to SAT or MaxSAT. Reductions from Steiner Tree, Hamiltonian Cycle and Minimum Hamiltonian Cycle are shown, as well a reduction from Clique to SAT (although there's a simpler known reduction from MaxClique to MaxSAT). All these reductions are linear or quadratic in the size of the given graph. These reductions use a cardinality operator that is not among the traditional ones from the propositional logic. However, this operator can be translated to a CNF formula in linear time, so one can use a state-of-art clausal SAT solver to solve the generated instances. It's also worth trying to solve these instances with a non-clausal SAT solver that supports the operator. By doing this, one can use the operator directly, without converting it to a CNF formula. Thus, this work also presents a modified version of a non-clausal SAT solver that can handle this operator and solve the non-clausal SAT and MaxSAT instances obtained from the new reductions. Also, this new solver is helped by two new modules. One of these modules is able to anticipate the solver's backtracks by analyzing its current partial assignment on the original graph. The other, more generic one, is able to store the clauses learnt during the process and to infer truth values according to the partial assignment. The new reductions are compared against some other known reductions for the same problems, both in the size of the generated formulae and in the performance of a SAT solver working on them. Also, the performance of the modified non-clausal SAT solver and its new modules is tested.