CMSOL est la logique de deuxième ordre monadique, c'est-à-dire une logique de graphiques où le domaine est l'ensemble des sommets et des arêtes, il y a des prédicats pour la contiguïté des sommets et les incidences des arêtes et des sommets, il y a une quantification sur les arêtes, les sommets, les ensembles d'arêtes et les sommets. ensembles, et il existe un prédicat qui exprime si la taille de S est n modulo p .
Le célèbre théorème de Courcelle déclare que si est une propriété de graphes exprimables en CMSOL, alors pour chaque graphe G de largeur d'arbre au plus k, il peut être décidé en temps linéaire si Π est vrai , à condition qu'une décomposition arborescente de G soit donnée en entrée. Les versions ultérieures du théorème ont supprimé l'exigence qu'une décomposition d'arbre soit donnée en entrée (car on peut être calculé avec l'algorithme de Bodlaender ), et a également permis une optimisation au lieu d'une simple décision; c'est-à-dire, étant donné une formule MSOL ϕ ( S ), nous pouvons également calculer le plus grand ou le plus petit ensemble S qui satisfait ϕ .
Ma question concerne l'adaptation du théorème de Courcelle à des graphes de largeur de clique bornée. Il existe un théorème similaire qui dit que si vous avez un MSOL1 qui permet la quantification sur les sommets, les bords, les ensembles de sommets mais pas les ensembles de bords, alors étant donné un graphique de largeur de clique k (avec une expression de clique donnée), pour chaque k fixe, il peut être décidé en temps linéaire si le graphe G satisfait à une formule MSOL1 ϕ ; toutes les références que j'ai vues indiquent
Problèmes d'optimisation soluble dans le temps linéaire sur des graphiques de largeur de clique bornée par Courcelle, Makowsky et Rotics, Theory of Computing Systems, 2000.
J'ai essayé de lire le document, mais il n'est pas autonome par rapport à la définition exacte de MSOL1 et il est franchement difficile à lire. J'ai deux questions concernant ce qui est exactement possible d'optimiser en FPT, paramétré par la largeur de clique du graphe, si une expression de clique est donnée en entrée.
- MSOL1 autorise-t-il le prédicat pour tester la taille d'un ensemble modulo un certain nombre?
- Est-il possible de trouver un ensemble de taille minimum / maximum qui satisfait une formule MSOL1 ϕ ( S ) en FPT paramétré par largeur de clique, lorsque l'expression est donnée?
Pour ces deux questions, j'aimerais également savoir quelles sont les bonnes références à citer lorsque je revendique ces résultats. Merci d'avance!
la source
Réponses:
Après avoir demandé un peu plus, il semble que les réponses aux points 1) et 2) soient toutes les deux OUI. L'optimisation de la cardinalité d'un ensemble est possible dans LinEMSOL (comme mentionné par Martin Lackner); comme on me l'a dit, l'existence des prédicats de cardinalité ne pose aucun problème car ils peuvent être efficacement gérés par des automates d'arbres à états finis, qui devraient suivre (plus explicitement que dans l'article référencé à l'origine) de On parse trees et Myhill-Nerode- des outils de type pour gérer les graphiques de rang-largeur borné .
la source
http://www.labri.fr/perso/courcell/Textes1/BC-Makowsky-Rotics(2000).pdf (qui est le document que vous avez mentionné mais une version plus lisible) définit LinEMSOL (définition 10). LinEMSOL permet des problèmes d'optimisation MSO1 et le théorème 4 déclare que ces problèmes sont traitables à paramètres fixes en ce qui concerne la largeur de clique. La réponse à votre deuxième puce / question devrait donc être oui.
Concernant la première puce: Dans "Vertex-minors, monadic second-order logic, and a conjecture by Seese" de Bruno Courcelle et Sang-il Oum, les auteurs écrivent que "Il peut être prouvé qu'aucune formule MS φ (X) ne peut exprimer , dans chaque structure, qu'un ensemble X a même une cardinalité [10] "où [10] =" Courcelle, la logique monadique du second ordre des graphes "
J'espère que cela pourra aider
la source