\documentclass[12pt]{article}
\renewcommand{\baselinestretch}{1.5} % For Andrzej

\newcommand{\define}[1]{\textit{#1}}
\newcommand{\suchthat}[0]{\textrm{ such that }}
\newcommand{\code}[1]{\texttt{#1}}
\newcommand{\file}[1]{{\tt \bf #1}}

\usepackage{algorithmic}
\usepackage{algorithm}
\usepackage{verbatim}
\usepackage{url}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{graphicx}

\title{A General Algorithm for Performing Graph Reductions}

\author{P. Boothe\\
Computer Science Dept.\\
University of Oregon\\
{\tt peter@cs.uoregon.edu} \\
\url{http://soy.dyndns.org/~peter/projects/research/reduction/}}

\begin{document}
\maketitle

\section{Introduction}

Graph theory and the testing of graph properties have proven to be fertile
grounds for algorithms research, with applications to networks, digital design,
and even the analysis of social hierarchies.  Graphs with a particular property
are often essential to guarantee a correct design or efficient runtime.  Many
properties are very easy to test for -- graph connectivity can be tested with a
simple depth-first search -- but testing for other properties, such as the
existence of a Hamiltonian Path, has been shown to be NP-Hard or worse.

The ideal algorithm would take a description of the desired property in some
formal language and a graph.  Then it would quickly determine whether or not
the graph has the desired property.  Unfortunately, since many properties are
NP-Hard to test for, this algorithm probably does not exist.  All is not lost,
however, as we can consider restrictions to the formal language, and perhaps we
can find a language in which it is impossible to express an NP-Hard property.
One such language that almost meets that criteria is \define{monadic second
order logic} (MSOL), a restriction of second order logic to quantifiers over
functions of arity at most one.  In 1993 was shown by Arnborg et. al.
\cite{Reduction} that if we make the requirement that the property under test
has bounded treewidth, then there exists a testing algorithm that works in
linear time with respect to the size of the input graph.  Despite this
surprising bound on time, the language still retains quite a bit of expressive
power.  Many properties, including outerplanarity, planarity, 3-connectedness,
partial 3-tree, planar partial 3 tree, and planar partial 2 tree can all be
expressed in this framework.

The existence of this algorithm was proven by non-constructively showing that
for every bounded treewidth property described in MSOL there was a
corresponding \define{graph reduction system}, and then proving the existence
of a linear time algorithm for each system.  In this paper, we describe and
prove the correctness of an algorithm that works for all graph reduction
systems.  Before we move further, however, a general overview of what a graph
reduction system is and how they work is in order.

\section{Graph Reduction Systems}

A graph reduction system is a set of \define{reduction rules}, which are pairs
of labeled graphs, each vertex of which is tagged as \define{restricted} or
\define{unrestricted}, and a set of irreducible \define{reducts}.  Whenever