\def\pgfsysdriver{pgfsys-dvisvgm.def}

\documentclass[table,english,dvisvgm]{beamer}


\usepackage[utf8]{luainputenc}
\usetheme{uzl-conference}


\makeatletter
\def\Gin@driver{dvisvg-graphics.def}
\input{dvisvgm-graphics.def}
\dvisvgmmodetrue
\makeatother

\usepackage{tikz}
\usepackage[english]{babel}

\usetikzlibrary{arrows.meta,graphs,graphdrawing.force,graphdrawing,graphdrawing.trees,quotes,positioning,graphdrawing.trees,decorations.pathmorphing,graphs.standard,decorations.pathreplacing,backgrounds,animations}

\tikzset{
  graph/.style={thick, >={Stealth[round,sep]}},
  node/.style={draw=#1,fill=#1!10,thick,circle,minimum size=4mm,inner sep=2pt,font=\footnotesize},
  node/.default=structure.fg,
  full node/.style={node=#1,fill=#1,draw=none,minimum
    size=4mm+0.2pt,outer sep=0pt,text=white}
}

\tikzset{only/.code args={<#1>#2}{\only<#1>{\tikzset{#2}}}}

\newbox\mytempbox
\newdimen\mytempdimen

\newcommand\includegraphicscopyright[3][]{%
  \leavevmode\vbox{\vskip3pt\raggedright\setbox\mytempbox=\hbox{\includegraphics[#1]{#2}}%
    \mytempdimen=\wd\mytempbox\box\mytempbox\par\vskip1pt%
    \sffamily\fontsize{3}{3.5}\selectfont\spaceskip=.333em\xspaceskip=.5em{\color{black}{\vbox{\hsize=\mytempdimen#3}}}\vskip3pt%
}}

\def\Class#1{\text{\normalfont\small$\operatorname{#1}$}}
\def\Lang#1{\text{\normalfont{\footnotesize\uppercase{#1}}}}
  
\def\basenum#1#2#3#4{%
  \ifnum#1>0\relax\foreach \i in {1,...,#1} {%
    \tikz[very thick,line cap=round,baseline=.0ex]
    \draw \foreach \j in {1,...,4} {(\j/#4,0) -- (\j/#4,#3) }
      (0,0) -- (5/#4,#3);%
    }\fi\ifnum#2>0\relax%
      \tikz[very thick,line cap=round,baseline=.0ex]{ \path (0,0);
       \foreach \i in {1,...,#2} \draw (\i/#4,0) -- ++(0,#3);}\fi%
}
\def\num#1#2{\basenum{#1}{#2}{1em}{8}}
\def\snum#1#2{\basenum{#1}{#2}{.6em}{12}}

\title{Algorithmic Metatheorems 2.0}

%\subtitle{}

\author{Till Tantau}

%\institute[Uni Lübeck]
%{
%  Institute of Theoretical Computer Science\\
%  Universität zu Lübeck
%}


\date{Theorietag in Speyer, September 2015}


\logo{\hskip-6mm\includegraphics[scale=.62]{uzl-logo-itcs.svg}}

\begin{document}


%\includeonlyframes{current}

\maketitle

\frame{\frametitle{Outline}\tableofcontents}


\section{Algorithmic Metatheorems}

\begin{frame}<3->[t]{A Well-Known Problem}
  
    \begin{columns}[T]
      \column{8.15cm}
  \only<1>{
    \includegraphicscopyright[width=\textwidth]{media/nuit.jpg}{Author Daniel Case,
      Creative Commons Attribution Sharelike License}
  }
  \only<2->{
    \tikz [graph] {
      \useasboundingbox (0,0) (8,7.8);
      \only<-5>{\node [above right]
      {\includegraphicscopyright[height=75mm]{media/Irvington_Nuits_floorplan.jpg}{Public
          Domain}};}
    \only<3->{
      \only<2-4>{\tikzgraphsset{how/.style={nodes={inner
            sep=0pt,as={\includegraphics[height=5mm]{media/osa.png}}}}}}
      \only<5->{\tikzgraphsset{how/.style={nodes={node,as=}}}}
        \graph [no placement, how] {
          a [x=4,y=6],
          b [x=3.7,y=7.2],
          c [x=2.8,y=6.2],
          d [x=3.7,y=5],
          e [x=5.5,y=4.5],
          f [x=4,y=3],
          g [x=3,y=2.5],
          h [x=3,y=1.5],
          i [x=4.5,y=2],
          j [x=5,y=3],
          k [x=6.5,y=3],
          l [x=3,y=3.5]
        };
        \only<4->{
        \graph [use existing nodes, edges=structure.fg]{
          {b,c} -- a -- d -- f -- {l,h,g,j -- {e,k}},
          b--c,
          l -- g -- h,
          i -- j,
          e -- k
        };
        }
      }
    }}
    \column{4cm}
    \begin{itemize}
    \item<3->We install {\small WLAN} routers in a home.
    \item<4->Adjacent routers interfere.
    \item<6->The abstract problem is of course \alert{3-colorability}.
    \end{itemize}
  \end{columns}
\end{frame}


\begin{frame}{3-Colorability is Hard.}
  
  \begin{itemize}
  \item 3-Colorability is a classical $\Class{NP}$-complete problem.
  \item Assuming $\Class P \neq \Class{NP}$, it 
    \alert{cannot} be solved efficiently.
  \end{itemize}
  \begin{block}{However}
    What happens, when the input has a 
    \alert{tree-like decomposition} and we can apply
    \alert{divide and conquer}?
  \end{block}
\end{frame}





\begin{frame}{Divide and Conquer, First Attempt}

  \only<1>{
    \begin{columns}[onlytextwidth,T]
    \column{.45\textwidth}
    \begin{quote}
      \alert{Entzwei und gebiete!\\
      Tüchtig Wort. – \\
      Verein und leite!\\
      Besserer Hort.}
  \end{quote}
  \par
    \hfill      Johann Wolfgang Goethe   
    \column{.5\textwidth}
    \includegraphics[width=\textwidth]{media/goethe.jpg}
  \end{columns}
}
\only<2->{
  \begin{columns}
    \column{.4\textwidth}
    \tikz [graph] {
      \path (25mm,0);
    \graph [no placement, edge=structure.fg, nodes={node,as=}] {
      f [x=4,y=3,only=<3->{full node=blue}],
      {
        [nodes={only=<4->{opacity=.25}},edges={only=<4->{opacity=.25}}]
        a [x=4,y=6,only=<5->{full node=green!50!black}],
        b [x=3.7,y=7.2,only=<5->{full node=red}],
        c [x=2.8,y=6.2,only=<5->{full node=blue}],
        d [x=3.7,y=5,only=<3->{full node=red}],
        {b,c} -- a -- d,
        b--c,
        d -- f
      },
      g [x=3,y=2.5],
      h [x=3,y=1.5,only=<9->{full node=red}],
      {
        [nodes={only=<7->{opacity=.25}},edges={only=<7->{opacity=.25}}]
        i [x=4.5,y=2,only=<8->{full node=blue}],
        j [x=5,y=3,only=<6->{full node=green!50!black}],
        k [x=6.5,y=3,only=<8->{full node=red}],
        e [x=5.5,y=4.5,only=<8->{full node=blue}],
      i -- j,
      f --j,
      j -- e -- k --j,
      },
      l [x=3,y=3.5],
      f -- {l,h,g},
      l -- g -- h,
    };
  }
  \column{.65\textwidth}
  \alt<10->{A \alert{game} describes how we can proceed.}%
  {\alert{Sometimes} divide and conquer can be applied to 3-colorability.
  \begin{itemize}
  \item<3-> Pick \alert{two appropriate} vertices and consider the 6
    possible colorings.
  \item<4-> A vertex \alert{screens} part of the graph
  \item<5-> and we can solve the problem \alert{recursively} on the
    \alert{independent} parts.
  \item<9-> It can happen that we have to \alert{remember several
      vertices} during the recursion.
  \end{itemize}}
\end{columns}
}  
\end{frame}


\def\gamegraph#1#2#3#4#5#6{%
  \tikz [graph] {
    \path(2,.5);
    
    \graph [no placement, edge=structure.fg, nodes={node,as=}] {
      a [x=4,y=6],
      b [x=3.7,y=7.2],
      c [x=2.8,y=6.2],
      d [x=3.7,y=5],
      e [x=5.5,y=4.5],
      f [x=4,y=3],
      g [x=3,y=2.5],
      h [x=3,y=1.5],
      i [x=4.5,y=2],
      j [x=5,y=3],
      k [x=6.5,y=3],
      l [x=3,y=3.5],
      {b,c} -- a -- d -- f -- {l,h,g,j -- {e,k}},
      b--c,
      l -- g -- h,
      i -- j,
      e -- k,
    };
    \node (heli) at (7,7) {\includegraphics[height=2cm]{media/helicopter.png}};
    
    \ifx#6//\else\draw [red] (#6) circle [radius=5mm];\fi

    \ifx#4//\else\node at (#4) {\includegraphics[height=9mm]{media/#5.png}};\fi
    \ifx#1//\else\node at ([yshift=1mm]#1) {\includegraphics[height=9mm]{media/red-person.png}};\fi
    \ifx#2//\else\node at ([yshift=1mm]#2) {\includegraphics[height=9mm]{media/blue-person.png}};\fi
    \ifx#3//\else\node at ([yshift=1mm]#3) {\includegraphics[height=9mm]{media/gray-person.png}};\fi
  }  
}


\begin{frame}{Robbers and Coppers}

  \begin{block}{Game Objective}
    The \alert{$k$ cops} try to catch a \alert{robber} by being
      on the \alert{same vertex} as her.
  \end{block}

  \begin{block}{Game Rules}
    \begin{enumerate}
    \item First the cops, then the robber pick a start vertex.
    \item A cop gets on a \alert{helicopter} and heads towards some
      vertex. 
    \item \alert{Meanwhile} the robber moves along \alert{unoccupied vertices}.
    \end{enumerate}    
  \end{block}
\end{frame}



\begin{frame}{Robbers and Coppers:}{Two Cops Do Not Catch the Robber.}

  \tikz [graph] {
    \path(2,.5);
    
    \graph [no placement, edge=structure.fg, nodes={node}] {
      a [x=4,y=6],
      b [x=3.7,y=7.2],
      c [x=2.8,y=6.2],
      d [x=3.7,y=5],
      e [x=5.5,y=4.5],
      f [x=4,y=3],
      g [x=3,y=2.5],
      h [x=3,y=1.5],
      i [x=4.5,y=2],
      j [x=5,y=3],
      k [x=6.5,y=3],
      l [x=3,y=3.5],
      {b,c} -- a -- d -- f -- {l,h,g,j -- {e,k}},
      b--c,
      l -- g -- h,
      i -- j,
      e -- k,
    };

    \node (heli) at (7,7) {\includegraphics[height=2cm]{media/helicopter.png}};

    \node [animate={freeze at end,opacity=0.1, duration=1s, begin on=click}] (go) at (8,5) [circle,fill=structure.fg!20] {Go};

    \animate {whom = focus, opacity = 0, shift=(j), duration=1ms, freeze at end}
    \animate {whom = rob, opacity = 0, shift=(i), duration=1ms, freeze at end}
    \animate {whom = robsmile, opacity = 0, shift=(d), duration=1ms, freeze at end}
    \animate {whom = c1,  opacity = 0, shift=(d), duration=1ms, freeze at end}
    \animate {whom = c2,  opacity = 0, shift=(f), duration=1ms, freeze at end}

    \animate {whom = rob, opacity = 0...1, freeze at end, begin on={click, of=go, delay=3s}, duration=2s}
    \animate {whom = c1, opacity = 0...1, freeze at end, begin on={click, of=go}, duration=2s}
    \animate {whom = c2, opacity = 0...1, freeze at end, begin on={click, of=go}, duration=2s}

    \animate {whom = c1, shift=(d) ... (heli), interpolation=spline,key spline control={0.5}{0}{0.5}{1},freeze at end, begin on={click, of=go, delay=6s}, duration=2s}
    \animate {whom = focus, opacity = 0...1, freeze at end, begin on={click, of=go, delay=8s}, duration=2s}

    \animate {whom = rob, shift=(i) ... (j) ... (k),key time=0,key time=0.4,key time=1,key spline control={0.5}{0}{1}{1},key spline control={0}{0}{0.5}{1}, interpolation=spline, freeze at end, begin on={click, of=go, delay=12s}, duration=2s}

    \animate {whom = c1, shift=(heli) ... (j), interpolation=spline,key spline control={0.5}{0}{0.5}{1}, freeze at end, begin on={click, of=go, delay=14s}, duration=2s}
    \animate {whom = focus, opacity = 1...0, freeze at end, begin on={click, of=go, delay=14s}, duration=2s}
   
    \animate {whom = c2, shift=(f) ... (heli), interpolation=spline,key spline control={0.5}{0}{0.5}{1}, freeze at end, begin on={click, of=go, delay=18s}, duration=2s}
    \animate {whom = focus, shift=(k) ... (k), freeze at end, begin on={click, of=go, delay=18}, duration=1ms}
    \animate {whom = focus, opacity = 0...1, freeze at end, begin on={click, of=go, delay=18s}, duration=2s}

    \animate {whom = rob, shift=(k) ... (e), interpolation=spline,key spline control={0.5}{0}{0.5}{1}, freeze at end, begin on={click, of=go, delay=22s}, duration=1s}

    \animate {whom = c2, shift=(heli) ... (k), interpolation=spline,key spline control={0.5}{0}{0.5}{1}, freeze at end, begin on={click, of=go, delay=24s}, duration=2s}
    \animate {whom = focus, opacity = 1...0, freeze at end, begin on={click, of=go, delay=24s}, duration=2s}
   
    \animate {whom = c1, shift=(j) ... (heli), interpolation=spline,key spline control={0.5}{0}{0.5}{1}, freeze at end, begin on={click, of=go, delay=26s}, duration=2s}
    \animate {whom = focus, shift=(e) ... (e), freeze at end, begin on={click, of=go, delay=26s}, duration=1ms}
    \animate {whom = focus, opacity = 0...1, freeze at end, begin on={click, of=go, delay=26s}, duration=2s}

    \animate {whom = rob, shift=(e) ... (j) ... (f) ... (d), key time=0,key time=0.35,key time=0.55,key time=1,key spline control={0.5}{0}{1}{1},key spline control={0}{0}{1}{1},key spline control={0}{0}{0.5}{1}, interpolation=spline,freeze at end, begin on={click, of=go, delay=30s}, duration=2s}

    \animate {whom = c1, shift=(heli) ... (e),  interpolation=spline,key spline control={0.5}{0}{0.5}{1},freeze at end, begin on={click, of=go, delay=32s}, duration=2s}
    \animate {whom = focus, opacity = 1...0, freeze at end, begin on={click, of=go, delay=32s}, duration=2s}

    \animate {whom = rob, opacity=1...0, freeze at end, begin on={click, of=go, delay=32s}, duration=2s}
    \animate {whom = robsmile, opacity=0...1, freeze at end, begin on={click, of=go, delay=32s}, duration=2s}
    
    \draw [name=focus, red] (0,0) circle [radius=5mm];

    \node (rob) {\includegraphics[height=9mm]{media/plain.png}};
    \node (robsmile) {\includegraphics[height=9mm]{media/smile.png}};
    \node (c1) at ([yshift=1mm]0,0) {\includegraphics[height=9mm]{media/red-person.png}};
    \node (c2) at ([yshift=1mm]0,0) {\includegraphics[height=9mm]{media/blue-person.png}};

    }
  

\end{frame}

\begin{frame}{Robbers and Coppers:}{Three Cops Always Catch the Robber.}

  \tikz [graph] {
    \path(2,.5);
    
    \graph [no placement, edge=structure.fg, nodes={node}] {
      a [x=4,y=6],
      b [x=3.7,y=7.2],
      c [x=2.8,y=6.2],
      d [x=3.7,y=5],
      e [x=5.5,y=4.5],
      f [x=4,y=3],
      g [x=3,y=2.5],
      h [x=3,y=1.5],
      i [x=4.5,y=2],
      j [x=5,y=3],
      k [x=6.5,y=3],
      l [x=3,y=3.5],
      {b,c} -- a -- d -- f -- {l,h,g,j -- {e,k}},
      b--c,
      l -- g -- h,
      i -- j,
      e -- k,
    };

    \node (heli) at (7,7) {\includegraphics[height=2cm]{media/helicopter.png}};

    \node [animate={freeze at end,opacity=0.1, duration=1s, begin on=click}] (go) at (8,5) [circle,fill=structure.fg!20] {Go};

    \animate {whom = focus, opacity = 0, shift=(g), duration=1ms, freeze at end}
    \animate {whom = rob, opacity = 0, shift=(g), duration=1ms, freeze at end}
    \animate {whom = roboh, opacity = 0, shift=(h), duration=1ms, freeze at end}
    \animate {whom = c1,  opacity = 0, shift=(d), duration=1ms, freeze at end}
    \animate {whom = c2,  opacity = 0, shift=(f), duration=1ms, freeze at end}
    \animate {whom = c3,  opacity = 0, shift=(a), duration=1ms, freeze at end}

    \animate {whom = rob, opacity = 0...1, freeze at end, begin on={click, of=go, delay=3s}, duration=2s}
    \animate {whom = c1, opacity = 0...1, freeze at end, begin on={click, of=go}, duration=2s}
    \animate {whom = c2, opacity = 0...1, freeze at end, begin on={click, of=go}, duration=2s}
    \animate {whom = c3, opacity = 0...1, freeze at end, begin on={click, of=go}, duration=2s}

    \animate {whom = c1, shift=(d) ... (heli),  interpolation=spline,key spline control={0.5}{0}{0.5}{1},freeze at end, begin on={click, of=go, delay=6s}, duration=2s}
    \animate {whom = focus, opacity = 0...1, freeze at end, begin on={click, of=go, delay=8s}, duration=2s}

    \animate {whom = rob, shift=(g) ... (h),   interpolation=spline,key spline control={0.5}{0}{0.5}{1}, freeze at end, begin on={click, of=go, delay=12s}, duration=1.5s}

    \animate {whom = c1, shift=(heli) ... (g),   interpolation=spline,key spline control={0.5}{0}{0.5}{1},freeze at end, begin on={click, of=go, delay=14s}, duration=2s}
    \animate {whom = focus, opacity = 1...0, freeze at end, begin on={click, of=go, delay=14s}, duration=2s}
   
    \animate {whom = c3, shift=(a) ... (heli),  interpolation=spline,key spline control={0.5}{0}{0.5}{1}, freeze at end, begin on={click, of=go, delay=18s}, duration=2s}
    \animate {whom = focus, shift=(h) ... (h),  interpolation=spline,key spline control={0.5}{0}{0.5}{1}, freeze at end, begin on={click, of=go, delay=18}, duration=1ms}
    \animate {whom = focus, opacity = 0...1, freeze at end, begin on={click, of=go, delay=18s}, duration=2s}

    \animate {whom = rob, opacity=1...0, freeze at end, begin on={click, of=go, delay=20s}, duration=2s}
    \animate {whom = roboh, opacity=0...1, freeze at end, begin on={click, of=go, delay=20s}, duration=2s}

    \animate {whom = c3, shift=(heli) ... (h),  interpolation=spline,key spline control={0.5}{0}{0.5}{1}, freeze at end, begin on={click, of=go, delay=22s}, duration=2s}
    \animate {whom = focus, opacity = 1...0, freeze at end, begin on={click, of=go, delay=22s}, duration=2s}
    
    \draw [name=focus, red] (0,0) circle [radius=5mm];

    \node (rob) {\includegraphics[height=9mm]{media/plain.png}};
    \node (roboh) {\includegraphics[height=9mm]{media/surprise-pd-tango.png}};
    \node (c1) at ([yshift=1mm]0,0) {\includegraphics[height=9mm]{media/red-person.png}};
    \node (c2) at ([yshift=1mm]0,0) {\includegraphics[height=9mm]{media/blue-person.png}};
    \node (c3) at ([yshift=1mm]0,0) {\includegraphics[height=9mm]{media/gray-person.png}};

    }
  

\end{frame}

%% \begin{frame}{Robbers and Coppers:}{Two Cops Do Not Catch the Robber.}

%%   \only<1>{\gamegraph{d}{f}{}{}{plain}{}}
%%   \only<2>{\gamegraph{d}{f}{}{i}{plain}{}}
%%   \only<3>{\gamegraph{heli}{f}{}{i}{plain}{j}}
%%   \only<4>{\gamegraph{heli}{f}{}{k}{plain}{j}}
%%   \only<5>{\gamegraph{j}{f}{}{k}{plain}{}}
%%   \only<6>{\gamegraph{j}{heli}{}{k}{plain}{k}}
%%   \only<7>{\gamegraph{j}{heli}{}{e}{plain}{k}}
%%   \only<8>{\gamegraph{j}{k}{}{e}{plain}{}}
%%   \only<9>{\gamegraph{heli}{k}{}{e}{plain}{e}}
%%   \only<10>{\gamegraph{heli}{k}{}{d}{smile}{e}}
%%   \only<11>{\gamegraph{e}{k}{}{d}{smile}{}}
%% \end{frame}

%% \begin{frame}{Robbers and Coppers:}{Three Cops Always Catch the Robber.}

%%   \only<1>{\gamegraph{d}{f}{a}{}{plain}{}}
%%   \only<2>{\gamegraph{d}{f}{a}{g}{plain}{}}
%%   \only<3>{\gamegraph{heli}{f}{a}{g}{plain}{g}}
%%   \only<4>{\gamegraph{heli}{f}{a}{h}{plain}{g}}
%%   \only<5>{\gamegraph{g}{f}{a}{h}{plain}{}}
%%   \only<6>{\gamegraph{g}{f}{heli}{h}{surprise-pd-tango}{h}}
%%   \only<7>{\gamegraph{g}{f}{h}{h}{surprise-pd-tango}{}}
%% \end{frame}


\begin{frame}{The Cops's Strategy = Tree Decomposition}

  The \alert{winning strategy of the cops} forms a \alert{tree}:
  \begin{itemize}
  \item The \alert{nodes} are positions of the cops.
  \item The \alert{root} is their initial position.
  \item The \alert{children} of a tree node are the \alert{graph
      components that could contain the robber}.
  \end{itemize}
  
\end{frame}

\def\makemytinygraph#1#2#3#4#5{%
  \tikz [graph,scale=.2] {
    \path  (2.5,1.25) rectangle (6.75,7.5);
    \graph [no placement, edge=#1, nodes={circle,inner
      sep=0pt,minimum size=2pt,fill=#1,draw=#1,as=}] {
      b [x=3.7,y=7.2,#2],
      a [x=4,y=6],
      c [x=2.8,y=6.2],
      d [x=3.7,y=5],
      e [x=5.5,y=4.5,#4],
      f [x=4,y=3],
      g [x=3,y=2.5],
      h [x=3,y=1.5,#3],
      l [x=3,y=3.5,#3],
      i [x=4.5,y=2,#4],
      j [x=5,y=3],
      k [x=6.5,y=3,#4,#5],
      a--b,
      l -- g -- h,
      i -- j,
      j -- {k,e},
      e --[#4] k,
      { [edges=black!40]
        a -- d -- f -- {l,h,g,j},
        b--c,
      c -- a,
      }
    };
  }
}
\newbox\mytinygraph\setbox\mytinygraph=\hbox{\makemytinygraph{black}{}{}{}{}}
\newbox\mytinygrapha\setbox\mytinygrapha=\hbox{\makemytinygraph{black!40}{black}{}{}{}}
\newbox\mytinygraphb\setbox\mytinygraphb=\hbox{\makemytinygraph{black!40}{}{}{black}{}}
\newbox\mytinygraphba\setbox\mytinygraphba=\hbox{\makemytinygraph{black!40}{}{}{}{black}}
\newbox\mytinygraphc\setbox\mytinygraphc=\hbox{\makemytinygraph{black!40}{}{black}{}{}}

\newbox\mytinygraphx\setbox\mytinygraphx=\hbox{\makemytinygraph{black!40}{}{}{}{}}

\def\gametinygraph#1#2#3#4{
  \tikz {
    {\pgftransformshift{\pgfqpoint{1.43cm}{1.5cm}}\pgftext[right,top]{\copy#4}}
    \begin{scope}[scale=.2]
      \ifx#1//\else\scoped[shift=(#1.center),yshift=-3pt] \fill[red] (90:18pt) --
        (210:18pt) -- (-30:18pt) -- cycle;\fi
      \ifx#2//\else\scoped[shift=(#2.center)] \fill[red] (0,0) circle [radius=14pt];\fi
      \ifx#3//\else\scoped[shift=(#3.center)] \fill[red] (-12pt,-12pt)
      rectangle (12pt,12pt);\fi
    \end{scope}
  }
}

\begin{frame}{Example of a Tree Decomposition of Width 2.}
  
  \tikz [graph] \graph [tree layout, level sep=5mm, sibling sep=5mm,
  nodes={circle,fill=black!15,inner sep=0pt}] {
    /[as=\gametinygraph{c}{d}{f}{\mytinygraph}] -> {
      /[as=\gametinygraph{c}{d}{a}{\mytinygrapha}] -> /[as=\gametinygraph{c}{b}{a}{\mytinygraphx}],
      /[as=\gametinygraph{g}{d}{f}{\mytinygraphc}] -> {
        /[as=\gametinygraph{g}{l}{f}{\mytinygraphx}],
        /[as=\gametinygraph{g}{h}{f}{\mytinygraphx}]},
      /[as=\gametinygraph{j}{d}{f}{\mytinygraphb}] -> {
        /[as=\gametinygraph{j}{i}{f}{\mytinygraphx}],
        /[as=\gametinygraph{j}{e}{f}{\mytinygraphba}] -> /[as=\gametinygraph{j}{e}{k}{\mytinygraphx}]
      }
    }    
  };
  
\end{frame}

\begin{frame}{Divide and Conquer, Second Attempt}

  \begin{theorem}
    For a graph $G$ let a tree decomposition of width $k$ with $n$
    nodes be given. Then we can decide in time
    \begin{align*}
      O(3^{k+1} n)
    \end{align*}
    whether $G$ is 3-colorable.
  \end{theorem}

  \uncover<2>{
  \begin{theorem}
    For a graph $G$ let a tree decomposition of width $k$ with $n$
    nodes be given. Then we can compute in time
    \begin{align*}
      O(2^{k+1} n)
    \end{align*}
    the largest independent set of $G$.
  \end{theorem}
  }
\end{frame}




\begin{frame}{Why We Need \alert{Meta}\,theorems.}

%  * Eine Idee, auf viele Probleme (Auszug aus dem Paper zeigen) anwendbar.

  \tikz{
    \node [above, inner sep=0pt] {
      \includegraphics[width=9cm,clip=true,viewport=25mm 45mm 235mm 75mm]{bodlaender/7/img/1.png}};
    \node [below, inner sep=0pt] {
      \includegraphics[width=9cm,clip=true,viewport=19.5mm 70mm 228.5mm 193mm]{bodlaender/8/img/1.png}};
  }

\end{frame}


\subsection{Classic Variants \dots}
\frame{\frametitle{Outline}\tableofcontents[currentsubsection]}


\begin{frame}{All Problems Share one Property.}

  In 1990, Courcelle noted that all of the problems can be described
  in \alert{monadic second order logic} (MSO logic).
  
\end{frame}




\def\quesex#1{{\hbox to .75ex{\footnotesize\alt<#1>{?}{}\hfil}}}

\begin{frame}{A Logical Formula Specifying 3-Colorability.}
  
%  $\varphi_{\operatorname{3-colorable}} ={}$
  \tikzset{R/.style=node,G/.style=node,B/.style=node}
  \only<2->{\tikzset{R/.style={node=red}}}
  \only<3->{\tikzset{G/.style={node=green!50!black}}}
  \only<4->{\tikzset{B/.style={node=blue}}}
  \begin{align*}
    \smash{\tikz [graph,baseline=-.5cm-.5ex] {\graph [nodes=node,empty nodes] {
      {a[R],b[G]} -- {c[B],d[R]} -- {e[R],f[B]};
      a--b, c--d, e--f;
      b--c;
    }; \only<5->{\node [orange,anchor=mid]at (b) {$x$}; \node [orange,anchor=mid]at (c) {$y$};}}} \models^{\quesex{-4}}\smash{{\alt<6>{\color{black}}{\color{white}}
  \underbrace{{\color{black}\textcolor<2->{red}{\exists R}\,
    \textcolor<3->{green!50!black}{\exists G}\,
    \textcolor<4->{blue}{\exists B}\;
    \textcolor<5->{orange}{\forall x\forall y}}}_{\text{Pattern } E_1E_1E_1 aa}}} &\bigl( E(x,y) \to \\
     &\quad((R(x) \land \neg G(x) \land \neg B(x)) \lor {} \\
     &\quad\phantom{(}(\neg R(x) \land G(x) \land \neg B(x)) \lor {} \\
     &\quad\phantom{(}(\neg R(x) \land \neg G(x) \land B(x))) \land {} \\
    &\quad\neg(R(x) \land R(y)) \land{}\\
    &\quad\neg(G(x) \land G(y)) \land{}\\
    &\quad\neg(B(x) \land B(y))\bigr)
  \end{align*}
\end{frame}




% \begin{frame}<7->{Die Beschreibung von Grapheigenschaften mittels Logik.}
  
%   \only<1-6>{
%     Sei $\varphi_{\operatorname{4-clique}}$ folgende
%     \alert{erststufige} Formel:
%     \begin{align*}
%       \textcolor<2->{orange}{\exists a}
%       \textcolor<3->{blue}{\exists b}
%       \textcolor<4->{green!50!black}{\exists c}
%       \textcolor<5->{violet}{\exists d}
%       \bigl( \textcolor<6->{red}{E(a,b) \land E(a,c)
%         \land E(a,d) \land E(b,c) \land E(b,d) \land E(c,d)} \bigr)
%     \end{align*}
%     Ein Graph ist ein Modell dieser Formel gdw.\ er eine 4-Clique enthält:
    
%     \tikzset{a/.style=node,b/.style=node,c/.style=node,d/.style=node,hi/.style=}
%     \only<2->{\tikzset{a/.style={node=orange}}}
%     \only<3->{\tikzset{b/.style={node=blue}}}
%     \only<4->{\tikzset{c/.style={node=green!50!black}}}
%     \only<5->{\tikzset{d/.style={node=violet}}}
%     \only<6->{\tikzset{hi/.style={red,very thick}}}
    
%     \begin{align*}
%       \tikz [graph,baseline=-.5cm] \graph [empty nodes] {
%         {a [a], b [b]} --[hi] {c [c] ,d [d]} -- {e[node],f[node]};
%         a--[hi]b, c--[hi]d, e--f;
%         a --[hi] d, c--[hi] b;
%       }; &\models \varphi_{\operatorname{4-clique}} \\ \\
%       \tikz [graph,baseline=-.5cm] \graph [nodes=node,empty nodes] {
%         {a,b} -- {c,d};
%         a--b, c--d; b--c;
%       }; &\not\models \varphi_{\operatorname{4-clique}}
%     \end{align*}
% }
% \only<7->{
%      Eine typische \alert{monadische zweitstufige} Formel ist $\varphi_{\operatorname{3-colorable}} ={}$
%      \begin{align*}
%       \textcolor<8->{red}{\exists R}\,
%       \textcolor<9->{green!50!black}{\exists G}\,
%       \textcolor<10->{blue}{\exists B}\;
%       &\forall x (R(x) \lor G(x) \lor B(x)) \land \\
%       &\forall x\forall y \bigl( E(x,y) \to \\
%       &\quad\neg(R(x) \land R(y)) \land
%       \neg(G(x) \land G(y)) \land
%       \neg(B(x) \land B(y))\bigr)
%      \end{align*}
%      Sie »beschreibt« 3-Färbbarkeit:
%      \tikzset{R/.style=node,G/.style=node,B/.style=node}
%      \only<8->{\tikzset{R/.style={node=red}}}
%      \only<10->{\tikzset{B/.style={node=blue}}}
%      \only<9->{\tikzset{G/.style={node=green!50!black}}}
%      \begin{align*}
%        \tikz [graph,baseline=-.5cm] \graph [nodes=node,empty nodes] {
%          {a[R],b[G]} -- {c[B],d[R]} -- {e[R],f[B]};
%          a--b, c--d, e--f;
%          b--c;
%        }; &\models \varphi_{\operatorname{3-colorable}} \\ \\
%        \tikz [graph,baseline=-.5cm] \graph [empty nodes,nodes=node] {
%          {a, b} -- {c, d} -- {e,f};
%          a--b, c--d, e--f;
%          a -- d, c-- b;
%        }; &\not\models \varphi_{\operatorname{3-colorable}}
%      \end{align*}
%  }

% \end{frame}

{\setbox0=\hbox{\makemytinygraph{}{}{}{}{}}}

\begin{frame}{Classical Algorithmic Metatheorems.}
  
  \begin{theorem}[Courcelle]
    Let $\varphi$ be an MSO formula and $k$ a number. Then
    \begin{align*}
      \{ G \mid G \models \varphi \text{ and $G$ has tree width at
        most 
        $k$}\}
    \end{align*}
    can be decided in \alert{linear time}.
  \end{theorem}
\end{frame}


\begin{frame}<2->[t]{Proof Sketch}
  
  \only<2>{\strut
  Step 1: The original question.
  
  \tikz [graph] {
    \graph [no placement, edge=structure.fg, nodes={node,as=}] {
      a' [x=4,y=6],
      b' [x=3.7,y=7.2],
      c' [x=2.8,y=6.2],
      d' [x=3.7,y=5],
      e' [x=5.5,y=4.5],
      f' [x=4,y=3],
      g' [x=3,y=2.5],
      h' [x=3,y=1.5],
      i' [x=4.5,y=2],
      j' [x=5,y=3],
      k' [x=6.5,y=3],
      l' [x=3,y=3.5],
      {b',c'} -- a' -- d' -- f' -- {l',h',g',j' -- {e',k'}},
      b'--c',
      l' -- g' -- h',
      i' -- j',
      e' -- k',
    };

    \node [right] at (7,5) {$\models
      \varphi_{\operatorname{3-colorable}}$ ?};
  }
}
\only<3>{\strut
  Step 2: Compute a tree decomposition in linear time.
  
  
  \tikz [graph] \graph [tree layout, level sep=2.5mm, sibling sep=5mm,
  nodes={circle,fill=black!15,inner sep=0pt}] {
    /[as=\gametinygraph{c}{d}{f}{\mytinygraph}] -> {
      /[as=\gametinygraph{c}{d}{a}{\mytinygrapha}] -> /[as=\gametinygraph{c}{b}{a}{\mytinygraphx}],
      /[as=\gametinygraph{g}{d}{f}{\mytinygraphc}] -> {
        /[as=\gametinygraph{g}{l}{f}{\mytinygraphx}],
        /[as=\gametinygraph{g}{h}{f}{\mytinygraphx}]},
      /[as=\gametinygraph{j}{d}{f}{\mytinygraphb}] -> {
        /[as=\gametinygraph{j}{i}{f}{\mytinygraphx}],
        /[as=\gametinygraph{j}{e}{f}{\mytinygraphba}] -> /[as=\gametinygraph{j}{e}{k}{\mytinygraphx}]
      }
    }    
  };
}
\only<4>{\strut
  Step 3: Adjust the formula so that it applies to the tree.
  
  
  \tikz [graph]{
    \graph [tree layout, level sep=2.5mm, sibling sep=5mm,
  nodes={circle,fill=black!15,inner sep=0pt}] {
    /[as=\gametinygraph{c}{d}{f}{\mytinygraph}] -> {
      /[as=\gametinygraph{c}{d}{a}{\mytinygrapha}] -> /[as=\gametinygraph{c}{b}{a}{\mytinygraphx}],
      /[as=\gametinygraph{g}{d}{f}{\mytinygraphc}] -> {
        /[as=\gametinygraph{g}{l}{f}{\mytinygraphx}],
        /[as=\gametinygraph{g}{h}{f}{\mytinygraphx}]},
      /[as=\gametinygraph{j}{d}{f}{\mytinygraphb}] -> {
        /[as=\gametinygraph{j}{i}{f}{\mytinygraphx}],
        /[as=\gametinygraph{j}{e}{f}{\mytinygraphba}] -> /[as=\gametinygraph{j}{e}{k}{\mytinygraphx}]
      }
    }
  };
   \node [right] at (2,0) {$\models \varphi'_{\operatorname{3-colorable}}$ ?};
 }
}
\only<5>{\strut
  Step 4: Transform the formula into a tree automaton.
  
  \tikz [graph]{
    \graph [tree layout, level sep=2.5mm, sibling sep=5mm,
  nodes={circle,fill=black!15,inner sep=0pt}] {
    /[as=\gametinygraph{c}{d}{f}{\mytinygraph}] -> {
      /[as=\gametinygraph{c}{d}{a}{\mytinygrapha}] -> /[as=\gametinygraph{c}{b}{a}{\mytinygraphx}],
      /[as=\gametinygraph{g}{d}{f}{\mytinygraphc}] -> {
        /[as=\gametinygraph{g}{l}{f}{\mytinygraphx}],
        /[as=\gametinygraph{g}{h}{f}{\mytinygraphx}]},
      /[as=\gametinygraph{j}{d}{f}{\mytinygraphb}] -> {
        /[as=\gametinygraph{j}{i}{f}{\mytinygraphx}],
        /[as=\gametinygraph{j}{e}{f}{\mytinygraphba}] -> /[as=\gametinygraph{j}{e}{k}{\mytinygraphx}]
      }
    }
  };
  \node [right] at (2,0) {$\in L(M_{\operatorname{3-colorable}})$?};
 }
}
\only<6>{\strut
  Step 5: Evaluate that automaton in linear time.
  
  \tikz [graph]{
    \graph [tree layout, level sep=2.5mm, sibling sep=5mm,
  nodes={circle,fill=black!15,inner sep=0pt}] {
    /[as=\gametinygraph{c}{d}{f}{\mytinygraph}] -> {
      /[as=\gametinygraph{c}{d}{a}{\mytinygrapha}] -> /[as=\gametinygraph{c}{b}{a}{\mytinygraphx},label=-90:$q_0$],
      /[as=\gametinygraph{g}{d}{f}{\mytinygraphc}] -> {
        /[as=\gametinygraph{g}{l}{f}{\mytinygraphx},label=-90:$q_0$],
        /[as=\gametinygraph{g}{h}{f}{\mytinygraphx},label=-90:$q_0$]},
      /[as=\gametinygraph{j}{d}{f}{\mytinygraphb}] -> {
        /[as=\gametinygraph{j}{i}{f}{\mytinygraphx},label=-90:$q_0$],
        /[as=\gametinygraph{j}{e}{f}{\mytinygraphba}] -> /[as=\gametinygraph{j}{e}{k}{\mytinygraphx},label=0:$q_0$]
      }
    }
  }; 
 }
}
\only<7>{\strut
  Step 5: Evaluate that automaton in linear time.
  
  \tikz [graph]{
    \graph [tree layout, level sep=2.5mm, sibling sep=5mm,
  nodes={circle,fill=black!15,inner sep=0pt}] {
    /[as=\gametinygraph{c}{d}{f}{\mytinygraph}] -> {
      /[as=\gametinygraph{c}{d}{a}{\mytinygrapha},label=0:$q_3$] -> /[as=\gametinygraph{c}{b}{a}{\mytinygraphx},label=-90:$q_0$],
      /[as=\gametinygraph{g}{d}{f}{\mytinygraphc},label=0:$q_2$] -> {
        /[as=\gametinygraph{g}{l}{f}{\mytinygraphx},label=-90:$q_0$],
        /[as=\gametinygraph{g}{h}{f}{\mytinygraphx},label=-90:$q_0$]},
      /[as=\gametinygraph{j}{d}{f}{\mytinygraphb}] -> {
        /[as=\gametinygraph{j}{i}{f}{\mytinygraphx},label=-90:$q_0$],
        /[as=\gametinygraph{j}{e}{f}{\mytinygraphba},label=0:$q_5$] -> /[as=\gametinygraph{j}{e}{k}{\mytinygraphx},label=0:$q_0$]
      }
    }
  };
 }
}
\only<8>{
  \strut  Step 5: Evaluate that automaton in linear time.
  
  \tikz [graph]{
    \graph [tree layout, level sep=2.5mm, sibling sep=5mm,
  nodes={circle,fill=black!15,inner sep=0pt}] {
    /[as=\gametinygraph{c}{d}{f}{\mytinygraph},label=0:$q_5 \in Q_{\operatorname{accepting}}$?] -> {
      /[as=\gametinygraph{c}{d}{a}{\mytinygrapha},label=0:$q_3$] -> /[as=\gametinygraph{c}{b}{a}{\mytinygraphx},label=-90:$q_0$],
      /[as=\gametinygraph{g}{d}{f}{\mytinygraphc},label=0:$q_2$] -> {
        /[as=\gametinygraph{g}{l}{f}{\mytinygraphx},label=-90:$q_0$],
        /[as=\gametinygraph{g}{h}{f}{\mytinygraphx},label=-90:$q_0$]},
      /[as=\gametinygraph{j}{d}{f}{\mytinygraphb},label=0:$q_8$] -> {
        /[as=\gametinygraph{j}{i}{f}{\mytinygraphx},label=-90:$q_0$],
        /[as=\gametinygraph{j}{e}{f}{\mytinygraphba},label=0:$q_5$] -> /[as=\gametinygraph{j}{e}{k}{\mytinygraphx},label=0:$q_0$]
      }
    }
  };
 }
}


\end{frame}



\begin{frame}{Classical Algorithmic Metatheorems.}

  \begin{theorem}[\strut The General Pattern]
    If
    \begin{itemize}
    \item the problem can be described in a  \alert{certain logic}
    \item and the input can be \alert{decomposed in a certain way},
    \end{itemize}
    then
    \begin{itemize}
    \item there is a \alert{certain kind} of algorithm for it.
    \end{itemize}
  \end{theorem}
\end{frame}

\begin{frame}<2->{Classical Algorithmic Metatheorems.}
  \only<2>{
    \begin{theorem}[\strut Courcelle]
      If
      \begin{itemize}
      \item the problem can be described in \alert{MSO logic}
      \item and the input has \alert{tree width at most $k$},
      \end{itemize}
      then
      \begin{itemize}
      \item there is a \alert{linear time} of algorithm for it.
      \end{itemize}
    \end{theorem}
  }
  
  \only<3>{
    \begin{theorem}[\strut Bodlaender, Courcelle]
      If
      \begin{itemize}
      \item the problem can be described in \alert{MSO logic}
      \item and the input has \alert{tree width at most $k$},
      \end{itemize}
      then
      \begin{itemize}
      \item there is a \alert{parallel algorithm} running in time
        $O(\log n)$.
      \end{itemize}
    \end{theorem}
  }
  
  \only<4>{
    \begin{theorem}[\strut Courcelle, Makowsky, Rotics]
      If
      \begin{itemize}
      \item the problem can be described in MSO logic
      \item and the input has \alert{clique} width at most $k$,
      \end{itemize}
      then
      \begin{itemize}
      \item there is a \alert{polynomial time} algorithm for it.
      \end{itemize}
    \end{theorem}
  }
  
  \only<5>{
    \begin{theorem}[\strut Frick, Grohe]
      If
      \begin{itemize}
      \item the problem can be described in \alert{FO} logic
      \item and the input is \alert{planar},
      \end{itemize}
      then
      \begin{itemize}
      \item there is a \alert{linear time} algorithm for it.
      \end{itemize}
    \end{theorem}
  }
  
  \only<6>{
    \begin{theorem}[\strut Flum, Grohe]
      If
      \begin{itemize}
      \item the problem can be described in \alert{FO} logic
      \item and the input has a \alert{forbidden minor},
      \end{itemize}
      then
      \begin{itemize}
      \item there is a \alert{polynomial time} algorithm for it.
      \end{itemize}
    \end{theorem}
  }
  
\end{frame}



\subsection{\dots and New Variants}
\frame{\frametitle{Outline}\tableofcontents[currentsubsection]}

\begin{frame}{Beyond Time}
  
  \begin{itemize}
  \item While the classical theorems yield \alert{tight upper time} bounds\dots
  \item \dots they yield \alert{no} completeness results.
  \item The new metatheorems concern 
    \begin{itemize}
    \item \alert{space complexity} and
    \item \alert{circuit complexity}
    \end{itemize}
  \item and yield \alert{completeness results}.
  \end{itemize}

\end{frame}


% \begin{frame}{Überblick über die Klassen, um die es im Folgenden geht.}

%   \begin{tikzpicture}[graph,yscale=1.2]
%     \coordinate (AC^0) at ( 0,2.0);    
%     \coordinate (TC^0) at ( 0,2.5);    
%     \coordinate (REG)   at ( 0,1.5);    
%     \coordinate (NC^1) at ( 0,3.0);    
%     \coordinate (L) at ( 0,3.5);    
%     \coordinate (NL) at ( 0,4.0);    
%     \coordinate (NC) at ( 0,4.5);    
%     \coordinate (P) at ( 0,5);    

%     \begin{scope}[draw=structure.fg,thick]
%       \foreach \class/\x/\col in
%       {P/5/5,NC/4.5/8,NL/4.0/11,L/3.5/14,NC^1/3.0/17,TC^0/2.0/20,AC^0/1.5/23}
%       {
%         \draw[fill=structure.fg!\col] (-\x,0) parabola bend (\class) (\x,0);
%         \node[below] at (\class) {$\Class{\class}$};
%       }
      
%       \foreach \class/\x/\col in {REG/2.5/20}
%       {
%         \draw (-\x,0) parabola bend (\class) (\x,0);
%         \node[below] at (\class) {$\Class{\class}$};
%       }

%       \draw (-5.5,0) -- (5.5,0);
%     \end{scope}
    
%     \begin{scope}[green!40!black,*-,nodes={fill=white,rounded corners,fill opacity=0.8,text opacity=1,align=left,right}]
      
%       \draw([xshift=3mm,yshift=-3mm]P) -- ++(2.2,0)
%       node {
%         $\Lang{cvp}$
%       };
      
%       \draw([xshift=3mm,yshift=-3mm]NL) -- ++(2.2,0)
%       node {
%         $\Lang{reach}$\\[-1mm]
%         $\Lang{distance}$
%       };
      
%       \draw([xshift=3mm,yshift=-3mm]L) -- ++(2.2,-0.3)
%       node {
%         $\Lang{ureach}$
%       };
      
%       \draw([xshift=-4mm,yshift=-3mm]NC^1) -- ++(-2,.3)
%       node [left,align=right] {
%         \small$\Lang{boolean-formula}$
%       };
      
%       \draw([xshift=-3mm,yshift=-4mm]TC^0) -- ++(-2,0)
%       node [left,align=right] {
%         \small$\Lang{majority}$
%       };
      
%       \draw([xshift=-3mm,yshift=-4mm]AC^0) -- ++(-2,-.3)
%       node [left,align=right] {
%         \small$\Lang{4-clique}$
%       };
      
%     \end{scope}
%   \end{tikzpicture}
  
% \end{frame}



\section{New Variants 1: Space Complexity}

\frame{\frametitle{Outline}\tableofcontents[currentsection]}



\begin{frame}{A Logspace Turing Machine}

  \begin{tikzpicture}[graph, decoration=zigzag]
    \begin{scope}[yshift=4cm] % Input tape
      \fill[structure.fg!30!bg]
        (0,0) decorate { -- ++(0,0.5) }  -- ++(4.5,0)
              decorate { -- ++(0,-0.5) } -- cycle;

      \node      at (0,0.5) [above right] {Input tape (read only), $n$ symbols};
      \node (it) at (0,0.25) [right]      {\ttfamily3401234*3143223};
    \end{scope}
   
    \begin{scope}[yshift=2cm,xshift=4cm] % Work tape
      \fill[structure.fg!30!bg]
        (0,0) decorate { -- ++(0,0.5) } -- ++(1.5,0)
              decorate { -- ++(0,-0.5) } -- cycle;

      \node      at (0,0.5)  [above right] {Work tape, $O(\log n)$ symbols};
      \node (wt) at (0,0.25) [right]      {\ttfamily42};
    \end{scope}
   
%     \begin{scope}[yshift=-5mm] % Output tape
%       \fill[structure.fg!30!bg]
%         (0,0) decorate { -- ++(0,0.5) } -- ++(4.5,0)
%               decorate { -- ++(0,-0.5) } -- cycle;

%       \node      at (0,0)   [below right] {Ausgabeband (nur schreiben)};
%       \node (ot) at (0,0.25) [right]      {\ttfamily10690836937182};
%     \end{scope}

    \node (g4) at (1.75,2) [node,rectangle,minimum size=1cm]  {$M$};

    \draw[->] (g4.north) .. controls +(up:1cm) and +(down:1cm) .. (it.south west);
%    \draw[->] (g4.south) .. controls +(down:1cm) and +(up:1cm) .. (ot.north east);
    \draw[->] (g4.east)  .. controls +(right:1cm) and +(down:1cm) .. (wt.south);
  \end{tikzpicture}  
  
\end{frame}



{\setbox0=\hbox{\makemytinygraph{}{}{}{}{}}}

\subsection{New Theorems}

\begin{frame}{The Logspace Version of Courcelle's Theorem.}
    
  \begin{theorem}[Elberfeld, T, Jakoby, 2010]
    Let $\varphi$ be an MSO formula and $k$ a number. Then
    \begin{align*}
      \{ G \mid G \models \varphi \text{ and $G$ has tree width at
        most 
        $k$}\}
    \end{align*}
    can be decided in \alert{logspace}.
  \end{theorem}

%  \begin{proof}[Beweisideen]
%    \begin{enumerate}
%    \item<alert@1> Berechne eine Baumzerlegung $T$ von $G$ in
%      logarithmischem Platz.
%    \item Übersetze $G \models^? \varphi$ in $T \models^? \varphi'$.
%    \item Übersetze $T \models^? \varphi'$ in $T \in^? L(M)$.
%    \item<alert@1> Werte $M$ auf $T$ in logarithmischem Platz aus.\qedhere
%    \end{enumerate}
%  \end{proof}
\end{frame}

% \begin{frame}<2-6,9>{Beweis der Logspace-Version des Satzes von Courcelle.}
  
% \only<2>{\strut
%   Beweisschritt 1: Die Ausgangsfrage.
  
%   \tikz [graph] {
%     \graph [no placement, edge=structure.fg, nodes={node,as=}] {
%       a' [x=4,y=6],
%       b' [x=3.7,y=7.2],
%       c' [x=2.8,y=6.2],
%       d' [x=3.7,y=5],
%       e' [x=5.5,y=4.5],
%       f' [x=4,y=3],
%       g' [x=3,y=2.5],
%       h' [x=3,y=1.5],
%       i' [x=4.5,y=2],
%       j' [x=5,y=3],
%       k' [x=6.5,y=3],
%       l' [x=3,y=3.5],
%       {b',c'} -- a' -- d' -- f' -- {l',h',g',j' -- {e',k'}},
%       b'--c',
%       l' -- g' -- h',
%       i' -- j',
%       e' -- k',
%     };

%     \node [right] at (7,5) {$\models
%       \varphi_{\operatorname{3-colorable}}$ ?};
%   }
% }
% \only<3-4>{\strut
%   Beweisschritt 2: Berechnung einer Baumzerlegung in\\
%   logarithmischem Platz.

%   \bigskip
  
%   \tikz [graph] \graph [grow down=1.25cm,branch right=1.25cm,
%   nodes={circle,fill=black!15,minimum size=8mm,as=,inner sep=0pt}] {
%     {subgraph I_n [n=7, name=A]} -!-
%     {subgraph I_n [n=7, name=B]} -!-
%     {subgraph I_n [n=7, name=C]} -!-
%     {subgraph I_n [n=7, name=D]} -!-    
%     {subgraph I_n [n=7, name=E]},
%     { [edges={only=<4>{red}}]
%       A 1 -> {B 1, B 2 -> {C 1 -> {D 1, D 2} -> {E 1, E 2}, C 2, C 4 ->
%           {D 3, D 4,D 5} -> {E 3, E 4, E 5}}},
%     },
%     A 2 -> B 2,
%     A 3 -> B 3 -> C 3,
%     A 4 -> C 3,
%     A 5 -> { B 3, B 4 ->  C 4 , B 5 -> C 5, B 6 -> C 6 -> D 6 -> { E 6, E 7 }},
%     A 6 -> { B 5, B 6 },
%     A 7 -> B 7 -> C 7 -> D 7 -> { E 6, E 7 },    
%   };
% }
% \only<5>{\strut
%   Beweisschritt 3: Übertragung der Formel auf den Baum:
    
%   \tikz [graph]{
%     \graph [tree layout, level sep=2.5mm, sibling sep=5mm,
%   nodes={circle,fill=black!15,inner sep=0pt}] {
%     /[as=\gametinygraph{c}{d}{f}{\mytinygraph}] -> {
%       /[as=\gametinygraph{c}{d}{a}{\mytinygrapha}] -> /[as=\gametinygraph{c}{b}{a}{\mytinygraphx}],
%       /[as=\gametinygraph{g}{d}{f}{\mytinygraphc}] -> {
%         /[as=\gametinygraph{g}{l}{f}{\mytinygraphx}],
%         /[as=\gametinygraph{g}{h}{f}{\mytinygraphx}]},
%       /[as=\gametinygraph{j}{d}{f}{\mytinygraphb}] -> {
%         /[as=\gametinygraph{j}{i}{f}{\mytinygraphx}],
%         /[as=\gametinygraph{j}{e}{f}{\mytinygraphba}] -> /[as=\gametinygraph{j}{e}{k}{\mytinygraphx}]
%       }
%     }
%   };
%    \node [right] at (2,0) {$\models \varphi'_{\operatorname{3-colorable}}$ ?};
%  }
% }
% \only<6>{\strut
%   Beweisschritt 4: Umwandlung der Formel in einen Baumautomaten:
  
%   \tikz [graph]{
%     \graph [tree layout, level sep=2.5mm, sibling sep=5mm,
%   nodes={circle,fill=black!15,inner sep=0pt}] {
%     /[as=\gametinygraph{c}{d}{f}{\mytinygraph}] -> {
%       /[as=\gametinygraph{c}{d}{a}{\mytinygrapha}] -> /[as=\gametinygraph{c}{b}{a}{\mytinygraphx}],
%       /[as=\gametinygraph{g}{d}{f}{\mytinygraphc}] -> {
%         /[as=\gametinygraph{g}{l}{f}{\mytinygraphx}],
%         /[as=\gametinygraph{g}{h}{f}{\mytinygraphx}]},
%       /[as=\gametinygraph{j}{d}{f}{\mytinygraphb}] -> {
%         /[as=\gametinygraph{j}{i}{f}{\mytinygraphx}],
%         /[as=\gametinygraph{j}{e}{f}{\mytinygraphba}] -> /[as=\gametinygraph{j}{e}{k}{\mytinygraphx}]
%       }
%     }
%   };
%    \node [right] at (2,0) {$\in L(M_{\operatorname{3-colorable}})$?};
%  }
% }
% \only<7>{\strut
%   Beweisschritt 5: Auswertung des Automaten in logarithmischem Platz.
  
%   \tikz [graph]{
%     \graph [tree layout, level sep=2.5mm, sibling sep=5mm,
%   nodes={circle,fill=black!15,inner sep=0pt}] {
%     /[as=\gametinygraph{c}{d}{f}{\mytinygraph}] -> {
%       /[as=\gametinygraph{c}{d}{a}{\mytinygrapha}] -> /[as=\gametinygraph{c}{b}{a}{\mytinygraphx}],
%       /[as=\gametinygraph{g}{d}{f}{\mytinygraphc}] -> {
%         /[as=\gametinygraph{g}{l}{f}{\mytinygraphx}],
%         /[as=\gametinygraph{g}{h}{f}{\mytinygraphx}]},
%       /[as=\gametinygraph{j}{d}{f}{\mytinygraphb}] -> {
%         /[as=\gametinygraph{j}{i}{f}{\mytinygraphx}],
%         /[as=\gametinygraph{j}{e}{f}{\mytinygraphba}] -> /[as=\gametinygraph{j}{e}{k}{\mytinygraphx}]
%       }
%     }
%   };
%  }
% }
% \only<8>{\strut
%   Beweisschritt 5: Auswertung des Automaten in logarithmischem Platz.
  
%   \tikz [graph]{
%     \graph [tree layout, level sep=2.5mm, sibling sep=5mm,
%   nodes={circle,fill=black!15,inner sep=0pt}] {
%     /[as=\gametinygraph{c}{d}{f}{\mytinygraph}] -> {
%       /[as=\gametinygraph{c}{d}{a}{\mytinygrapha}] -> /[as=\gametinygraph{c}{b}{a}{\mytinygraphx},label=-90:$q_0$],
%       /[as=\gametinygraph{g}{d}{f}{\mytinygraphc},label=0:$q_2$] -> {
%         /[as=\gametinygraph{g}{l}{f}{\mytinygraphx}],
%         /[as=\gametinygraph{g}{h}{f}{\mytinygraphx}]},
%       /[as=\gametinygraph{j}{d}{f}{\mytinygraphb},label=0:$q_8$] -> {
%         /[as=\gametinygraph{j}{i}{f}{\mytinygraphx}],
%         /[as=\gametinygraph{j}{e}{f}{\mytinygraphba}] -> /[as=\gametinygraph{j}{e}{k}{\mytinygraphx}]
%       }
%     }
%   };
%  }
% }
% \only<9>{\strut
%   Beweisschritt 5: Auswertung des Automaten in logarithmischem Platz.
  
%   \tikz [graph]{
%     \graph [tree layout, level sep=2.5mm, sibling sep=5mm,
%   nodes={circle,fill=black!15,inner sep=0pt}] {
%     /[as=\gametinygraph{c}{d}{f}{\mytinygraph},label=0:$q_5 \in Q_{\operatorname{accepting}}$?] -> {
%       /[as=\gametinygraph{c}{d}{a}{\mytinygrapha}] -> /[as=\gametinygraph{c}{b}{a}{\mytinygraphx}],
%       /[as=\gametinygraph{g}{d}{f}{\mytinygraphc}] -> {
%         /[as=\gametinygraph{g}{l}{f}{\mytinygraphx}],
%         /[as=\gametinygraph{g}{h}{f}{\mytinygraphx}]},
%       /[as=\gametinygraph{j}{d}{f}{\mytinygraphb}] -> {
%         /[as=\gametinygraph{j}{i}{f}{\mytinygraphx}],
%         /[as=\gametinygraph{j}{e}{f}{\mytinygraphba}] -> /[as=\gametinygraph{j}{e}{k}{\mytinygraphx}]
%       }
%     }
%   };
%  }
% }


% \end{frame}


\begin{frame}{The Low-Hanging Fruits.}
  
  \begin{columns}
    \column{.55\textwidth}
    \begin{corollary}
      For all $k$, we can solve in \alert{logspace}:
      \begin{itemize}
      \item $\{ G \mid G$ is \alert{3-colorable}\\
        and $G$ has tree width at most $k\}$.
      \item $\{ G \mid G$ has a \alert{perfect matching}\\
        and $G$ has tree width at most $k\}$.
      \item $\{ (G,s,t) \mid t$ is \alert{reachable} from $s$\\
        and $G$ has tree width at most $k\}$.
      \item \dots
      \end{itemize}
    \end{corollary}
    
    \bigskip
    (Each result used to be a paper.)
  
    \column{.5\textwidth}
    \tikz
    {
      \node [inner sep=0pt,outer sep=0pt] { \includegraphics[width=\textwidth]{media/Lucas_Cranach.jpg}};
      \draw [overlay,ultra thick,white,->] (-1,0.5) -- (.2,0.5);
    }
  \end{columns}
  
\end{frame}



\subsection{Applications: Cycle Lengths in Graphs}

\frame{\frametitle{Outline}\tableofcontents[currentsubsection]}


\begin{frame}{The High-Hanging Fruits.}
  
  \begin{columns}
    \column{.55\textwidth}
    Metatheorems make statements\\
    about \alert{decomposable} graphs.

    \bigskip
    For \alert{arbitrary} graph, this may work:
  \begin{itemize}
  \item If the graph \alert{is} decomposable, \\
    apply the metatheorem.
  \item If the graph \alert{is not} decomposable,\\
    it must have \alert{many edges},\\
    which we may \alert{use algorithmically}.
  \end{itemize}
    \column{.5\textwidth}
    \tikz
    {
      \node [inner sep=0pt,outer sep=0pt] { \includegraphics[width=\textwidth]{media/Lucas_Cranach.jpg}};
      \draw [overlay,ultra thick,white,->] (-1.2,3.2) -- (0,3.2);
    }
  \end{columns}
\end{frame}


% \begin{frame}{The Even Cycle Problem}
  
%   \begin{columns}[t,onlytextwidth]
%     \column{.49\textwidth}
%     \begin{example}
%       \tikz [graph] {
%         \graph [spring electrical layout, nodes={node, as=}] {
%           a -- b -- c -- c'-- d -- e --e'--e''-- f -- a;
%           d -- f''[nudge=(down:5mm)] -- f -- b;
%           a -- e
%         };
%         \node [right] at (-1,-2.5) {$\in \Lang{even-cycle}$};
%       }
%     \end{example}
%     \column{.49\textwidth}
%     \begin{example}
%       \tikz [graph] {
%         \graph [spring electrical layout, nodes={node, as=}, horizontal=b to e] {
%           a -- b -- c -- a;
%           a -- d -- e -- a;
%         };
%         \node [right] at (-1,-1) {$\notin \Lang{even-cycle}$};
%       }
%     \end{example}
    
%   \end{columns}
  
% \end{frame}


\begin{frame}{The Formula $\varphi_3$ Describes the \\Existence of Cycles Whose Length is a Multiple of 3.}
  
  \tikzset{R/.style=node,G/.style=node,B/.style=node}
  \only<2->{\tikzset{R/.style={node=red}}}
  \only<3->{\tikzset{G/.style={node=green!50!black}}}
  \only<4->{\tikzset{B/.style={node=blue}}}
  \begin{align*}
    \smash{\alt<-4>{\tikz [graph,baseline=-.5cm-.5ex] \graph [nodes=node,empty nodes] {
      {a[R],b[B],x[R]} -- {c[G],d[G]} -- {e[B],f[R]};
      a--b, c--d, e--f;
      b--c, x -- {b, d};
    };}{\tikz [graph,baseline=-.5cm-.5ex] \graph [nodes=node,empty nodes] {
      {a[R],b[B],x[R]} -- {c[G],d[G]} -- {e[B],f[R]};
      a--b, c--d, e--f;
      b--c, x -- {b, d};
      {[edges={orange,bend left,overlay}]a->c -> e -> f -> d -> b -> a; x->b}
    };}
}
  \models^{\quesex{-4}}\smash{{\alt<6>{\color{black}}{\color{white}}
  \underbrace{{\color{black}\textcolor<2->{red}{\exists R}\,
    \textcolor<3->{green!50!black}{\exists G}\,
    \textcolor<4->{blue}{\exists B}\;
    \textcolor<5->{orange}{\forall x\exists y}}}_{\text{Pattern } E_1E_1E_1 ae}}} &\bigl( E(x,y) \land \\
     &\quad((R(x) \land \neg G(x) \land \neg B(x)) \lor {} \\
     &\quad\phantom{(}(\neg R(x) \land G(x) \land \neg B(x)) \lor {} \\
     &\quad\phantom{(}(\neg R(x) \land \neg G(x) \land B(x))) \land {} \\
    &\quad(R(x) \to G(y)) \land{}\\
    &\quad(G(x) \to B(y)) \land{}\\
    &\quad(B(x) \to R(y))\bigr)
  \end{align*}
\end{frame}



\begin{frame}{Detecting Cycles Whose Length is a Multiple of $3$.}
  
  \begin{theorem}
    There is a logspace algorithm that on input of an undirected graph $G$
    decides whether $G$ has a cycle whose length is a multiple of $3$.
  \end{theorem}

  \begin{proof}
    \begin{enumerate}
    \item Check, whether $G$ has small tree width.
    \item If yes, subdivide all edges and apply the metatheorem to $\varphi_4$. 
    \item \alert{If no, output ``yes''.}\\[.5em]
      Thomassen has shown that all graphs of sufficiently large tree
      width have a cycle whose length is a multiple of $3$.\qedhere
    \end{enumerate}
  \end{proof}

  (A similar argument shows $\Lang{even-cycle} \in \Class L$.)
\end{frame}




\subsection{Applications: Quantifier Prefix Classes}
\frame{\frametitle{Outline}\tableofcontents[currentsubsection]}


\begin{frame}{Formulas in Existential Second-Order Logic Describe NP.}

  \begin{theorem}[Fagin, 1974]
    A problem is in \alert{$\Class{NP}$} if, and only if,\\ it can be described by
    a formula in \alert{existential second-order logic.} 
  \end{theorem}
  
  \uncover<2>{
    \bigskip
    \begin{itemize}
    \item However, $E_1E_1E_1 aa$ suffices to describe NP-complete problems.
    \item What about $E_1E_1E_1 ae$?
    \item What about $E_1E_1 aa$?
    \item What about $E_1 aa$?
    \item \dots
    \end{itemize}

    \bigskip
    \alert{Can we refine Fagin's Theorem?}
  }
\end{frame}




\begin{frame}[t]{A Very Hard-To-Prove Upper Bound}

  \begin{theorem}[Gottlob, Kolaitis, Schwentick, 2004]
    $E_1^* ae$ formulas describe problems \alert{in $\Class P$} over undirected loop-free graphs.
  \end{theorem}
\only<2-6>{
  \begin{proof}
    \only<2>{
    \smallskip
    \begin{tikzpicture}
      \foreach \i in {50,...,40} {
        \node[overlay,draw,fill=yellow!25] at (\i*0.75,-\i*.02)
        {\includegraphics[width=1.7cm,trim=4.5cm 3.5cm 4.5cm 2.5cm]{media/GottlobKS2004/\i.svg}};
      }
      \foreach \i in {39,...,28} {
        \node[draw,fill=yellow!25,xshift=11.75*0.75cm,yshift=1cm] at (\i*0.75,-\i*.02)
        {\includegraphics[width=1.7cm,trim=4.5cm 3.5cm 4.5cm 2.5cm]{media/GottlobKS2004/\i.svg}};
      }
      \foreach \i in {27,...,16} {
        \node[draw,fill=yellow!25,xshift=23.5*0.75cm,yshift=2cm] at (\i*0.75,-\i*.02)
        {\includegraphics[width=1.7cm,trim=4.5cm 3.5cm 4.5cm 2.5cm]{media/GottlobKS2004/\i.svg}};
      }
    \end{tikzpicture}}
  \only<3-4>{

    \alt<3>{Original question:}{New question:}
    \medskip
    
    \hbox{}\qquad
    \tikz [baseline=-1cm-.5ex,graph]
      \graph [nodes=node,empty nodes] {
        {a,b,x} -- {c,d} -- {e,f};
        a--b, c--d, e--f;
        b--c, x -- {b, d};
      };
      \only<3>{
        $\models^? \exists R \exists G \exists B \forall x \exists y\, (\varphi)$
      }
      \only<4->{
        \tikz [baseline,graph] {
          \draw [->] decorate[decoration={snake,amplitude=.25ex,post length=1em}] { (0,0) -- node[above] {Is there a
              special} node [below] {homomorphism?} (4,0) };
          
          \begin{scope}[xshift=5cm]
            \graph [nodes=node,empty nodes, no placement] {
              a[at={(90:8mm)}] -> [edge label=$\oplus$] b[at={(-30:8mm)}] -> [edge
              label=$\oplus$] c [at={(210:8mm)}] -> [edge label=$\oplus$] a;
            };
          \end{scope}
        }
      }
    }
    \only<5->{
      \begin{enumerate}
      \item Preprocess the input graph.
      \item Check whether the \alert{tree width is small}.
      \item If so, we get a polynomial time algorithm by \alert{Courcelle's Theorem}.
      \item If not, depending on the target graph,  
        \begin{enumerate}
        \item we can either \alert{just say ``yes''} or
        \item test whether a special cycle of \alert{constant length} exists.
        \end{enumerate}
      \end{enumerate}
      \vskip-1em
    }
  \end{proof}
  \only<6>{
    \begin{block}{Key Insight}
      All steps can also be done in \alert{logspace}, in
      particular also \alert{applying Courcelle's Theorem} because of
      its logspace version.
    \end{block}
  }}
\only<7>{
      
    \begin{theorem}[T., 2015]
      $E_1^* ae$ formulas describe problems \alert{in $\Class L$} over undirected loop-free graphs.
    \end{theorem}

    \begin{corollary}
      $\Lang{even-cycle} \in \Class L$.
    \end{corollary}
  }
\end{frame}



\begin{frame}{All Pattern Classes Over Undirected Self-Loop Free Graphs}  
  
  \begin{theorem}
    The patterns below yield the classes over undirected self-loop
    free graphs:
    \medskip
    
    \begin{tikzpicture}[graph]
      \fill [structure.fg!10] (-0.75,0) rectangle (9.6,1);
      \fill [structure.fg!20] (-0.75,1) rectangle (9.6,2.75);
      \fill [structure.fg!30] (-0.75,2.75) rectangle (9.6,4.5);
      \fill [structure.fg!40] (-0.75,4.5) rectangle (9.6,6.25);

      \draw [structure.fg]
      (-0.75,0) -- ++ (11,0)
      (-0.75,1) -- ++ (11,0)
      (-0.75,2.75) -- ++ (11,0)
      (-0.75,4.5) -- ++ (11,0)
      (-0.75,6.25) -- ++ (11,0)
      ;
      
      \graph [no placement] {
        ae/$(ae)^*$ [x=2, y=0.5];
        Eea/$E_{\text{\itshape any}}^*e^*a$ [x=5, y=0.5];
        E1aa/$E_1aa$ [x=2, y=1.5];
        Eaa/$E_{\text{\itshape any}}aa$ [x=1, y=2.25];
        E1esaa/$E_1e^*aa$ [x=3,y=4];
        E1eaa/$E_1eaa$ [x=3,y=3.25];
        E1ae/$E_1ae$ [x=7, y=.5];
        E1E1ae/$E_1E_1ae$ [x=6, y=1.5];
        E2ae/$E_2ae$ [x=8, y=1.5];
        Eae/$E_{\text{\itshape any}}^*ae$ [x=7, y=2.25];
        Eaeae/$E_{\text{\itshape any}}^*(ae)^*$ [x=3, y=5.75];
        
        E1E1aa/$E_1E_1aa$ [x=0,y=5];
        E1aaa/$E_1aaa$ [x=1.5,y=5];
        E2eaa/$E_2eaa$ [x=3,y=5];
        E1eae/$E_1eae$ [x=4.5,y=5];
        E1aee/$E_1aee$ [x=6,y=5];
        E1aea/$E_1aea$ [x=7.5,y=5];
        E1aae/$E_1aae$ [x=9,y=5];
        
        AC0/$\Class{AC}^0$ [x=10,y=0.5];
        L/$\Class{L}$ [x=10,y=1.875];
        NL/$\Class{NL}$ [x=10,y=3.625];
        NP/$\Class{NP}$ [x=10,y=5.375];
      };
    \end{tikzpicture}
  \end{theorem}
    
\end{frame}



\subsection{Applications: Integer Optimization}
\frame{\frametitle{Outline}\tableofcontents[currentsubsection]}

{\setbox0=\hbox{\makemytinygraph{}{}{}{}{}}}


\begin{frame}[t]{The Subset Sum Problem}
  
  \only<1-2>{
  \begin{tikzpicture}
    \node [above right]
    {\includegraphics[height=5cm]{media/Blackboard-2.jpg}};

    \node [above right, text width=3cm, text=white] at (1,1) {
      98237534\\ 3245\\ 1095345\\ 13435\\ 39087539\\ 759\\ 98798754910
    };
    \node [above right, text width=3cm, text=white] at (4,1) {
      246301534\\ 2336245\\ 6245\\ 202934435\\ 10237\\ 59\\ 91111074234
    };
  \end{tikzpicture}  

  \begin{block}{The Subset Sum Problem}
    Circle some numbers so that they add up  exactly to 1000000000.
  \end{block}

  \uncover<2>{This is a well-known $\Class{NP}$-complete problem.}
}

  \only<3->{
    \begin{tikzpicture}
      \node [above right]
      {\includegraphics[height=5cm]{media/Blackboard-2.jpg}};
      
      \node [above right, text width=5.5cm, text=white] at (1,0.6) {
        \num{3}{2}\\[1mm] \num{2}{1}\\[1mm] \num{4}{0}\\[1mm] \num{5}{4}\\[1mm]
        \num{1}{1}\\[1mm] \num{0}{4}\\[1mm] \num {5}{1}
      };
    \end{tikzpicture}  
    
    \begin{block}{The Unary Subset Sum Problem}
      Cirlce some numbers so that they add up exactly to $\num{11}{0}$.
    \end{block}
  }

\end{frame}


\begin{frame}{The Unary Version Is In Logspace.}

  \begin{theorem}
    $\Lang{unary-subset-sum} \in\Class{L}$.
  \end{theorem}
  
  \begin{proof}
    For an input like \snum{1}{2},\ \ \textcolor<2->{red}{\snum{0}{3}},\ \
    \snum{2}{0},\ \ \textcolor<2->{red}{\snum{1}{0}}
    consider the forest
    \medskip
      
    \begin{tikzpicture}[graph]
      \foreach \i/\a/\opt in {1/6/,2/2/node=red,3/9/,4/4/node=red}
      {
        \begin{scope}[xshift=\i*2.5cm]
          \node [node,only/.expanded=<2->\opt] (x) at (0,0) {};
          \foreach \j in {1,...,\a}
          \node [node,only/.expanded=<2->\opt] at (360*\j/\a:7mm) {} edge (x);
        \end{scope}
      }
    \end{tikzpicture}
    \medskip
    
    \begin{enumerate}
    \item<2->
      The size of a set \textcolor<2->{red}{$S$} that is
      closed under reachability corresponds to a 
      \textcolor<2->{red}{subset sum}.
    \item<2->
      The formula $\varphi_{\operatorname{closed}}(X) = \forall u \forall v 
      \bigl[( X(u) \land E(u,v)) \to X(v) \bigr]$ describes ``being
      closed under reachability.''
    \item<2->
      New goal: Find out whether $\varphi$ has a solution of a \alert{certain size}.
      \qedhere
    \end{enumerate}
  \end{proof}
\end{frame}


\begin{frame}<1>{A Stronger Algorithmic Metatheorem}
    
  \only<1>{
    
  \begin{theorem}[Elberfeld, T, Jakoby, 2010]
    Let $\varphi(X)$ be an MSO formula with a free variable and let
    $k$ be a number.\\
    Then there is \alert{logspace Turing machine} that on input of
    \begin{enumerate}
    \item a graph $G$ of tree width at most $k$ and
    \item a number $s$ 
    \end{enumerate}
    computes the \alert{number of subsets $S$} with
    \begin{enumerate}
    \item $|S| = s$ and
    \item $G \models \varphi(S)$.
    \end{enumerate}
  \end{theorem}

}
% \only<2>{\strut
%   Beweisschritt 1: Die Ausgangsfrage.
  
%   \tikz [graph] {
%     \graph [no placement, edge=structure.fg, nodes={node,as=}] {
%       a' [x=4,y=6],
%       b' [x=3.7,y=7.2],
%       c' [x=2.8,y=6.2],
%       d' [x=3.7,y=5],
%       e' [x=5.5,y=4.5],
%       f' [x=4,y=3],
%       g' [x=3,y=2.5],
%       h' [x=3,y=1.5],
%       i' [x=4.5,y=2],
%       j' [x=5,y=3],
%       k' [x=6.5,y=3],
%       l' [x=3,y=3.5],
%       {b',c'} -- a' -- d' -- f' -- {l',h',g',j' -- {e',k'}},
%       b'--c',
%       l' -- g' -- h',
%       i' -- j',
%       e' -- k',
%     };

%     \node [right, text width=5cm] at (7,5) {hat wie viele unabhängige Mengen der Größe $5$?};
%   }
% }
% \only<3>{\strut
%   Beweisschritt 2: Berechnung einer Baumzerlegung in
%   logarithmischem Platz.

%   \bigskip
  
%   \tikz [graph] \graph [grow down=1.25cm,branch right=1.25cm,
%   nodes={circle,fill=black!15,minimum size=8mm,as=,inner sep=0pt}] {
%     {subgraph I_n [n=7, name=A]} -!-
%     {subgraph I_n [n=7, name=B]} -!-
%     {subgraph I_n [n=7, name=C]} -!-
%     {subgraph I_n [n=7, name=D]} -!-    
%     {subgraph I_n [n=7, name=E]},
%     { [edges={red}]
%       A 1 -> {B 1, B 2 -> {C 1 -> {D 1, D 2} -> {E 1, E 2}, C 2, C 4 ->
%           {D 3, D 4,D 5} -> {E 3, E 4, E 5}}},
%     },
%     A 2 -> B 2,
%     A 3 -> B 3 -> C 3,
%     A 4 -> C 3,
%     A 5 -> { B 3, B 4 ->  C 4 , B 5 -> C 5, B 6 -> C 6 -> D 6 -> { E 6, E 7 }},
%     A 6 -> { B 5, B 6 },
%     A 7 -> B 7 -> C 7 -> D 7 -> { E 6, E 7 },    
%   };
% }
% \only<4>{\strut
%   Beweisschritt 3: Übertragung der Formel auf den Baum:
    
%   \tikz [graph]{
%     \graph [tree layout, level sep=2.5mm, sibling sep=5mm,
%   nodes={circle,fill=black!15,inner sep=0pt}] {
%     /[as=\gametinygraph{c}{d}{f}{\mytinygraph}] -> {
%       /[as=\gametinygraph{c}{d}{a}{\mytinygrapha}] -> /[as=\gametinygraph{c}{b}{a}{\mytinygraphx}],
%       /[as=\gametinygraph{g}{d}{f}{\mytinygraphc}] -> {
%         /[as=\gametinygraph{g}{l}{f}{\mytinygraphx}],
%         /[as=\gametinygraph{g}{h}{f}{\mytinygraphx}]},
%       /[as=\gametinygraph{j}{d}{f}{\mytinygraphb}] -> {
%         /[as=\gametinygraph{j}{i}{f}{\mytinygraphx}],
%         /[as=\gametinygraph{j}{e}{f}{\mytinygraphba}] -> /[as=\gametinygraph{j}{e}{k}{\mytinygraphx}]
%       }
%     }
%   };
%    \node [below right] at (-4.5,-5) {$\models \varphi'(S)$ für wie viele $S$ mit
%      $|S|=5$?};
%  }
% }
% \only<5>{\strut
%   Beweisschritt 4: Umwandlung der Formel in einen Baumautomaten:
  
%   \tikz [graph]{
%     \graph [tree layout, level sep=2.5mm, sibling sep=5mm,
%   nodes={circle,fill=black!15,inner sep=0pt}] {
%     /[as=\gametinygraph{c}{d}{f}{\mytinygraph}] -> {
%       /[as=\gametinygraph{c}{d}{a}{\mytinygrapha}] -> /[as=\gametinygraph{c}{b}{a}{\mytinygraphx}],
%       /[as=\gametinygraph{g}{d}{f}{\mytinygraphc}] -> {
%         /[as=\gametinygraph{g}{l}{f}{\mytinygraphx}],
%         /[as=\gametinygraph{g}{h}{f}{\mytinygraphx}]},
%       /[as=\gametinygraph{j}{d}{f}{\mytinygraphb}] -> {
%         /[as=\gametinygraph{j}{i}{f}{\mytinygraphx}],
%         /[as=\gametinygraph{j}{e}{f}{\mytinygraphba}] -> /[as=\gametinygraph{j}{e}{k}{\mytinygraphx}]
%       }
%     }
%   };
%    \node [below right,align=left] at (-4.5,-5) {hat wie viele Färbungen mit $5$ gefärbten
%      Knoten,\\ so dass $M$ akzeptiert?};
%  }
% }
% \only<6>{\strut
%   Beweisschritt 5: Umwandlung des Automaten in einen Faltungsterm:
  
%   \tikz [graph]{
%     \graph [tree layout, level sep=2.5mm, sibling sep=3mm, fresh nodes,  nodes=] {
%       "$*$" -> { "$+$" -> {"$*$" -> {"[0,0,1,0]","[1,0,0,0]"},
%           "[0,1,1,2]"},
%         "$+$" ->  {"$*$"-> {"$+$" -> {"[0,3,1,0]","[1,1,0,0]"},"[0,2,0,2]"}, "$*$"-> {"[0,0,1,1]","[1,0,0,1]"}} }
%     };
%   }
% }
% \only<7>{\strut
%   Beweisschritt 6: Umwandlung des Faltungsterms in einen arithmetischen Baum:
  
%   \tikz [graph]{
%     \graph [tree layout, level sep=2.5mm, sibling sep=3mm, fresh nodes,  nodes=] {
%       "$\times$" -> { "$+$" -> {"$\times$" -> {"10","1000"},
%           "0112"},
%         "$+$" ->  {"$\times$"-> {"$+$" -> {"310","1100"},"202"}, "$\times$"-> {"11","1001"}} }
%     };
%   }
% }

\end{frame}




\begin{frame}[t]{What We Are Really Interested In:\\ The
    \alert{Original} Subset Sum Problem.}
  
  Let $a_1$, \dots, $a_n$ be the inputs and $s$ the target sum.
  
  \begin{theorem}
    \alert{Dynamic programming} solves the subset sum problem in 
    \begin{itemize}
    \item time $O(ns)$ and
    \item space $O(s)$.
    \end{itemize}
  \end{theorem}
  
  \medskip
  
  \only<1>{
    \begin{columns}[onlytextwidth]
      \column{.6\textwidth}
      For larger $s$, \alert{space} is the bottleneck:
      4GB of memory are filled in \alert{one second} for $s =
      1{,}000{,}000{,}000$. 
      \column{.35\textwidth}
      \includegraphicscopyright[width=\linewidth]{media/ram-ccsa-Utente-Sassospicco.jpg}
      {Unknown author, Creative Commons Attribution Sharealike License}
    \end{columns}
  }
  

%%   \only<2>{
%%   \begin{theorem}[Lokshtanov, Nederlof, 2010]
%%     The subset sum problem can be solved in
%%     \begin{itemize}
%%     \item time $n^{O(1)} s^{O(1)}$ and
%%     \item space $n^{O(1)}$.
%%     \end{itemize}
%%   \end{theorem}
%%   \begin{proof}
%%     Complex analysis of approximation circuits for Fourier
%%     transformations.
%%   \end{proof}
%% }

\end{frame}



\begin{frame}{A Magic Trick.}
  
  \only<1>{
  \begin{tikzpicture}[graph, decoration=zigzag]
    \begin{scope}[yshift=7.5cm] % Input tape
      \fill[structure.fg!30!bg]
        (0,0) decorate { -- ++(0,0.5) }  -- ++(2.5,0)
              decorate { -- ++(0,-0.5) } -- cycle;

      \node      at (0,0.5) [above right] {Real input};
      \node (rt) at (0,0.25) [right]      {\ttfamily2;9;5;20};
    \end{scope}
    
    \begin{scope}[yshift=4cm,opacity=.5] % Input tape
      \fill[structure.fg!30!bg]
        (0,0) decorate { -- ++(0,0.5) }  -- ++(9.5,0)
              decorate { -- ++(0,-0.5) } -- cycle;

      \node      at (0,0.5) [above right] {Virtual input (read only)};
      \node (it) at (0,0.25) [right]      {\ttfamily11;111111111;11111;11111111111111111111};
    \end{scope}
   
    \begin{scope}[yshift=2cm,xshift=6cm] % Work tape
      \fill[structure.fg!30!bg]
        (0,0) decorate { -- ++(0,0.5) } -- ++(1.5,0)
              decorate { -- ++(0,-0.5) } -- cycle;

      \node      at (0,0.5)  [above right] {Work tape};
      \node (wt) at (0,0.25) [right]      {\ttfamily42};
    \end{scope}
   
    \node (g4) at (1.75,2) [node,rectangle,minimum size=1cm, opacity=.5]
    {Virtual logspace machine $M$};
    \node (g5) at (6.5,6) [node,rectangle,minimum size=1cm]  {Real machine};

    \draw[->] (g4.north) .. controls +(up:1cm) and +(down:1cm) .. (it.south west);
    \draw[->] (g4.east)  .. controls +(right:1cm) and +(down:1cm) .. (wt.south);
    \draw[->] (g5) to[out=90,in=-90] (rt.-30);
    \draw[->] (g5) to[out=-90,in=90] (wt.north west);
  \end{tikzpicture}  
}

\only<2>{
  A similar argument shows that there are \alert{space efficient}
  pseudo-polynomial time algorithms for:
  \begin{itemize}
  \item knapsack problems,
  \item bin packing problems,
  \item scheduling problems, and
  \item integer programming for a fixed number of inequalities.
  \end{itemize}
}  
\end{frame}


\section{New Variants 2: Circuit Complexity}

\frame{\frametitle{Outline}\tableofcontents[currentsection]}

\subsection{New Theorems}

\begin{frame}[t]{The Class NC$^1$}
  
  \hfill \tikz[overlay]{
    \node [rotate=-5] {\includegraphics[height=3cm]{media/Wanted.jpg}};
    \node [rotate=-5,scale=1.5,yshift=1mm,minimum height=8mm,minimum width=1cm,fill=white,text=red] {$\Class{NC^1}$}
  }\kern1cm\\[-1em]
  \tikz [graph] {
    \graph [tree layout, grow'=up, nodes=node, level distance=0pt, level sep=3pt, sibling distance=1.5cm] {
      "$y_1$"[nudge=(down:1mm)] <- "$\land$"[pin={[pin
        distance=.25em,red]85:fan in 2}] <- {
        2[as=$\land$] <- {3[as=$\lor$,x=0,y=-1.5], 4[as=$\lor$]},
        5[as=$\land$] <- {
          6[as=$\lor$]<- {7[as=$\lor$], 8[as=$\land$]},
          9[as=$\lor$] <- {10[as=$\land$], 11[as=$\lor$]}
        }
      }
    };
    \graph [nodes=node, branch right=1.1cm] {
      x1[as=$x_1$],
      x2[as=$x_2$],
      x3[as=$x_3$],
      x4[as=$x_4$],
      x5[as=$x_5$],
      x6[as=$x_6$],
      x7[as=$x_7$],
      x8[as=$x_8$],
      x1 -> {(3), (7)},
      x2 -> {(3), (8)},
      x3 -> {(4)},
      (7) -> (4),
      x4 -> (7),
      x5 -> (8),
      x6 -> (10),
      x7 -> {(10), (11)},
      x8 -> (11)
    };

    \draw [red, decoration={brace,raise=5pt},decorate] (x1.north)
    -- node [above=10pt] {$n$ input gates} (x8.north);
    
    \draw [red, decoration={brace,raise=5pt},decorate] (x8.east)
    -- node [right=10pt] {$\log n$ layers} ++(0,-3);
  }
  
  \begin{itemize}
  \item $\Class{REG} \subseteq \Class{NC}^1 \subseteq \Class L$.
  \item Addition, multiplication, and division all lie in $\Class{NC}^1$.
  \item Tree decompositions cannot be computed in $\Class{NC}^1$
    unless $\Class{NC}^1 = \Class L$. 
  \end{itemize}
  
\end{frame}
  

  
{\setbox0=\hbox{\makemytinygraph{}{}{}{}{}}}

\begin{frame}{The NC$^1$ Version of Courcelle's Theorem.}
    
  \begin{theorem}[Elberfeld, T, Jakoby, 2012]
    Let $\varphi$ be an MSO formula and $k$ a number. Then there is an
    \alert{$\Class{NC}^1$ circuit family} that on input of
    \begin{enumerate}
    \item a graph $G$ 
    \item \alert{together with a tree decomposition of $G$ of width $k$}
    \end{enumerate}
    decides whether $G \models \varphi$.
  \end{theorem}

  \bigskip
  (As for logspace, there is also a ``counting version''.)
  
%  \bigskip
%  Weiterhin gilt auch die entsprechende »Zählversion« dieses Satzes.
  
%  \begin{proof}[Beweisideen]
%    \begin{enumerate}
%    \item<alert@1> Berechne eine Baumzerlegung $T$ von $G$ in
%      logarithmischem Platz.
%    \item Übersetze $G \models^? \varphi$ in $T \models^? \varphi'$.
%    \item Übersetze $T \models^? \varphi'$ in $T \in^? L(M)$.
%    \item<alert@1> Werte $M$ auf $T$ in logarithmischem Platz aus.\qedhere
%    \end{enumerate}
%  \end{proof}

% \only<2>{\strut
%   Beweisschritt 1: Die Ausgangsfrage.
  
%   \tikz [graph] {
%     \graph [no placement, edge=structure.fg, nodes={node,as=}] {
%       a' [x=4,y=6],
%       b' [x=3.7,y=7.2],
%       c' [x=2.8,y=6.2],
%       d' [x=3.7,y=5],
%       e' [x=5.5,y=4.5],
%       f' [x=4,y=3],
%       g' [x=3,y=2.5],
%       h' [x=3,y=1.5],
%       i' [x=4.5,y=2],
%       j' [x=5,y=3],
%       k' [x=6.5,y=3],
%       l' [x=3,y=3.5],
%       {b',c'} -- a' -- d' -- f' -- {l',h',g',j' -- {e',k'}},
%       b'--c',
%       l' -- g' -- h',
%       i' -- j',
%       e' -- k',
%     };

%     \node [right] at (7,5) {$\models
%       \varphi_{\operatorname{3-colorable}}$ ?};
%   }
% }
% \only<3>{\strut
%   Beweisschritt 2: Die Baumzerlegung ist als Teil der Eingabe \alert{geschenkt}.
  
%   \tikz [graph]{
%     \graph [tree layout, level sep=2.5mm, sibling sep=5mm,
%   nodes={circle,fill=black!15,inner sep=0pt}] {
%     /[as=\gametinygraph{c}{d}{f}{\mytinygraph}] -> {
%       /[as=\gametinygraph{c}{d}{a}{\mytinygrapha}] -> /[as=\gametinygraph{c}{b}{a}{\mytinygraphx}],
%       /[as=\gametinygraph{g}{d}{f}{\mytinygraphc}] -> {
%         /[as=\gametinygraph{g}{l}{f}{\mytinygraphx}],
%         /[as=\gametinygraph{g}{h}{f}{\mytinygraphx}]},
%       /[as=\gametinygraph{j}{d}{f}{\mytinygraphb}] -> {
%         /[as=\gametinygraph{j}{i}{f}{\mytinygraphx}],
%         /[as=\gametinygraph{j}{e}{f}{\mytinygraphba}] -> /[as=\gametinygraph{j}{e}{k}{\mytinygraphx}]
%       }
%     }
%   };}
% }
% \only<4>{\strut
%   Beweisschritt 3: Übertragung der Formel auf den Baum:
    
%   \tikz [graph]{
%     \graph [tree layout, level sep=2.5mm, sibling sep=5mm,
%   nodes={circle,fill=black!15,inner sep=0pt}] {
%     /[as=\gametinygraph{c}{d}{f}{\mytinygraph}] -> {
%       /[as=\gametinygraph{c}{d}{a}{\mytinygrapha}] -> /[as=\gametinygraph{c}{b}{a}{\mytinygraphx}],
%       /[as=\gametinygraph{g}{d}{f}{\mytinygraphc}] -> {
%         /[as=\gametinygraph{g}{l}{f}{\mytinygraphx}],
%         /[as=\gametinygraph{g}{h}{f}{\mytinygraphx}]},
%       /[as=\gametinygraph{j}{d}{f}{\mytinygraphb}] -> {
%         /[as=\gametinygraph{j}{i}{f}{\mytinygraphx}],
%         /[as=\gametinygraph{j}{e}{f}{\mytinygraphba}] -> /[as=\gametinygraph{j}{e}{k}{\mytinygraphx}]
%       }
%     }
%   };
%    \node [right] at (2,0) {$\models \varphi'_{\operatorname{3-colorable}}$ ?};
%  }
% }
% \only<5>{\strut
%   Beweisschritt 4: Umwandlung der Formel in einen Baumautomaten:
  
%   \tikz [graph]{
%     \graph [tree layout, level sep=2.5mm, sibling sep=5mm,
%   nodes={circle,fill=black!15,inner sep=0pt}] {
%     /[as=\gametinygraph{c}{d}{f}{\mytinygraph}] -> {
%       /[as=\gametinygraph{c}{d}{a}{\mytinygrapha}] -> /[as=\gametinygraph{c}{b}{a}{\mytinygraphx}],
%       /[as=\gametinygraph{g}{d}{f}{\mytinygraphc}] -> {
%         /[as=\gametinygraph{g}{l}{f}{\mytinygraphx}],
%         /[as=\gametinygraph{g}{h}{f}{\mytinygraphx}]},
%       /[as=\gametinygraph{j}{d}{f}{\mytinygraphb}] -> {
%         /[as=\gametinygraph{j}{i}{f}{\mytinygraphx}],
%         /[as=\gametinygraph{j}{e}{f}{\mytinygraphba}] -> /[as=\gametinygraph{j}{e}{k}{\mytinygraphx}]
%       }
%     }
%   };
%    \node [right] at (2,0) {$\in L(M_{\operatorname{3-colorable}})$?};
%  }
% }
% \only<6>{\strut
%   Beweisschritt 5: Auswertung des Automaten in $\Class{NC}^1$.
  
%   \tikz [graph]{
%     \graph [tree layout, level sep=2.5mm, sibling sep=5mm,
%   nodes={circle,fill=black!15,inner sep=0pt}] {
%     /[as=\gametinygraph{c}{d}{f}{\mytinygraph},label=0:$q_5 \in Q_{\operatorname{accepting}}$?] -> {
%       /[as=\gametinygraph{c}{d}{a}{\mytinygrapha}] -> /[as=\gametinygraph{c}{b}{a}{\mytinygraphx}],
%       /[as=\gametinygraph{g}{d}{f}{\mytinygraphc}] -> {
%         /[as=\gametinygraph{g}{l}{f}{\mytinygraphx}],
%         /[as=\gametinygraph{g}{h}{f}{\mytinygraphx}]},
%       /[as=\gametinygraph{j}{d}{f}{\mytinygraphb}] -> {
%         /[as=\gametinygraph{j}{i}{f}{\mytinygraphx}],
%         /[as=\gametinygraph{j}{e}{f}{\mytinygraphba}] -> /[as=\gametinygraph{j}{e}{k}{\mytinygraphx}]
%       }
%     }
%   };
%  }
% }

\end{frame}

  

\subsection{Applications: Visible Pushdown Languages}
\frame{\frametitle{Outline}\tableofcontents[currentsubsection]}


\begin{frame}{\strut Visible Pushdown Languages}

  \begin{enumerate}
  \item The input is processed by a \alert{pushdown automaton}.
  \item Whether the automaton does a push or a pop may depend only
    on \alert{the read symbol} and \alert{not} on the state.
  \end{enumerate}

  \tikz [graph] {
    \begin{scope}[node]
      
      \begin{scope} % Input tape
        \fill[structure.fg!30!bg]
        (0.2,0) decorate { -- ++(0,0.5) }  -- ++(6.8,0)
        decorate { -- ++(0,-0.5) } -- cycle;
        
        \node [left] at (0,0.25) {Input tape};
        \foreach \symbol[count=\i] in {{(},[,1,+,1,],+,{(},2,+,[,2,+,2,],{)},{)}}
          \node at (\i*0.4,0.25) {\ttfamily\symbol};

        \node (go) [animate={begin on=click,duration=15s,shift={(0,0) ... (0.4*16,0)},freeze at end},
          circle,red,fill,opacity=.4,minimum size=5mm] at (0.4,0.25) {};
      \end{scope}

      \begin{scope}[yshift=-2cm]
        \node [left] at (0,0.4) {Stack};

        \foreach \stack[count=\i] in
        {{}{(},{{(},[},{{(},[},{{(},[},{{(},[},{{(}},{{(}},{{(},{(}},{{(},{(}},{{(},{(}},{{(},{(},[},{{(},{(},[},{{(},{(},[},{{(},{(},[},{{(},{(}},{{(}}} {
         \begin{scope}[animate={whom=s\i,opacity=0,freeze at end},
             animate={whom=s\i,begin on={click, of=go,delay=\i s-2s},opacity=0...1...0,freeze at end,duration=2s},
             animate={whom=s\i,begin on={click, of=go,delay=18s},opacity=0...1,freeze at end,duration=1s},
             animate={whom=x\i-1,begin on={click, of=go,delay=19s},shift={(0,0)...(\i*0.4-0.4,0)},freeze at end,duration=3s},
             animate={whom=x\i-2,begin on={click, of=go,delay=19s},shift={(0,0)...(\i*0.4-0.4,0)},freeze at end,duration=3s},
             animate={whom=x\i-3,begin on={click, of=go,delay=19s},shift={(0,0)...(\i*0.4-0.4,0)},freeze at end,duration=3s},
           ]
           \scoped [name=s\i] {
           \foreach \symbol[count=\j] in \stack {
             \node [rectangle,fill=structure.fg!30!bg,inner sep=0pt,minimum height=3.5mm, minimum width=3mm](x\i-\j)
             at (0.4,\j*0.4) {\symbol};
           }}
         \end{scope}
       }
      \end{scope}
    \end{scope}
  }
  
\end{frame}

%% \begin{frame}{\strut Visible Pushdown Languages}

%%   \begin{enumerate}
%%   \item The input is processed by a \alert{pushdown automaton}.
%%   \item Whether the automaton does a push or a pop may depend only
%%     on \alert{the read symbol} and \alert{not} on the state.
%%   \end{enumerate}

%%   \tikz [graph] {
%%     \begin{scope}[node]
      
%%       \begin{scope} % Input tape
%%         \fill[structure.fg!30!bg]
%%         (0.2,0) decorate { -- ++(0,0.5) }  -- ++(6.8,0)
%%         decorate { -- ++(0,-0.5) } -- cycle;
        
%%         \node [left] at (0,0.25) {Input tape};
%%         \foreach \symbol[count=\i] in {{(},[,1,+,1,],+,{(},2,+,[,2,+,2,],{)},{)}}
%%           \node [only=<\i>{red}] at (\i*0.4,0.25) {\ttfamily\symbol};
%%       \end{scope}

%%       \begin{scope}[yshift=-2cm]
%%         \node [left] at (0,0.4) {Stack};

%%         \foreach \stack[count=\i] in
%%         {{}{(},{{(},[},{{(},[},{{(},[},{{(},[},{{(}},{{(}},{{(},{(}},{{(},{(}},{{(},{(}},{{(},{(},[},{{(},{(},[},{{(},{(},[},{{(},{(},[},{{(},{(}},{{(}}} 
%%         \foreach \symbol[count=\j] in \stack
%%         {
%%           \only<\i->{
%%           \node [rectangle,fill=structure.fg!30!bg,inner
%%           sep=0pt,minimum height=3.5mm, minimum width=3mm]
%%           at (\i*0.4,\j*0.4) {\symbol};}
%%         }
%%       \end{scope}
%%     \end{scope}
%%   }
  
%% \end{frame}


\def\openbrace{(}
\def\closebrace{)}
\def\opensquare{[}
\def\closesquare{]}

\begin{frame}{\strut We Can Precompute the Stack Outline}

  \begin{enumerate}
  \item The input is processed by a \alert{pushdown automaton}.
  \item Whether the automaton does a push or a pop may depend only
    on \alert{the read symbol} and \alert{not} on the state.
  \end{enumerate}

  \tikz [graph] {
    \begin{scope}[node]
      
      \begin{scope} % Input tape
        \fill[structure.fg!30!bg]
        (0.2,0) decorate { -- ++(0,0.5) }  -- ++(6.8,0)
        decorate { -- ++(0,-0.5) } -- cycle;
        
        \node [left] at (0,0.25) {Input tape};
        \foreach \symbol[count=\i] in
        {{(},[,1,+,1,],+,{(},2,+,[,2,+,2,],{)},{)}}
        {
          \ifx\symbol\openbrace
          \node [green!50!black] at (\i*0.4,0.25) {$\uparrow$};
          \fi
          \ifx\symbol\opensquare
          \node [green!50!black] at (\i*0.4,0.25) {$\uparrow$};
          \fi
          \ifx\symbol\closebrace
          \node [red] at (\i*0.4,0.25) {$\downarrow$};
          \fi
          \ifx\symbol\closesquare
          \node [red] at (\i*0.4,0.25) {$\downarrow$};
          \fi
        }
      \end{scope}

      \begin{scope}[yshift=-2cm]
        \node [left] at (0,0.4) {Stack};

        \foreach \stack[count=\i] in
        {{}{(},{{(},[},{{(},[},{{(},[},{{(},[},{{(}},{{(}},{{(},{(}},{{(},{(}},{{(},{(}},{{(},{(},[},{{(},{(},[},{{(},{(},[},{{(},{(},[},{{(},{(}},{{(}}} 
        \foreach \symbol[count=\j] in \stack
        {
          \node [rectangle,fill=structure.fg!30!bg,inner
          sep=0pt,minimum height=3.5mm, minimum width=3mm]
          at (\i*0.4,\j*0.4) {};
        }
      \end{scope}
    \end{scope}
  }
  
\end{frame}


\begin{frame}{The Complexity of Visible Pushdown Languages}

  \begin{theorem}
    All visible pushdown languages lie in $\Class{NC}^1$.
  \end{theorem}

  \begin{proof}
    For an input like $([1+1]+(2+[2+2]))$ we can construct the
    following graph using ``simple counting'':
    \bigskip
    
    \tikz [graph, nodes={node,minimum size=2.5mm}] {
      \foreach \i in {1,...,16}
        \node (a\i) at (\i*0.5,0) {};
      \foreach \i in {2,...,5,7,8,...,15}
        \node (b\i) at (\i*0.5,0.5) {};
      \foreach \i in {11,...,14}
        \node (c\i) at (\i*0.5,1) {};
        
      \foreach \i[count=\j] in {2,...,16}
        \draw (a\j) edge[->] (a\i);
        
      \graph [use existing nodes] {
        a1 -> b2 -> b3 -> b4 -> b5 -> a6 -> b7 -> b8 -> b9 -> b10 ->
        b11 -> b12 -> b13 -> b14 -> b15 -> a16;

        b10 -> c11 -> c12 -> c13 -> c14 -> b15;        
      };
    }
    
    \bigskip
    \uncover<2>{
      Apply the metatheorem for $\Class{NC}^1$ to a formula stating
      \alert{``there exist states and symbols for the nodes that are
        locally consistent''}. 
    }    
  \end{proof}
  
\end{frame}




%\section{Zusammenfassung und Ausblick}

%\frame{\frametitle{Outline}\tableofcontents[currentsection]}



\begin{frame}{Summary}
  
  \alert{Algorithmic metatheorems} have the form
  \begin{quote}
    If a problem can be described in a \alert{certain logic} and the
    input graphs can be \alert{decomposed in a certain fashion}, then
    there is a \alert{certain kind of algorithm}.
  \end{quote}
    
  \begin{itemize}
  \item
    There are algorithmic metatheorems for logarithmic space.
  \item
    There are algorithmic metatheorems for $\Class{NC}^1$.
  \item
    Algorithmic metatheorems have applications\\ \alert{even when the
      inputs are not decomposable graphs}. 
  \end{itemize}
  
\end{frame}



\begin{frame}{Outlook}
  
  \begin{block}{Further Results}
    \begin{itemize}
    \item There are algorithmic metatheorems for constant depth circuits
      ($\Class{AC}^0$ and $\Class{TC}^0$). 
    \item There are algorithmic metatheorems for pure logic.
    \end{itemize}
  \end{block}

  \begin{block}{Some Open Problems}
    \begin{itemize}
    \item Is there an logspace metatheorem for bounded \alert{clique width}?
    \item Can we \alert{construct} solutions of a certain size?
    \item How difficult is detecting cycles whose \alert{length modulo~$3$ is~$1$}?
    \end{itemize}    
  \end{block}
  
\end{frame}


\end{document}

