CMSOL é Counting Monadic Second Order Logic, ou seja, uma lógica de gráficos em que o domínio é o conjunto de vértices e arestas, existem predicados para adjacência vértice-vértice e incidência de aresta-vértice, quantificação sobre arestas, vértices, conjuntos de arestas e vértices conjuntos, e existe um predicado que expressa se o tamanho de S é n módulo p .
O famoso teorema de Courcelle afirma que se é uma propriedade de gráficos expressáveis em CMSOL, então para cada gráfico G de largura de árvore no máximo k pode ser decidido em tempo linear se Π é válido, desde que uma decomposição de árvore de G seja dada na entrada. Versões posteriores do teorema eliminaram o requisito de que uma decomposição em árvore é fornecida na entrada (porque é possível calcular com o algoritmo de Bodlaender ) e também permitia a otimização em vez de apenas a decisão; ou seja, dada uma fórmula MSOL ϕ ( S ) , também podemos calcular o conjunto maior ou menor S que satisfaz ϕ .
Minha pergunta diz respeito à adaptação do teorema de Courcelle a gráficos de largura de cliques limitada. Existe um teorema semelhante dizendo que, se você possui um MSOL1 que permite quantificar sobre vértices, arestas, conjuntos de vértices, mas não conjuntos de arestas, em seguida, é fornecido um gráfico de largura de cliques k (com a expressão de clique dada), para cada k fixo , pode ser decidido em tempo linear, se o gráfico G satisfaz alguma fórmula MSOL1 ϕ ; todas as referências que vi apontam para
Problemas lineares de otimização de tempo solucionável em gráficos de largura de clique limitada por Courcelle, Makowsky e Rotics, Teoria de sistemas computacionais, 2000.
Eu tentei ler o artigo, mas ele não é independente com relação à definição exata de MSOL1 e é francamente difícil de ler. Eu tenho duas perguntas sobre o que exatamente é possível otimizar no FPT, parametrizado pela largura de cliques do gráfico, se uma expressão de clique for fornecida na entrada.
Para ambas as perguntas, eu também gostaria de saber quais são as referências corretas ao reivindicar esses resultados. Desde já, obrigado!
fonte
Respostas:
Depois de perguntar um pouco mais, parece que as respostas para 1) e 2) são SIM. A otimização da cardinalidade de um conjunto é possível no LinEMSOL (como mencionado por Martin Lackner); como me disseram, a existência dos predicados de cardinalidade não é um problema, pois eles podem ser eficientemente manipulados por autômatos de árvores de estado finito, que devem seguir (mais explicitamente do que no artigo originalmente mencionado) de On parse trees e Myhill-Nerode- ferramentas de tipo para manipular gráficos de largura de classificação limitada .
fonte
http://www.labri.fr/perso/courcell/Textes1/BC-Makowsky-Rotics(2000).pdf (que é o artigo que você mencionou, mas com uma versão mais legível) define LinEMSOL (Definição 10). O LinEMSOL permite problemas de otimização do MSO1 e o Teorema 4 afirma que esses problemas são tratáveis por parâmetros fixos em relação à largura da clique. Portanto, a resposta para o seu segundo marcador / pergunta deve ser sim.
Sobre o primeiro item: Em "Vertex-menores, lógica monádica de segunda ordem e uma conjectura de Seese", de Bruno Courcelle e Sang-il Oum, os autores escrevem que "Pode-se provar que nenhuma fórmula MS φ (X) pode expressar , em toda estrutura, que um conjunto X tem cardinalidade uniforme [10] "onde [10] =" Courcelle, a lógica monádica de segunda ordem dos gráficos "
espero que ajude
fonte