Recognizability equals CMSO-definability for graphs of rank-width at most two

Resumo Técnico: Reconhecibilidade equivale à definibilidade em CMSO para grafos de largura de rank no máximo dois

Enunciado do Problema
O artigo aborda o problema da "reconhecibilidade versus definibilidade" dentro do programa de Courcelle, especificamente para classes de grafos densos. A questão central é se toda propriedade de grafo que é VR-reconhecível (saturada por uma congruência finita da álgebra de substituição de vértices) é também definível em lógica Monádica de Segunda Ordem com Contagem (CMSO) em classes de largura de rank limitada. Embora essa equivalência seja conhecida para largura de árvore limitada (grafos esparsos) e largura de clique linear limitada, ela permanecia aberta para o caso geral de largura de rank limitada. Especificamente, o artigo foca na classe $\mathcal{C}_2$ de grafos finitos com largura de rank no máximo dois, avançando o problema do caso de largura de rank um (decomposição de divisão/split-decomposition) para o primeiro nível não trivial de largura de rank limitada.

Metodologia e Abordagem Estrutural
A prova procede separando os testemunhos estruturais dos objetos lógicos a serem transduzidos, tratando o problema em duas etapas principais: grafos primos de divisão (split-prime) e grafos arbitrários.

1. Organização Estrutural de Grafos Primos de Divisão:

   • Os autores utilizam a teoria de funções de conectividade de Clark–Whittle, especificamente os teoremas da "flor" (flower) e da "árvore parcial máxima" (maximal partial-tree), para organizar separações exatas de corte-rank-dois não sequenciais.
   • Eles definem núcleos canônicos (canonical cores) para classes de equivalência forte de separações. Ao fixar uma orientação de "âncora", esses núcleos formam uma família laminar CMSO-definível.
   • Uma distinção fundamental é feita entre a árvore parcial auxiliar (usada para provar limites de largura) e a árvore laminar canônica (que é transduzida). A árvore auxiliar não é transduzida em si; ela serve apenas para provar que as peças locais admitem layouts de largura de clique linear uniformemente limitados.

2. Largura Linear Local Limitada:

   • Os autores constroem "torsos corrigidos" (corrected torsos) para as peças locais da decomposição laminar canônica. Esses torsos substituem blocos de fronteira por triplas de terminais (vértices de porta) enquanto preservam propriedades de corte-rank via operações algébricas lineares sobre $\mathbb{F}_2$.
   • Utilizando o teorema de exibição de largura de ramo (branch-width) três de Hall–Oxley–Semple–Whittle, os autores provam que componentes livres de flores admitem layouts contíguos de porta (port-contiguous layouts) de largura de rank linear no máximo seis.
   • Isso estabelece que cada peça local da decomposição possui uma largura de rank linear limitada por uma constante (especificamente, no máximo seis para o torso, e largura de clique linear limitada para a expansão local).

3. Frames Coerentes e Avaliação de Estado Finito:

   • Para permitir a avaliação lógica, os autores introduzem seletores de frames coerentes (coherent frame selectors) (cores unárias) para escolher bases de linhas ordenadas para os cortes de fronteira. Isso garante que as relações algébricas lineares entre peças locais adjacentes sejam consistentes e definíveis.
   • Eles definem um grafo de porta de rank-dois válido e um conjunto finito de estados representando as classes de congruência VR desses grafos.
   • Uma avaliação de baixo para cima (bottom-up) é realizada na árvore laminar. As transições locais são definidas por fórmulas CMSO porque as expansões locais (formadas pela substituição de representantes para os estados filhos) possuem largura de clique linear limitada. Isso baseia-se no teorema de Bojańczyk, Grohe e Pilipczuk, que garante a definibilidade CMSO para propriedades em classes de largura de clique linear limitada.

4. Elevação para Grafos Arbitrários:

   • O resultado é estendido de grafos primos para todos os grafos de largura de rank no máximo dois usando a decomposição de divisão canônica (Cunningham).
   • Os autores empregam uma transdução CMSO da decomposição de divisão enriquecida (Campbell et al.) para lidar com a árvore de fator (factor tree).
   • Para fatores não primos (cliques e estrelas), a largura de clique linear limitada é trivial. Para fatores primos, o resultado previamente estabelecido para o caso primo aplica-se.
   • Componentes conexos são tratados via um cálculo de monoide comutativo finito sobre os estados das raízes dos componentes, expressável em CMSO usando predicados de cardinalidade modular.

Principais Contribções e Resultados

• Teorema Principal: O artigo prova que, para a classe $\mathcal{C}_2$ (grafos de largura de rank $\le 2$), uma linguagem $L \subseteq \mathcal{C}_2$ é VR-reconhecível se, e somente se, é definível por uma sentença CMSO.
• Interface Estrutural: O trabalho estabelece uma interface rigorosa entre a teoria de árvore parcial de Clark–Whittle e as transduções lógicas. Demonstra que, embora a árvore parcial completa não seja transduzida, o núcleo laminar da árvore canônica é, e isso é suficiente para organizar a avaliação local.
• Limites de Largura: O artigo fornece limites explícitos para a largura de rank linear dos torsos locais (no máximo seis) e para a largura de clique linear das expansões locais, que são suficientes para invocar teoremas de definibilidade lógica existentes.
• Tratamento de Cortes Não Sequenciais: A metodologia organiza com sucesso cortes de rank-dois não sequenciais em uma estrutura laminar, superando o problema de que grafos de largura de rank um (como árvores) podem ter largura de clique linear ilimitada.

Significância e Alegações
O artigo afirma que avança o problema da reconhecibilidade-versus-definibilidade da largura de clique linear limitada para o primeiro nível não trivial de largura de rank limitada além do caso de decomposição de divisão.

• Modéstia das Alegações: Os autores declaram explicitamente que o argumento não implica que grafos de largura de rank dois tenham largura de clique linear limitada (eles não têm). Em vez disso, a significância reside no fato de que seus cortes de rank-dois não sequenciais podem ser organizados em um esqueleto laminar definível onde os torsos de porta individuais possuem uma limitação linear uniforme.
• Obstáculos Futuros: A conclusão identifica o obstáculo estrutural para estender este resultado para larguras de rank superiores: a necessidade de um análogo do teorema de exibição de Hall–Oxley–Semple–Whittle suficientemente forte para exibir blocos de fronteira sucessivos para funções de conectividade de rank superior, ou um mecanismo diferente para gerar torsos locais de largura limitada. O argumento atual é desenhado de modo que tal substituição poderia, teoricamente, ser inserida sem alterar a estrutura de avaliação de estado finito.

Em resumo, o artigo prova que a equivalência entre VR-reconhecibilidade e CMSO-definibilidade ocorre para largura de rank no máximo dois ao construir uma decomposição laminar transduzível por CMSO de grafos primos, provando limites uniformes de largura para os torsos resultantes e elevando o resultado via decomposição de divisão.