\pagestyle{empty}
\begin{center}

\large

Univerzita Karlova v Praze

\medskip

Matematicko-fyzikální fakulta

\vfill

{\bf\Large BAKALÁŘSKÁ PRÁCE}

\vfill

\centerline{\mbox{\includegraphics[width=60mm]{logo.eps}}}

\vfill
\vspace{5mm}

{\LARGE Martin Koutecký}

\vspace{15mm}

% Název práce přesně podle zadání
{\LARGE\bfseries Optimalizace na grafech s omezenou stromovou šířkou přes vlastnosti
vyjádřitelné v MSOL}

\vfill

% Název katedry nebo ústavu, kde byla práce oficiálně zadána
% (dle Organizační struktury MFF UK)
Katedra aplikované matematiky

\vfill
\begin{tabular}{rl}

Vedoucí bakalářské práce: & doc. Mgr. Petr Kolman Ph.D. \\
\noalign{\vspace{2mm}}
Studijní program: & Informatika \\
\noalign{\vspace{2mm}}
Studijní obor: & Obecná informatika \\
\end{tabular}

\vfill

% Zde doplňte rok
Praha 2011

\end{center}

\newpage

%%% Následuje vevázaný list -- kopie podepsaného "Zadání bakalářské práce".
%% Toto zadání NENÍ součástí elektronické verze práce, nescanovat.

%%% Na tomto místě mohou být napsána případná poděkování (vedoucímu práce,
%%% konzultantovi, tomu, kdo zapůjčil software, literaturu apod.)

\openright

%\noindent
Nejprve děkuji vedoucímu práce doc. Mgr. Petru Kolmanovi Ph.D. za cenné rady,
doporučení a připomínky k práci a především všechen čas, který takto obětoval.

\medskip
Dále děkuji doc. RNDr. Jiřímu Fialovi Ph.D., jehož přednášky mě přivedly k zájmu o tematiku práce a
položily potřebné základy.

\medskip
V neposlední řadě patří obrovský dík mým rodičům, kteří mi poskytují potřebné zázemí a bez jejichž
podpory bych se nemohl studiu plně věnovat.

\newpage

%%% Strana s čestným prohlášením k bakalářské práci

\vglue 0pt plus 1fill

\noindent
Prohlašuji, že jsem tuto bakalářskou práci vypracoval samostatně a výhradně
s~použitím citovaných pramenů, literatury a dalších odborných zdrojů.

\medskip\noindent
Beru na~vědomí, že se na moji práci vztahují práva a povinnosti vyplývající
ze zákona č. 121/2000 Sb., autorského zákona v~platném znění, zejména skutečnost,
že Univerzita Karlova v Praze má právo na~uzavření licenční smlouvy o~užití této
práce jako školního díla podle §60 odst. 1 autorského zákona.

\vspace{10mm}

\hbox{\hbox to 0.5\hsize{%
V Praze dne 27. 5. 2011
\hss}\hbox to 0.5\hsize{%
Martin Koutecký
\hss}}

\vspace{20mm}
\newpage

%%% Povinná informační strana bakalářské práce

\vbox to 0.5\vsize{
\setlength\parindent{0mm}
\setlength\parskip{5mm}

Název práce:
Optimalizace na grafech s omezenou stromovou šířkou přes vlastnosti vyjádřitelné v MSOL
% přesně dle zadání

Autor:
Martin Koutecký

Katedra:  % Případně Ústav:
Katedra aplikované matematiky
% dle Organizační struktury MFF UK

Vedoucí bakalářské práce:
doc. Mgr. Petr Kolman Ph.D.
% dle Organizační struktury MFF UK, případně plný název pracoviště mimo MFF UK

Abstrakt: Courcellova věta mluví o výpočetní složitosti rozhodovacích problémů
definovaný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é stromové šíř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.
% abstrakt v rozsahu 80-200 slov; nejedná se však o opis zadání bakalářské práce

Klíčová slova: Courcellova věta, stromová šířka, monadická logika druhého řádu, logické hry
% 3 až 5 klíčových slov

\vss}\nobreak\vbox to 0.49\vsize{
\setlength\parindent{0mm}
\setlength\parskip{5mm}

Title: Optimization in graphs with bounded treewidth through properties expressible in MSOL
% přesný překlad názvu práce v angličtině

Author:
Martin Koutecký

Department:
Department of Applied Mathematics
% dle Organizační struktury MFF UK v angličtině

Supervisor:
doc. Mgr. Petr Kolman, Ph.D.
% dle Organizační struktury MFF UK, případně plný název pracoviště
% mimo MFF UK v angličtině

Abstract: Courcelle's theorem speaks about computational complexity of decision problems defined by
formulae in monadic second order logic over relational structures with bounded treewidth. 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. This 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. The thesis also contains
an implementation 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.

% abstrakt v rozsahu 80-200 slov v angličtině; nejedná se však o překlad
% zadání bakalářské práce

Keywords: Courcelle's theorem, treewidth, monadic second order logic, logic games
% 3 až 5 klíčových slov v angličtině

\vss}

\newpage
\openright
\pagestyle{plain}
