CMSO-transducing tree-like graph decompositions

Declaração do Problema
O artigo aborda o problema de transduzir decomposições de grafos em forma de árvore a partir de grafos usando lógica Monádica de Segunda Ordem (MSO). Especificamente, busca-se determinar se decomposições como decomposições modulares, decomposições por cortes (split) e decomposições bi-join podem ser geradas via transduções CMSO (MSO com predicados de contagem módulo).

Trabalhos anteriores de Courcelle estabeleceram que tais decomposições poderiam ser transduzidas usando MSO invariante à ordem, uma lógica estritamente mais expressiva que a CMSO. A questão aberta central abordada aqui é se a dependência de uma ordem linear dos vértices pode ser eliminada, permitindo que essas decomposições sejam definidas puramente dentro da CMSO. Isso é significativo porque as transduções CMSO preservam a equivalência entre reconhecibilidade por autômatos de árvores e definibilidade em lógica para classes de grafos de largura de clique limitada (ou largura de rank).

Metodologia
Os autores desenvolvem um framework baseado nas propriedades estruturais de sistemas de conjuntos e sistemas de bipartição. A metodologia procede em várias etapas:

1. Sistemas de Conjuntos Laminar e Árvores: O desafio técnico central é transduzir a árvore laminar de um sistema de conjuntos (uma árvore que representa uma família de conjuntos não sobrepostos). Os autores introduzem uma técnica para representar cada nó interno da árvore laminar usando um par de folhas de sua subárvore. Eles provam que, para qualquer árvore laminar, o conjunto de nós internos pode ser particionado em quatro conjuntos "finos". Para cada conjunto fino, existe uma "bi-coloração" (uma partição das folhas em dois conjuntos disjuntos de tamanho igual) que identifica unicamente os nós desse conjunto.
2. Seleção de Representantes via C2MSO: Usando a propriedade dos conjuntos finos, os autores constroem uma transdução não determinística $C_2$MSO. Essa transdução adivinha quatro bi-colorações e usa predicados de contagem ($C_2$) para definir uma fórmula que seleciona uma folha representante única para cada nó interno. Isso permite a construção da estrutura da árvore laminar (especificamente a relação de ancestralidade) a partir do sistema de conjuntos.
3. Extensão para Sistemas Fracamente-Partitivos e Fracamente-Bipartitivos: Os autores generalizam a construção da árvore laminar para sistemas de conjuntos fracamente-partitivos (que incluem módulos de grafos) e sistemas fracamente-bipartitivos de bipartições (que incluem cortes e bi-joins). Eles recorrem a teoremas estruturais (de Courcelle, Montgolfier e Rao) que afirmam que esses sistemas podem ser caracterizados por uma árvore laminar equipada com rótulos específicos de nós (degenerado, primo, linear) e ordens parciais nos filhos.
4. Decomposições Enriquecidas: Uma vez que a estrutura subjacente da árvore é transduzida, os autores usam transduções determinísticas MSO para adicionar o "enriquecimento" necessário (por exemplo, relações de aresta entre irmãos na árvore) requerido para reconstruir o grafo original. Isso inclui definir "arestas-m" para decomposições modulares, "arestas-c" e "arestas-t" para decomposições por cortes, e "arestas-r" para decomposições bi-join.

Principais Contribuições e Resultados
O artigo fornece os seguintes resultados principais, formalizados como transduções não determinísticas $C_2$MSO:

• Árvores Laminar: Uma transdução que, dado um sistema de conjuntos laminar, produz sua árvore laminar (Teorema 3.1).
• Árvores Fracamente-Partitivas: Uma transdução que, dado um sistema de conjuntos fracamente-partitivo, produz sua "árvore fracamente-partitiva" canônica (uma árvore laminar com rótulos e ordens parciais) (Teorema 4.3).
• Decomposições Modulares: Uma transdução que, dado um grafo direcionado, produz sua decomposição modular enriquecida (Teorema 4.6).
• Cotrees: Uma transdução que, dado um cografo, produz sua cotree (Corolário 4.9).
• Árvores Fracamente-Bipartitivas: Uma transdução que, dado um sistema fracamente-bipartitivo de bipartições, produz sua "árvore fracamente-bipartitiva" canônica (Teorema 5.4).
• Decomposições por Cortes (Split): Uma transdução que, dado um grafo direcionado fortemente conexo, produz sua decomposição por cortes enriquecida (Teorema 5.9).
• Decomposições Bi-join: Uma transdução que, dado um grafo não direcionado conexo, produz seu "grafo esqueleto" (uma estrutura equivalente à decomposição bi-join da qual o grafo pode ser reconstruído) (Teorema 5.13).

Significância e Alegações
Os autores afirmam que seus resultados melhoram trabalhos anteriores de Courcelle ao remover a exigência de invariância à ordem. Ao alcançar essas transduções usando apenas $C_2$MSO (que é mais fraca que a MSO invariante à ordem), eles demonstram que essas decomposições canônicas são definíveis sem assumir uma ordem linear sobre os vértices.

O artigo destaca uma consequência teórica específica: para classes de grafos onde os grafos "primos" (em relação a decomposições por cortes ou bi-join) têm largura de rank limitada e satisfazem a propriedade de que a reconhecibilidade equivale à definibilidade em CMSO, essa equivalência se estende a toda a classe. Isso permite a extensão de resultados conhecidos sobre a equivalência entre reconhecibilidade e definibilidade para classes de grafos mais amplas, como grafos hereditários de distância e grafos livres de $(gem, co\text{-}gem)$, que anteriormente não eram conhecidos por satisfazer essa propriedade sob a CMSO isoladamente.

Os autores também observam que seus métodos são gerais o suficiente para potencialmente se aplicar a outras estruturas, como a decomposição de matróides de Tutte ou decomposições modulares de 2-estruturas, embora essas não sejam explicitamente construídas no artigo. Finalmente, eles levantam a questão aberta de se os predicados de contagem ($C_2$) são estritamente necessários para essas transduções ou se a MSO padrão é suficiente.