Název:
Optimalizace na grafech s omezenou stromovou šířkou přes vlastnosti vyjádřitelné v MSOL
Překlad názvu:
Optimization in graphs with bounded treewidth
Autoři:
Koutecký, Martin ; Kolman, Petr (vedoucí práce) ; Kráľ, Daniel (oponent) Typ dokumentu: Bakalářské práce
Rok:
2011
Jazyk:
cze
Abstrakt: [cze][eng] Courcellova věta mluví o výpočetní složitosti rozhodovacích problémů defino- vaných formulemi monadické logiky druhého řádu nad relačními strukturami s omezenou stromovou šířkou. Pro pevnou stromovou šířku a vstupní formuli dává Courcellova věta algoritmus, který formuli rozhodne v lineárním čase nad strukturou dané stro- mové šířky. Práce podává samostatný důkaz Courcellovy věty pomocí metod teorie konečných modelů. Dále obsahuje důkazy všech potřebných prerekvizit hlavního důkazu, zejména v teorii konečných modelů široce využívané Ehrenfeuchtovy-Fraïssého věty. Práce též obsahuje implementaci algoritmu plynoucího z tohoto důkazu. Nakonec nastiňuje aktuální stav výzkumu dané oblasti a z něj plynoucí možnosti. 1Courcelle's theorem speaks about computational complexity of decision problems defined by formulae in monadic second order logic over relational structures with bounded treewodth. For a fixed treewidth and a fixed formula, Courcelle's theorem gives an algorithm, which decides the formula over a structure of said treewidth in linear time. is thesis provides a self-contained proof of Courcelle's theorem using methods of finite model theory. Furthermore it contains the proofs of all propositions and theorems upon which the main proof depends, notably the Ehrenfeucht-Fraïssé theorem widely used in finite model theory. e thesis also contains an implementa- tion of an algorithm which follows from the main proof. Finally a sketch of the current state of the art of the area of research is given, as well as the possibilities following from it. 1
Klíčová slova:
Courcellova věta; logické hry; monadická logika druhého řádu; stromová šířka; Courcelle's theorem; logic games; monadic second order logic; treewidth