Solução de problemas em Grafos através da Lógica Monádica de Segunda Ordem e da Decomposição em Árvore

Abstract

O Teorema de Courcelle afirma que todo problema definível em Lógica Monádica de Segunda Ordem (LMSO) pode ser resolvido em grafos que apresentam uma decomposição em árvore com treewidth limitada por uma constante, em tempo de execução linear, através de um algoritmo de parâmetro fixo. Mas como todo algoritmo, seu tempo de execução depende de uma constante, a qual depende do limite da treewidth e do tamanho da expressão MSO, apresentando crescimento super exponencial à medida que a treewidth aumenta. Alguns autores têm apresentado abordagens para evitar esse problema da constante. Neste trabalho, exploramos uma pesquisa feita em [12], que trata esse problema utilizando teoria dos jogos para a avaliação da expressão MSO, a partir da decomposição em árvore do grafo de entrada. São descritos neste trabalho, os conceitos sobre a tratabilidade por parâmetro fixo, sobre decomposição em árvore e treewidth, e a abordagem para a avaliação de uma expressão MSO com um foco na validação experimental da complexidade do tempo de execução do algoritmo.

ABSTRACT - The Courcelle’s Theorem states that every problem definable in Monadic Second Order Logic (MSOL) can be solved in graphs that present a tree decomposition with limited treewidth by a constant in linear running time through a fixed parameter algorithm. But, as in any algorithm, its running time depends on a constant, which, in turn, depends on the limit of treewidth and the size of the MSO expression, presenting super-exponential growth as the treewidth increases. Some authors have presented approaches to avoid this huge constant problem. In this work, we explore research described in [12], which deals with this problem using game theory to evaluate the MSO expression using the tree decomposition of the input graph. In this work are described the concepts of fixed parameter tractability, tree decomposition and treewidth, and the approach to the evaluation of an MSO expression with a focus on experimental validation of the running time complexity of the algorithm.