%mm6/8/99
\documentclass[12pt]{article}
%\usepackage{psfigfx}
\usepackage{psfig}
%\usepackage{graphicx}

%au queries
\newcommand{\query}[1]{\marginpar{\raggedright\scriptsize #1}}

%operators
\def\operator#1{\mathop{\rm#1}\nolimits}
\newcommand{\adj}{{\operator{adj}}}
\newcommand{\op}{{\operator{op}}}
\newcommand{\Quad}{{\operator{Quad}}}
\newcommand{\univ}[1]{{\cal L}(U_{\operator{#1}})}


\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{notation}{Notation}
\newtheorem{claim}{Claim}
\newtheorem{definition}{Definition}

%TeX code for black box FR:
\newcommand{\qed}{\hspace*{\fill} \vrule width.25cm height.25cm depth0cm}
\newenvironment{proof}
  {\begin{trivlist}\item[\hskip\labelsep{\bf Proof}\,]}
{\leavevmode\unskip\nobreak
\qed\end{trivlist}}
%proof variation
\newenvironment{proofsk}
  {\begin{trivlist}\item[\hskip\labelsep{\bf Proof (sketch)}\,]}
{\leavevmode\unskip\nobreak
\qed\end{trivlist}}


\newenvironment{case}[1]
  {\begin{trivlist}\item[\hskip\labelsep{\bf Case #1}\,]}{\end{trivlist}}
\newenvironment{subcase}[1]
  {\begin{trivlist}\item[\hskip\labelsep{\bf Subcase #1}\,]}{\end{trivlist}}
\newenvironment{stage}[1]
  {\begin{trivlist}\item[\hskip\labelsep{\bf Stage #1}]\,}{\end{trivlist}}
\newenvironment{problem}[1]
  {\begin{trivlist}\item[\hskip\labelsep{\bf Problem #1}\,]}{\end{trivlist}}


\newcommand{\var}[3]{V_{#1, #2, #3}}
\newcommand{\node}[3]{N_{#1, #2, #3}}
\newcommand{\ith}[2]{#1^{(#2)}}
\newcommand{\ind}[1]{\#(#1)}
\newcommand{\comment}[1]{}
\newcommand{\pair}[2]{\langle #1, #2 \rangle}


\title{Complexity of Problems on Graphs Represented as 
  OBDDs\footnotetext{An extended abstract of this paper appears 
  in the proceedings of the 1998 Symposium on Theoretical 
  Aspects of Computer Science.}}

\author{
\scriptsize{Joan Feigenbaum}\\[-8pt]
\scriptsize{AT\&T Labs\ --\ Research}\\[-8pt]
\scriptsize{Room C203, 180 Park Avenue}\\[-8pt]
\scriptsize{Florham Park, NJ 07932 USA}\\[-8pt]
\scriptsize{{\tt jf@research.att.com}}
	\and 
\scriptsize{Sampath Kannan}\\[-8pt]
\scriptsize{Computer and Information Sciences}\\[-8pt]
\scriptsize{University of Pennsylvania}\\[-8pt]
\scriptsize{Philadelphia, PA 19104 USA}\\[-8pt]
\scriptsize{{\tt kannan@central.cis.upenn.edu}}
	\and 
\scriptsize{Moshe Y. Vardi}\\[-8pt]
\scriptsize{Computer Science}\\[-8pt]
\scriptsize{Rice University}\\[-8pt]
\scriptsize{Houston, TX 77251 USA}\\[-8pt]
\scriptsize{{\tt vardi@cs.rice.edu}}
	\and 
\scriptsize{Mahesh Viswanathan}\\[-8pt]
\scriptsize{Computer and Information Sciences}\\[-8pt]
\scriptsize{University of Pennsylvania}\\[-8pt]
\scriptsize{Philadelphia, PA 19104 USA}\\[-8pt]
\scriptsize{{\tt maheshv@saul.cis.upenn.edu}}
}

\comment{
\author{ 
Joan Feigenbaum,\inst{1}
Sampath Kannan,\inst{2}
\thanks{Work done in part as a consultant to AT\&T
and supported in part by NSF grant CCR96-19910 and ONR Grant N00014-97-1-0505.}
Moshe Y. Vardi,\inst{3}
\thanks{Work done as a visitor to DIMACS and Bell Laboratories
as part of the DIMACS Special Year on Logic and Algorithms and
supported in part by NSF grants CCR-9628400 and CCR-9700061
and by a grant from the Intel Corporation.}
Mahesh Viswanathan\inst{2}
\thanks{Supported by grants NSF CCR-9415346, NSF CCR-9619910,
AFOSR F49620-95-1-0508, ARO DAAH04-95-1-0092, and ONR Grant N00014-97-1-0505.
}}
\institute{
AT\&T Labs\ --\ Research\\
Room C203, 180 Park Avenue\\
Florham Park, NJ 07932 USA\\
{\tt jf@research.att.com}
\and
Computer and Information Sciences\\
University of Pennsylvania\\
Philadelphia, PA 19104 USA\\
{\tt kannan@central.cis.upenn.edu}\\
{\tt maheshv@gradient.cis.upenn.edu}
\and
Computer Science\\
Rice University\\
Houston, TX 77251 USA\\
{\tt vardi@cs.rice.edu}
}
}
\date{6 August 1999}

\begin{document}


%% 
%% Insert new MIT Press title page
%%
\def\registered{\({}^{\ooalign%
    {\hfil\raise.07ex\hbox{{\tiny\textup{R}}}%
    \hfil\crcr\scriptsize\mathhexbox20D\cr}}\)}
\begin{titlepage}
\pagenumbering{roman}
\null\vfil\vskip 60pt
\begin{center}
{\Huge\bf Chicago\nolinebreak[1] Journal of Theoretical Computer\nolinebreak[1] Science\par}
\vskip 3em
{\huge\it The MIT Press\par}
 \end{center}
\par\vskip 1.5em
{\Large
  \begin{center}
    Volume 1999, Article 5\\
    \textit{Complexity of Problems on Graphs Represented as OBDDs}
  \end{center}
}
\par\noindent
ISSN 1073--0486\@. MIT Press Journals, Five Cambridge Center, Cambridge, MA
02142-1493 USA; (617)253-2889;
\emph{journals-orders@mit.edu, journals-info@mit.edu}\@.
Published one article at a time in \LaTeX\ source form on the
Internet\@. Pagination varies from copy to copy\@. For more
information and other articles see:
\begin{itemize}
  \item \emph{http://mitpress.mit.edu/CJTCS/}
  \item \emph{http://www.cs.uchicago.edu/publications/cjtcs/}
  \item \emph{ftp://mitpress.mit.edu/pub/CJTCS}
  \item \emph{ftp://cs.uchicago.edu/pub/publications/cjtcs}
\end{itemize}

\par\noindent
The \emph{Chicago Journal of Theoretical Computer Science} is
abstracted or indexed in \emph{
Research Alert,\registered
SciSearch, \registered
Current Contents\registered/Engineering
Computing \& Technology}, and \emph{CompuMath Citation Index\@.\registered}

\par\noindent\copyright 1999 The Massachusetts Institute of Technology\@.
Subscribers are licensed to use journal articles in a variety of
ways, limited only as required to ensure fair attribution to authors
and the journal, and to prohibit use in a competing commercial
product\@. See the journal's World Wide Web site for further
details\@. Address inquiries to the Subsidiary Rights Manager, MIT
Press Journals; (617)253-2864;
\emph{journals-rights@mit.edu}\@.\pagebreak[2]

\par\noindent The \emph{Chicago Journal of Theoretical Computer Science}
is a peer-reviewed scholarly journal in theoretical computer
science\@. The journal is committed to providing a forum for
significant results on theoretical aspects of all topics in computer
science\@.
\par
\begin{trivlist}
  \item[\emph{Editor-in-Chief:}] Janos Simon
  \item[\emph{Consulting Editors:}]
    Joseph Halpern, Eric Allender, Raimund Seidel
  \item[\emph{Editors:}]
    \begin{tabular}[t]{lll}
	Martin Abadi & Greg Frederickson & John Mitchell \\
	Pankaj Agarwal & Andrew Goldberg & Ketan Mulmuley \\
	Georg Gottlob & Gil Neiger & Tetsuo Asano  \\
	Vassos Hadzilacos & David Peleg & Laszl\'o Babai \\
	Juris Hartmanis & Andrew Pitts & Eric Bach \\
	Maurice Herlihy & James Royer & Stephen Brookes \\
	Ted Herman & Alan Selman & Jin-Yi Cai \\
	Stephen Homer & Nir Shavit & Anne Condon \\
	Neil Immerman & Eva Tardos & Cynthia Dwork \\
	Howard Karloff & Sam Toueg & David Eppstein \\
	Philip Klein & Moshe Vardi & Ronald Fagin \\
	Phokion Kolaitis & Stuart Kurtz & Jennifer Welch \\
	Lance Fortnow & Stephen Mahaney & Pierre Wolper \\
	Steven Fortune & Michael Merritt
    \end{tabular}
  \vspace{1ex}
  \item[\emph{Managing Editor:}] Michael J.\ O'Donnell
  \vspace{1ex}
  \item[\emph{Electronic Mail:}] \emph{chicago-journal@cs.uchicago.edu}
\end{trivlist}
\vfil\null
\end{titlepage}
\maketitle
\pagenumbering{arabic}


%%
%% End of titlepage insert
%%






\begin{abstract}

To analyze the com\-ple\-xi\-ty of decision problems on graphs, one
nor\-mal\-ly as\-sumes that the input size is polynomial in the number
of vertices. Galperin and Wigderson \cite{cj99-05-13} and, later,
Papadimitriou and Yannakakis \cite{cj99-05-19} investigated the complexity of
these problems when the input graph is represented by a
polylogarithmically succinct circuit.  They showed that, under such a
representation, certain trivial problems become intractable and that,
in general, there is an exponential blowup in problem
complexity. Later, Balc\'{a}zar, Lozano, and Tor\'{a}n
\cite{cj99-05-01,cj99-05-02,cj99-05-03,cj99-05-23} extended these results to problems whose
inputs are structures other than graphs.

In this paper, we show that, when the input graph is represented by an
ordered binary decision diagram (OBDD), there is an exponential 
blowup in the complexity of most graph problems. In particular, we show
that the GAP and AGAP problems become complete for PSPACE and EXP,
respectively, when the graphs are succinctly represented by OBDDs.

\end{abstract}

\section{Introduction}

The efficiency of algorithms is generally measured as a function of
input size (see \cite{cj99-05-11}).  In analyses of graph-theoretic algorithms,
graphs are usually assumed to be represented either by adjacency
matrices or by adjacency lists.  Nevertheless, many problem domains, most
notably, com\-pu\-ter-aided verification
(refer to \cite{cj99-05-06,cj99-05-08,cj99-05-17}), 
involve extremely large graphs
that have regular, repetitive structure.  This regularity can yield
very succinct encodings of the input graphs, and hence one expects a
change in the time complexity or space complexity of the graph problems.

The effect of succinct input representations on the complexity of
graph problems was first formalized and studied by Galperin and
Wigderson \cite{cj99-05-13}.  They discovered that, when adjacency matrices
are represented by polylogarithmically sized circuits, many
computationally tractable problems become intractable.  Papadimitriou
and Yannakakis \cite{cj99-05-19} later showed that such representations
generally have the effect of exponentiating the complexity (time or
space) of graph problems. Following this line of research,
Balc\'{a}zar, Lozano, and Tor\'{a}n \cite{cj99-05-01,cj99-05-02,cj99-05-03,cj99-05-23}
extended these results to problems whose inputs are structures other
than graphs and provided a general technique to compute the complexity
of problems with inputs represented by succinct
circuits~\cite{cj99-05-03}. They also provided sufficiency conditions for
problems that become intractable when inputs are represented in this
way.  Veith \cite{cj99-05-24,cj99-05-25} showed that, even when inputs are
represented using Boolean formulae (instead of circuits), a problem's
computational complexity can experience an exponential blowup. He
also gave sufficiency conditions for when the problems become hard.

The possibility of representing extremely large graphs succinctly has
attracted a lot of attention in the area of com\-pu\-ter-aided
verification (e.g., 
\cite{cj99-05-06,cj99-05-08,cj99-05-17}).  In this domain,
graphs are represented by {\it ordered binary decision diagrams\/}
(OBDDs).  OBDDs are special kinds of rooted, directed acyclic graphs
that are used to represent Boolean formulae.  Because of their
favorable algorithmic properties, they are widely used in the areas of
digital design, verification, and
testing (see \cite{cj99-05-07,cj99-05-08,cj99-05-18}).  
Experience has shown that
OBDD-based algorithmic techniques scale up to industrial-sized
designs (see \cite{cj99-05-10}), 
and tools based on such techniques are gaining
acceptance in industry (refer to 
\cite{cj99-05-04}).  Although OBDDs provide canonical
succinct representations in many practical situations, they are
exponentially less powerful than Boolean circuits, in the formal sense
that Boolean functions exist that have polynomial-sized circuit
representations but do not have subexponential-sized OBDD
representations (see \cite{cj99-05-20,cj99-05-21}). 
(On the other hand, the
translation from OBDDs to Boolean circuits is linear \cite{cj99-05-06}.)
Thus, the results of 
\cite{cj99-05-02,cj99-05-03,cj99-05-13,cj99-05-19,cj99-05-23,cj99-05-24,cj99-05-25} do not
apply to OBDD-represented graphs.  Furthermore, even though Boolean
formulae are, in terms of representation size, less powerful than
circuits, they are still more succinct than OBDDs.  Translation from
OBDDs to formulae leads to at most a quasi-polynomial ($n^{\log n}$)
blowup, whereas there are functions (e.g., multiplication of
binary integers) that have polynomial-sized formulae but require
exponential-sized OBDDs.  Indeed, while the satisfiability problem is
NP-complete 
for Boolean formulae, it is in nondeterministic logspace
for OBDDs (see \cite{cj99-05-06}).  
Therefore, the results in \cite{cj99-05-24,cj99-05-25}
do not apply to our case.

In this paper, we show that, despite these theoretical limitations on
the power of OBDDs to encode inputs succinctly, using them to
represent graphs nonetheless causes an exponential blowup in problem
complexity.  That is, the well-studied phenomenon of exponential
increase in computational complexity for graph problems with inputs
represented by Boolean circuits or
formulae 
(see \cite{cj99-05-02,cj99-05-03,cj99-05-13,cj99-05-19,cj99-05-23,cj99-05-24,cj99-05-25}) 
also occurs when the
graphs are represented by OBDDs.  Graph properties that are ordinarily
NP-complete become 
NEXP-complete.  The graph accessibility problem
(GAP) and the alternating graph accessibility problem (AGAP) for
OBDD-encoded graphs are PSPACE-complete and EXP-complete,
respectively.  Both GAP and AGAP are important problems in {\it model
checking}, a domain in which OBDDs are widely
used (refer to \cite{cj99-05-08,cj99-05-12,cj99-05-15,cj99-05-16}).

In Section \ref{sec:prelm}, we formally define OBDDs and present some
known results about them. In Section \ref{sec:py}, we discuss the
problem in greater detail and compare Papadimitriou and Yannakakis's
result to ours. Finally, in Sections \ref{sec:nexp}--\ref{sec:gap},
we give our technical results.

\section{Preliminaries} \label{sec:prelm}

\begin{definition}
A {\it binary decision diagram\/} (BDD) is a single-rooted, directed
acyclic graph in which
\begin{itemize}
\item Each internal node (i.e., a node with nonzero outdegree) 
is labeled by a Boolean variable.
\item Each internal node has outdegree $2$. One of the outgoing edges is
labeled  $1$ (the ``then-edge'') and the other is labeled
$0$ (the ``else-edge'').
\item Each external node (i.e., a node with zero outdegree) is 
labeled $0$ or $1$.
\end{itemize}
\end{definition}

Let $X = \{ x_1, x_2, \ldots, x_n \}$ be the set of Boolean variables
that occur as labels of nodes in a given BDD $B$. Each assignment
$\alpha = (\alpha_1, \alpha_2, \ldots, \alpha_n)$ of Boolean values to
these variables naturally defines a computational path---the one
that leads from the root to an external node and has the property
that, when it reaches a node labeled $x_i$, it follows the edge
labeled $\alpha_i$, for all $i$.

\begin{definition}
A BDD $B$ {\it represents the Boolean function\/} $f(x_1, x_2, \ldots,
x_n)$ if, for each assignment $\alpha = (\alpha_1, \alpha_2, \ldots,
\alpha_n)$ to the variables of $f$, the computation path defined by
$\alpha$ terminates in an external node that is labeled by the value
$f(\alpha_1, \alpha_2, \ldots, \alpha_n)$.
\end{definition}

\begin{definition}
Two nodes $u$ and $v$ of a BDD are {\it equivalent\/} if the BDDs
rooted at $u$ and $v$ represent the same Boolean function. A BDD in
which no two different nodes are equivalent is called {\it reduced}.
\end{definition}

\begin{definition}
Let $<$ be a total ordering on a set $X$.  An {\it ordered binary
decision diagram\/} (OBDD) over $(X, <)$ is a reduced BDD with
node-label set $X$ such that, along any path from the root to an
external node, there is at most one occurrence of each variable, and
the order in which the variables occur along the path is consistent
with the order $(X, <)$.  The {\it size\/} of an OBDD is the number of
internal nodes in it.
\end{definition}

\begin{definition}
\label{dfn:gr-rep}
An OBDD $O$ {\it represents the graph\/} $G = (V, E)$ if $O$ represents the
Boolean function $\adj$, where
\[ \adj(v_1, v_2) = \left\{ \begin{array}{ll}
			1 & \mbox{if and only if $\pair{v_1}{v_2} \in E$} \\
			0 & \mbox{otherwise.}
			\end{array}
		\right. \]
\end{definition}

\begin{theorem}[Bryant~\cite{cj99-05-06}] \label{bryant1}
For each Boolean function $f$ and ordering $(X,<)$ of the set
of variables $X$, there is a unique (up to isomorphism) OBDD over
$(X,<)$ that represents $f$.
\end{theorem}

\begin{theorem}[Bryant~\cite{cj99-05-06}] \label{bryant2}
Let $F$ and $G$ be OBDDs over $(X,<)$ representing functions $f$ and
$g$, respectively. Let the size of $F$ be $m$, the size of $G$ be $n$,
and $\langle \op \rangle$ be a binary Boolean operation.  Then there is
an OBDD over $(X,<)$ of size at most $mn$ and constructable in time
polynomial in $m$ and $n$ that represents $f \langle \op \rangle g$.
\end{theorem}

\begin{definition}

Let $L = (G, <)$ be a linear order on the gates of a circuit, where
the inputs and outputs are classified as special instances of
gates. We say that the {\em forward cross section of the circuit at
gate\/} $g$ is the number of wires connected to the output of some gate
$g_1$ AND an input of some gate $g_2$ such that $g_1 \leq g$ and $g <
g_2$. The {\em reverse cross section of the circuit at gate\/} $g$ is
the number of wires connected to an output of some gate $g_1$ and an
input of some gate $g_2$ such that $g_2 \leq g$ and $g < g_1$.

\end{definition}

\begin{definition}
The {\it forward width of a circuit under order $L$}, denoted $w_f$, is the
maximum, over all gates $g$, of the forward cross section at $g$. Similarly,
{\it the reverse width of the circuit under order $L$}, denoted by $w_r$, is
the maximum, over all gates $g$, of the reverse cross section at $g$.
\end{definition}

\begin{theorem}[Berman~\cite{cj99-05-05}]
\label{berman}
For a circuit and gate ordering with $w_r = 0$, there exists a
variable ordering such that the OBDD size is bounded by $n2^{w_f}$,
where n is the number of inputs to the circuit.
\end{theorem}

\begin{notation}
We are interested in complexity classes ${\bf C}$ that have
universal Turing machines and complete problems.  Let $U_{\bf C}$
denote the universal Turing machine for the complexity class {\bf
C}. Let $\univ{C}$ be the language accepted by the machine $U_{\bf C}$;
that is, $\univ{C} = \{ x : x$ encodes a ${\bf C}$-bounded Turing
machine $M$ and an input $y$ such that $M$ accepts $y \}$.

For an n-bit number $x$, we  refer to the $i$th bit by
$\ith{x}{i}$, where $\ith{x}{n}$ is the most significant bit.
\end{notation}

\section{Problem statement}\label{sec:py}

Papadimitriou and Yannakakis~\cite{cj99-05-19} show that any NP-complete
graph property $\pi$ to which satisfiability is reducible by a {\em
projection}, in the sense of Skyum and Valiant~\cite{cj99-05-22}, becomes
NEXP-complete when problem instances are encoded as circuits.  They
do this by first constructing a circuit that computes the
clause-literal incidence matrix of a formula $F(x)$ (i.e., given
a clause and a literal, the circuit decides whether the literal occurs
in the clause in $F(x)$) such that $F(x)$ is satisfiable if and only if
$x \in \univ{NEXP}$. Then, using the properties of projection, they
construct a circuit representing a graph $G(x)$ such that
$G(x)$ has a property $\pi$ if and only if $x \in \univ{NEXP}$.

When graphs are represented by OBDDs, such reductions are not
immediately obtainable, for two basic reasons. First, OBDDs are
strictly less powerful than Boolean circuits, in the sense that there
are Boolean functions that have small circuit representations but no
small OBDD representations. In particular, the function that computes
the $i$th bit of the product (or quotient) of two binary numbers
cannot be represented by a small OBDD
(see~\cite{cj99-05-20,cj99-05-21}).
Second, the size of OBDDs is sensitive to the ordering of the
variables of the function, and the OBDD representing the Boolean
combination of two OBDDs can be constructed quickly only when the
ordering of the variables is consistent in the two OBDDs. Hence, for a
result equivalent to Papadimitriou and Yannakakis's to hold for graphs
represented by OBDDs, we must construct reductions $f$ such that the
$j$th bit of $f(x)$ can be found by a small OBDD given $j$ as the
input, assuming that the $i$th bit of $x$ can be found by a small
OBDD given $i$ as the input. Furthermore, all OBDDs involved must read
the bits in consistent order.

\section{Cook's theorem} \label{sec:cook}

In order to show that satisfiability is NP-hard, Cook~\cite{cj99-05-09}
constructed a Boolean formula $F(x)$, given a string $x$ encoding a
nondeterministic Turing machine decription and an input string, such
that $F(x)$ is satisfiable if and only if the machine accepts the
input in polynomial time. If we view computation as a sequence of
machine descriptions,\footnote{A machine description is a sequence
that describes the values of the tape cells and the position of the
input head.} then the formula essentially encodes the following:
Each
machine description is correct and follows from the previous
description in the sequence, and the machine finally enters
an accepting state. We now describe this formula $F(x)$ more formally.

When describing the machine at some instant, we group the state
of the machine and the index of the next step taken by the machine,
with the symbol scanned to form a single composite symbol whose
appearance also indicates the head position.  For each time instant
$i$, for each tape cell $j$, and for each symbol $X$, which can either
be a symbol of the tape alphabet or a composite symbol, we create a
Boolean variable $\var{i}{j}{X}$ to indicate that the content of cell
$j$ at time $i$ is $X$. If $p(n)$ denotes the polynomial time bound on
the machine, then the formula $F(x)$ is a conjuction of the following
four formulae:
\begin{itemize}
\item[(A)] $\varphi_A = (\var{0}{0}{\triangleright}) \wedge
                 (\var{0}{1}{a_1} \vee \var{0}{1}{a_2} \vee \cdots
                 \vee \var{0}{1}{a_l}) \wedge %\\
 \bigwedge_{i=2}^{n}
                 \var{0}{i}{\ith{y}{i}} \wedge
                 \var{0}{n+1}{\triangleleft} \wedge
                 \bigwedge_{i=n+2}^{p(n)} \var{0}{i}{B}$. %\\ 
This basically says that at the start (time $0$), the tape contains
the input between the left ($\triangleright$) and right end-markers
($\triangleleft$), and the rest of the tape is blank. The symbols
$a_i$ encode the start state, first input symbol, and various
nondeterministic choices available initially.
\item[(B)] $\varphi_B = \bigvee_j (\bigvee_{X \in F} \var{p(n)}{j}{X})$. %\\
This says that at time $p(n)$ the machine is one of the final states.
($F$ is the set of composite symbols encoding a final state and a tape
symbol.)
\item[(C)] $\varphi_C = \bigwedge_{i,j} [ \bigvee_X \var{i}{j}{X}
\wedge \neg (\bigvee_{X \neq Y} (\var{i}{j}{X} \wedge
\var{i}{j}{Y}))]$. %\\
This says that at each time and for each cell, there is exactly one symbol.
\item[(D)] $\varphi_D = \bigwedge_{i,j} [\bigvee_{(W,X,Y,Z) \in \Quad}
( \var{i}{j-1}{W} \wedge \var{i}{j}{X} \wedge \var{i}{j+1}{Y} \wedge
\var{i+1}{j}{Z})]$,
where $\Quad$ is the set of all quadruples $(W,X,Y,Z)$ such that if the
symbols in the $(j-1)$th, $j$th, and $(j+1)$th cells of the tape are
$W$, $X$, and $Y$, respectively, then at the next time instant the symbol
at the $j$th cell is $Z$. So this says that the symbol at each
time and for each cell follows correctly from those at the previous
time instance.
\end{itemize}

\section{A small OBDD for a NEXP tableau} \label{sec:nexp}

\begin{figure}[tbh]
\begin{center}
\psfig{file=cj9905f1.eps,height=3in}
%\includegraphics{atab}%.eps}
\caption{\footnotesize 
A NEXP Tableau. Rows represent contents of tape cell at a
particular time instance. Time increases as you go down.}
\end{center}
\label{fig:tableau}
\end{figure}

Applying Cook's theorem to the tableau of a nondeterministic,
exponential-time Turing machine produces a Boolean formula with
exponentially many clauses and literals such that the formula is
satisfiable if and only if the tableau represents a valid, accepting
computation. In this section, we show that this formula can be
represented succinctly by an OBDD.  This means that we can fix an
enumeration of the clauses and literals such that, given the indices
of a clause and of a literal, we can determine whether the literal
occurs in the clause. Our proof exploits the great regularity of the
formula in question.  As can be seen in Figure~\ref{fig:tableau}, a
literal corresponding to cell $j$ at time $i-1$ occurs only in the
clauses corresponding to cells $j-1$, $j$, and $j+1$ at time $i$. This
implies that by a suitable ordering of the clauses, we can ensure the following:
Roughly speaking, for a given input $x$, there is a small, fixed
constant $c$ such that a literal with index $l$ occurs only in clauses
with indices between $(l-1) c + 1 + K$ and $lc + K$, where $K$ is some
(not necessarily small) number.

We begin by proving (in Lemmas~\ref{div} and \ref{add}) that this
range check can be computed by a small OBDD. The constructed OBDD uses
an ordering of variables wherein bits of the literal index and bits of
the clause index are interleaved. This construction plays a central
role in the proof of the main theorem of this section.

\begin{lemma}\label{div}\label{mod}
For a fixed integer $Y$, there is a circuit with $w_f = \log\ Y + 2$
and $w_r = 0$ that, given an ordering $\ith{x}{n} < \ith{x}{n-1} <
\cdots < \ith{x}{1}$ on input bits, computes the $i$th bit of $x /
Y$ (``$/$'' denotes integer division), for all $i$.  Similarly, for a
fixed $Y$, there is a circuit with $w_f = \log\ Y + 2$ and $w_r = 0$
that, given an ordering $\ith{x}{n} < \ith{x}{n-1} < \cdots <
\ith{x}{1}$ on input bits, computes the $i$th bit of $x\ mod\ Y$,
for all $i$.
\end{lemma}

\begin{proof}
A circuit that does long division by repeated subtraction computes
both the quotient and the remainder and has the above properties.
\end{proof}

\begin{lemma}\label{add}
Let $f$ be a function such that $\ith{f(x)}{i}$ depends only on
$\ith{x}{n}, \ith{x}{n-1},$ $\ldots, \ith{x}{i}$.  Given an ordering
$\ith{x}{n} < \ith{y}{n} < \ith{x}{n-1} < \cdots < \ith{y}{1}$ on
input bits, there is a circuit that checks whether $f(x \pm K) = y$,
for a fixed integer $K$, with $w_r = 0$ and $w_f = 2W + 4$, where $W$
is the forward width of the circuit that computes $f(x)$ given the
same ordering on input bits.
\end{lemma}

\begin{proof}
We  now present the construction for a circuit computing the
function $f(x + K)$ in detail. The case of $f(x - K)$ is similar, and
we present a sketch of the proof at the end.

The difficulty arises in computing $x + K$, using the given ordering
on the input bits. If we used the reverse ordering, going from least
significant bits to most significant bits, designing a circuit with
the desired widths would be simple. Unfortunately, the circuit
computing $f$ does so with a different ordering.

In order to compute the $i$th bit of the sum, we need to know
whether  $(\ith{x}{i-1}\ith{x}{i-2}\cdots \ith{x}{1} +
\ith{K}{i-1}\ith{K}{i-2}\cdots \ith{K}{1})$ yields a carry, and we
cannot know this until we compute the sum.

We overcome this obstacle using essentially the same idea
as is used in carry-look-ahead adders. A bit position $i$
is a carry {\em generator} if $\ith{x}{i}$ and $\ith{K}{i}$
are 1; it is a carry {\em propagator} if exactly one of these
bits is 1; it is  a  carry {\em killer} if both of these bits
are 0.

Initially, we compute $\ith{f(x + K)}{n}$ in two ways, one assuming
that there is a carry into the $n$th position and the other
assuming that there is no carry into the $n$th position. We compare
each value of $\ith{f(x + K)}{n}$ with $\ith{y}{n}$ terminating any
computation path that leads to inequality. Inductively, suppose that
we compute at most two different values for $\ith{f(x + K)}{i}$
and compare both with $\ith{y}{i}$.  If position $i-1$ is a
generator, we abandon the path in which there is no carry into
position $i$ and continue the path in which there is a carry into
position $i$ in two ways---one assuming there is a carry into
position $i-1$ and the other assuming not. Similarly, if position
$i-1$ is a propagator, we continue the path assuming a carry into
position $i$ by assuming that there is a carry into position $i-1$, and
we continue the path assuming no carry into position $i$ by assuming
that there is no carry into position $i-1$. Finally, if position $i-1$
is a carry killer, we abandon the path assuming that there is a carry
into position $i$, and once more we are left with at most two paths to
continue. Clearly, only one of these two paths is correct at the
end, and if along this path we have determined that the bits of
$f(x+K)$ are equal to the bits of $y$, we output a 1; otherwise we
output a 0. Our computation is an appropriate interleaving of the
carry-look-ahead adder, the circuit that computes $f$ hypothesized in
the lemma, and a circuit that checks equality of the bits of $f(x+K)$
and the bits of $y$.

To compute $f(x - K)$ we proceed in a similar manner.
\end{proof}

\begin{notation}
Consider the language $\univ{NEXP}$. Let $F(x)$ be the CNF Boolean
formula obtained by the exponential version of Cook's construction,
in which $F(x)$ is satisfiable if and only if $x \in \univ{NEXP}$.
\end{notation}

\begin{theorem} \label{cook-red}
Let $g_x$ be the Boolean function that decides whether a given literal
occurs in a given clause in $F(x)$; that is, $g_x(Cl, Lt) = 1$ if
and only if the literal whose index is $Lt$ occurs in the clause of
$F(x)$ whose index is $Cl$.  There is an OBDD of size 
polynomial in the length of $x$ that represents the function $g_x$.
\end{theorem}

\begin{proof}
As we saw in Section~\ref{sec:cook} there are four categories of
clauses in $F(x)$:
\begin{itemize}
\item[(A)] Clauses that state that, at time $0$, the tape contains the 
input string, and the machine is in the initial state
\item[(B)] Clauses that state that, at time $2^{p_M(n)}$, the machine is 
in one of the final states
\item[(C)] Clauses that state that, at time $i$, $0\leq i\leq 2^{p_M(n)}$,
each tape cell contains exactly one symbol of the tape alphabet
\item[(D)] Clauses that state that, at time $i$, $0\leq i\leq 2^{p_M(n)}$,
the contents of the tape cells and the state of the machine follow from those 
at the previous time $i-1$ by a valid ``move'' of the machine
\end{itemize}

We first list all the clauses in category A, then those in
category B, and then, finally, those in categories C and D. The
clauses in categories C and D are interleaved so that all
clauses in these two categories referring to the same cell of the
tableau occur together in the enumeration starting from $\pair{0}{0}$, 
that is, cell 0 and time 0, and proceeding in row major order.

An important property becomes clear in the proof: 
There is an integer $W$ such that, for each pair $i,j$, the number of
clauses in category C and D for time $i$ and tape cell $j$ is $W$,
and $W$ depends only on the alphabet size and the maximum
nondeterministic branching possible at any state.  Hence, for the
above listing of the clauses, determining the time and cell to which a
given clause number refers involves dividing by this fixed constant
$W$ and not by a number that is a function of $i$ or $j$. This is very
important, because the function that determines the quotient when one
number is divided by another does not, in general, have a small OBDD
representation.  Because there is a fixed constant $W$, we can use
Lemma~\ref{div}.

The literals $\var{i}{j}{X}$ have the same meaning as in
Section~\ref{sec:cook}, and they are numbered in the following order:
$\var{0}{0}{\sigma_1}, \neg \var{0}{0}{\sigma_1}$, $\ldots$,
$\var{0}{0}{\sigma_m}, \neg \var{0}{0}{\sigma_m},
\var{0}{1}{\sigma_1}$, $\ldots$, $\neg \var{0}{2^{p_M(n)}}{\sigma_m},
\var{1}{0}{\sigma_1}$, $\ldots$, $\neg
\var{2^{p_M(n)}}{2^{p_M(n)}}{\sigma_m},$ where $\Gamma = \{ \sigma_1,
\sigma_2, \ldots, \sigma_m \}$ is the set of tape symbols and
composite symbols.

\begin{notation}

We use $\ind{X}$ to denote the index of X, where X is a literal,
clause, or symbol in the enumeration.

\end{notation}

We now show that, for the set of clauses in any category, $g_x$
when restricted to this set of clauses can be represented by an OBDD
of polynomial size. Since $g_x$ is a logical OR
of all these
(constant number of) Boolean functions, Theorem~\ref{bryant2} implies
that there is a polynomial-sized OBDD that represents $g_x$.

In the rest of the proof, we only consider OBDDs with the
following ordering on the variables: $Cl^{(k)}, Lt^{(k)},
Cl^{(k-1)}, Lt^{(k-1)}, \ldots, Cl^{(1)}, Lt^{(1)}$, where $Cl$ is the
index of a clause and $Lt$ is the index of a literal.

\begin{case}{A}

Each clause in this category consists of a single literal.  Clauses
corresponding to cell positions $\pair{0}{0}$ to $\pair{0}{n+1}$
specify that the top row faithfully represents the input string
$\ith{y}{1}, \ldots, \ith{y}{n}$ along with suitable end-markers and
the start state, while clauses corresponding to cell positions
$\pair{0}{n+2}, \ldots, \pair{0}{2^{p_M(n)}}$ specify that these
symbols are $B$, the blank symbol.

Note that the OBDD is allowed to be of size polynomial in $n$. Thus we
can compute $g_x$ in the case when the clause number is between $0$
and $n+1$ by using an OBDD that resembles a trie.  Upon reading a
symbol, simply branch to the node in the trie that represents all
possible continuations of the clause and literal indices that would
make $g_x$ evaluate to 1. The size of the trie (and hence also the
size of the OBDD) is $O(n)$.

For clauses whose number is between $n+2$ and $2^{p_M(n)}$, check that
$Lt \bmod 2m$ produces a number that encodes the blank symbol.
Lemma~\ref{div} implies that there is an OBDD, of small size, that can
compute the $i$th bit of $Lt \bmod 2m$. Now checking if $Lt$
encodes a blank symbol just involves checking that each bit $Lt \bmod
2m$ is ``correct,'' and since the number of bits in $Lt \bmod 2m$ is
bounded by the input size ($|x|$), this conjunction has a small
(polynomial in $|x|$) sized OBDD.

The OR
of these two OBDDs computes $g_x$ in case A.

\end{case}

\begin{case}{B}

The clauses in this category are
$$ \bigvee_j \left(\bigvee_{X\in F} \var{2^{p_M(n)}}{j}{X}\right),$$ 
where $F$ is the set of composite symbols that encode a final state 
and symbol pair.

Here we need to test that $Cl = 2^{p_M(n)} + 1$, $Lt\ \bmod\ 2m$ is a
symbol that encodes a final state, and that $Lt$ is an index of a
literal corresponding to time $2^{p_M(n)}$, that is, $Lt/2m \geq
\pair{2^{p_M(n)}}{0}$. The first two tests clearly have small OBDDs.
Because $|F| \leq m$ (the size of the set of tape symbols and
composite symbols), the OBDD that decides whether a number ($\leq 2m$)
is a symbol in $F$ has at most $m$ paths and so is small. Thus we also
have a small OBDD representation for $g_x$ in this case.

\end{case}

\begin{case}{C}

The clauses in this case are
\begin{eqnarray*}
\bigvee_X \var{i}{j}{X}&&\\
\neg \var{i}{j}{X} \vee \neg \var{i}{j}{Y},&\quad\mbox{where}&X \neq Y.
\end{eqnarray*}
Recall that we interleaf the clauses in categories C and D.
Thus part of the tests in both these categories involve checking
whether the ``block'' (i.e., the $\pair{i}{j}$ pair) is
``correct.''

The block and offset within a block, for the
index of a clause, can be determined as follows: 
\begin{eqnarray*}
(Cl - K_1)/K_2 &=& \mbox{block and}\\
(Cl - K_1)\ \bmod\ K_2 &=& \mbox{offset,}
\end{eqnarray*}
where $K_1 = 2^{p_M(n)} + 1$
is the number of clauses in category A and B,
and $K_2$ 
is the number of clauses in category C and D for a fixed $i$
and $j$. 

Because $K_2$ is a constant that depends only on the alphabet size and
the maximum nondeterministic branching possible in $M$,
Lemmas~\ref{mod} and \ref{add} and Theorem~\ref{berman} imply that the
OBDDs that compute each bit of the block and offset are
small. Again, since the total number of bits in the block and
offset are bounded by the length of the input, $|x|$, checking if
the block (or offset) is equal to some value can be done by a
small OBDD.

\begin{subcase}{1} 
In the case $(Cl - K_1) \bmod K_2 = 1$, we check that at
least one symbol occurs in each cell position. We see
whether $(Cl - K_1)/K_2 = Lt/2m$, $(Cl - K_1)\ \bmod\ K_2 = 1$, and $Lt\
\bmod\ 2m$ is odd (i.e., literal is positive). Each of these tests has a
small OBDD, and so subcase 1 presents no problems.

\end{subcase}

\begin{subcase}{2}

In the case $1 < (Cl - K_1)/K_2 \bmod K_2 \leq
{m \choose 2}
+ 1$,  
we test whether $(Cl -K_1)/K_2 =
Lt/2m$ and $Lt\ \bmod\ 2m$ occurs in the clause whose offset is
$(Cl - K_1)\ \bmod\ K_2$.

For each value of $(Cl - K_1)\ \bmod\ K_2$, the OBDD that checks for
the occurrence of $Lt\ \bmod\ 2m$ has two paths, because each such clause has
two literals, and thus it is small. The desired OBDD has
$O(m^2)$ paths, where, in the $i$th path, one checks for the
case $(Cl - K_1)\bmod K_2 = i$.  The OBDD in subcase 2 is thus
polynomial-sized.

\end{subcase}

\end{case} 

\begin{case}{D}

The Boolean formula that states that any transition of the machine
from one configuration to another must follow from a valid ``move''
of the machine looks like
$$ \bigvee_{(W,X,Y,Z) \in \Quad} ( \var{i}{j-1}{W} \wedge \var{i}{j}{X}
\wedge \var{i}{j+1}{Y} \wedge \var{i+1}{j}{Z}),$$
where $\Quad$ is the set of all quadruples $(W,X,Y,Z)$ with the
following property:  If the symbols in the $(j-1)$th, $j$th, and
$(j+1)$th cells of the tape are $W$, $X$, and $Y$, respectively, then at
the next time instant the symbol at the $j$th cell will be $Z$.

Distributing the $\vee$ over the $\wedge$'s gives the following set
of clauses:
$$\var{i}{j-1}{W_1} \vee \var{i}{j-1}{W_2}\vee \cdots \vee
\var{i}{j-1}{W_k},$$ 
$$\var{i}{j-1}{W_1} \vee \var{i}{j-1}{W_2} \vee
\cdots \vee \var{i}{j}{X_1},$$ 
$$\vdots$$ 
$$\var{i+1}{j}{Z_1} \vee \var{i+1}{j}{Z_2} \vee \cdots \vee 
\var{i+1}{j}{Z_k},$$ where $|\Quad| = k$.

\begin{subcase}{1}

We have the 
case of $(Cl - K_1)/K_2 = Lt/2m + 1$, that is, the one in which
the literal refers to the $(j-1)$th cell and time $i$ (or
$\pair{i}{j-1}$). We must check whether the symbol encoded by
$Lt$ is one of the $W_i$'s occurring in the clause.  The clauses
(for each $i$ and $j$) are listed as above. There is a close
correspondence between the offset of a clause (i.e., $(Cl - K_1)\
\bmod\ K_2$) represented in base 4 and the presence of a literal
$\var{i}{j-1}{W_i}$ in the clause: If the $i$th most significant
bit of the base-4 representation of the offset is a $0$, then
$\var{i}{j-1}{W_i}$ is present in the clause. Otherwise it is not. So
checking if $Lt$ is present in the clause $Cl$ involves checking if
certain bits of the offset are $0$. (A base-4 representation can be
obtained by grouping pairs of bits in the binary
representation.) Since the bits of the offset can be obtained by a
small OBDD, there is a small OBDD for this subcase.

\end{subcase}

Subcases 2 through 4 are listed below. Arguments showing that
there are small OBDDs for these cases are similar to the one in subcase 1.

\begin{subcase}{2}

$(Cl - K_1)/K_2 = Lt/2m$.
\end{subcase}

\begin{subcase}{3}

$(Cl - K_1)/K_2 = Lt/2m - 1$.

\end{subcase}

\begin{subcase}{4}

$(Cl - K_1)/K_2 = Lt/2m - 2^{p_M(n)}$.

\end{subcase}
\end{case} 
\end{proof}

\section{NP-complete graph problems}\label{sec:np}

Theorem~\ref{cook-red} can be used to prove that most classical
NP-complete graph problems are NEXP-complete when graphs are
represented by OBDDs.  We give one example of such a proof;
others are quite similar. 

We now consider the independent set problem. Recall that, in the
decision version of this problem, we are given a graph $G$ and an
integer $k$ in binary and are asked if $G$ has an independent set of size
at least $k$. For the succinct version of the problem, we assume
that we are given an OBDD $O$ representing the adjacency relation of a
graph and an integer $k$ in binary and are asked if the graph represented
by $O$ has an independent set of size at least $k$.

\begin{theorem}
The independent set problem for graphs represented by OBDDs is 
NEXP-complete.
\end{theorem}

\begin{proof}
Consider the standard reduction from 3-SAT to independent set.
In this reduction, we create a graph in which there is a node
for each occurrence of each literal and two nodes are adjacent
if and only if they either correspond to two literals in the same
clause or correspond to two complementary literals $x$ and $\bar{x}$
occurring in two different clauses.
Let $G_{F(x)}$ be the graph obtained by such a reduction from
the formula $F(x)$, for some string $x$ that encodes a $2^{p_M(n)}$-time
bounded Turing machine $M$ and an input $y$. Let each node of
$G_{F(x)}$ be named by the clause-literal pair corresponding
to it.

\begin{claim}
Given two vertices $(Cl_1, Lt_1)$ and $(Cl_2, Lt_2)$ of graph $G_{F(x)}$,
there is a polynomial-sized OBDD that decides whether these vertices are
adjacent.
\end{claim}

\begin{proof}
In order to check whether $(Cl_1, Lt_1)$ is adjacent to $(Cl_2, Lt_2)$,
we check whether $(Cl_1, Lt_1)$ and $(Cl_2, Lt_2)$ are ``valid''
vertices in $G_{F(x)}$. 
\begin{itemize}
\item[(a)] If either one of these vertices is not
valid, we declare them to be adjacent.
\item[(b)] If both are valid, we check whether they are adjacent
as per the reduction described above.
\end{itemize}

A node $(Cl, Lt)$ is valid if and only if the literal whose index is
$Lt$ occurs in the clause $Cl$, that is, if and only if $g_x(Cl,
Lt) = 1$.  From the previous section, we know that there is a small
OBDD that computes $g_x$, and so we have a small OBDD to check whether a
node is valid.

From the construction of $G_{F(x)}$, we know that two valid vertices
are adjacent if and only if either they correspond to literals in the
same clause or they correspond to complementary literals in different
clauses; that is, either $Cl_1 = Cl_2$ or $|Lt_1 - Lt_2| = 1$ and
$(Lt_1 - 1) / 2 = (Lt_2 - 1)/ 2$.  By Lemma~\ref{add}, both of these
checks can be done by small OBDDs whose orderings of the variables are
consistent with that of the OBDD for $g_x$.
\end{proof}

Thus the adjacency relation for graph $G_{F(x)}$ can be represented by
a small OBDD. Furthermore this OBDD can be constructed in polynomial
time. $G_{F(x)}$ has an independent set of size $K$, where $K$ is
the number of clauses in $F(x)$, if and only if $F(x)$ is satisfiable 
if and only if $x \in \univ{NEXP}$.

Hence, the independent set problem for graphs represented by OBDDs is
NEXP-complete.
\end{proof}

Papadimitriou and Yannakakis~\cite{cj99-05-19} prove the general theorem that,
if the reduction from SAT to an NP-complete problem $\pi$ is a projection,
then $\pi$ becomes NEXP-complete when the input is
represented by a circuit. The fact that the reduction is a projection
is a sufficient condition for their result, but it appears far from
necessary.

Here we state an analogous result. Let $f$ be a reduction from SAT to
an NP-complete problem $\pi$. Suppose there is a constant $k$ such
that, for all $j$, $\ith{f(x)}{j}$ is a function only of the bits
$\ith{x}{j_1}, \ldots , \ith{x}{j_k}$. Moreover, suppose that there is
a Mealy machine that
takes the bits of $j$ in some canonical order as input and produces
the bits of $j_1, \ldots , j_k$ in most significant to
least significant order.\footnote{A Mealy machine is a finite
automaton that produces an output on reading an input symbol;
see~\cite{cj99-05-14}.} 
More precisely, there is a finite automaton
that, on reading the $i$th bit of $j$, produces the $i$th most significant
bit of $j_1, \ldots, j_k$. We refer to the above class of
reductions as padding reductions.  Note that the class of padding
reductions is incomparable with the class of projections.

We state the following theorem and provide a sketch of the proof.

\begin{theorem} \label{nc0padding}
Let $f$ be a padding reduction from SAT to a problem $\pi$ in NP. Then
$\pi$ is NEXP-complete when its instances are presented as OBDDs.
\end{theorem}

\begin{proofsk}
Consider the instance $f(F(x))$ of problem $\pi$,
where as before $F(x)$ denotes the Boolean formula obtained when Cook's
theorem is applied to a NEXP tableau. We need to show that there is a
small OBDD $O$ that, when given $j$, outputs the value of
$\ith{f(F(x))}{j}$, or in other words, that there is a small OBDD
representation for the instance $f(F(x))$.

Essentially, since $f$ is an padding
reduction, on reading the first bit of $j$ we know the most
significant bits of $j_1, \ldots ,j_k$, and so on. So if we have $k$
copies of the OBDD representation of $F(x)$ (constructed in
Section~\ref{sec:nexp}), we can step through these OBDDs
simultaneously as we read each bit of $j$. Once we compute
$\ith{F(x)}{j_i}, \ldots, \ith{F(x)}{j_k}$, we can obtain the value of
$\ith{f(F(x))}{j}$. Since $k$ is a constant, this construction 
yields a polynomial-sized OBDD.
\end{proofsk}

Padding reductions can be found for a number of graph problems such as
clique, vertex cover, and so on. Such reductions are obtained by
taking the standard reductions and padding the target instances so
that each of its indices has sufficient information to allow the
reconstruction of the indices on which it depends. For example, in the
case of the independent set problem, we padded the indices of the
vertices of the graph obtained by the standard reduction. We labeled
the vertices by a clause-literal pair, and this helped in constructing
a small OBDD for the adjacency relation.

\section{The GAP and AGAP problems} \label{sec:gap}

In this section, we examine two graph problems that are crucially
important in computer-aided verification.  We show that both
experience exponential blowup in worst-case complexity when instances
are represented as OBDDs.

\begin{problem}{(GAP)}
The graph accessibility problem is as follows.
\begin{quote}
{\em Input:}  A directed graph $G$ and vertices $s$ and $t$ in the
graph.
\end{quote}
\begin{quote}
{\em Output:} Is there a directed path from $s$ to $t$?
\end{quote}
\end{problem}

\begin{theorem}

GAP is PSPACE-complete when the graph $G$ is represented by an
OBDD.

\end{theorem}

\begin{proof}

Let $p$ be a polynomial and $x$ be a string that encodes a
$p_M(|y|)$-space-bounded Turing machine $M$ and an input $y$. Without
loss of generality, we may assume that the machine $M$ has a single
accepting configuration $C_f$.

Consider the configuration graph $G_{M,y} = (V_{M,y}, E_{M,y})$
corresponding to the machine $M$ and input $y$, where
\begin{quote}
$V_{M,y} = \{ v_C\ |\ C$ is a possible configuration of
the machine, that is, $C$ is a string of symbols, of which one is a
composite symbol encoding a state of machine $M$ and a tape symbol, and
all the rest are tape symbols $\}$;
\end{quote}
\begin{quote}
$E_{M,y} = \{\pair{v_{C_1}}{v_{C_2}}\ |$ the machine $M$ can go
from configuration $C_1$ to a configuration $C_2$ in one step\}.
\end{quote}

If $C_i$ is the initial configuration of machine $M$ on input $y$,
then $M$ accepts $y$ if and only if the node labeled by $C_f$ is
reachable from the node labeled by $C_i$ in $G_{M,y}$. In other words,
$x \in \univ{PSPACE}$ if and only if the GAP problem on $G_{M,y}$ has
the answer ``yes.''

\begin{claim}

The edge relation $E_{M,y}$ in graph $G_{M,y}$ has a small OBDD
representation.

\end{claim}

\begin{proof}

We need to show that the function $e$, where

\[ e(C_1, C_2) = \left\{ \begin{array}{ll}
			1 & \mbox{if and only if $\ \pair{v_{C_1}}{v_{C_2}} \in E_{M,y}$} \\
			0 & \mbox{otherwise}
			\end{array}
		\right. \]

\noindent
can be represented by a small OBDD.  Computing the function $e$ entails
\begin{itemize}
\item[(a)] checking that $C_1$ and $C_2$ are possible configurations, 
that is, there is exactly one composite symbol in each of $C_1$ and $C_2$,
and
\item[(b)] checking whether the configuration $C_2$ can be reached from $C_1$
in one step by the machine $M$.
\end{itemize}

Checking to see whether a symbol is composite amounts to checking
whether the index of the symbol is greater than some constant, because
we list all the composite symbols in the end. Hence, check (a)
involves examining only the symbols of the configuration in the order in
which they occur and thus has a small OBDD representation.

Let $\Quad = \{ (W,X,Y,Z) |$ if $W$, $X$, and $Y$ are the symbols in the
$(j-1)$th, $j$th, and $(j+1)$th cells, respectively, at some time
instant, then $Z$ is the symbol in the $j$th cell at the next time
instant\}.  Checking whether configuration $C_2$ can be reached
from configuration $C_1$ in one step involves checking whether all the
symbols in $C_2$ arise from the corresponding symbols in $C_1$. That
is, we need to check that for all $j$, $(\ith{C_1}{j-1}, \ith{C_1}{j},
\ith{C_1}{j+1}, \ith{C_2}{j}) \in \Quad$. As we saw in the proof of
Theorem~\ref{cook-red}, the function that checks whether a given
quadruple is in $\Quad$ can be represented by a small OBDD.  We just
read the symbols of $C_1$ and $C_2$ alternately and keep checking
whether they ``conform.''  Note that we need to ``remember'' only two
symbols of $C_1$ as we go along.  Hence, at any level in the OBDD,
there are at most a constant number of nodes, and checking whether one
configuration can follow from another is representable by a small
OBDD.
\end{proof}

Because $G_{M,y}$ can be represented by a small OBDD that can be
constructed in polynomial time, the GAP problem for graphs represented
by OBDDs is PSPACE-complete.
\end{proof}

\begin{definition}
An AND-or graph is a directed graph $G$ with vertices labeled AND
or OR. Reachability in such graphs is recursively defined as
follows:
\begin{itemize}
\item[(a)] Every vertex is reachable from itself.
\item[(b)] If $u$ is an AND node, then $v$ is reachable from $u$ if
and only if $v$ is reachable from {\em all} $u_i$, such that
$\pair{u}{u_i}$ is an edge in the graph.
\item[(c)] If $u$ is an OR node, then $v$ is reachable from $u$ if and
only if $v$ is reachable from {\em any} $u_i$, such that
$\pair{u}{u_i}$ is an edge in the graph.
\end{itemize}
The OBDD representation of an AND-or graph is an OBDD that, given the
index of two vertices (which includes their label AND or OR),
determines if they are adjacent.

\end{definition}

\begin{problem}{(AGAP)}
The alternating graph accessibility problem is as follows.
\begin{quote}
{\em Input:} An AND-or graph $G$ and vertices $s$ and $t$ in $G$.
\end{quote}
\begin{quote}
{\em Output:} Is $t$ reachable from $s$?
\end{quote}
\end{problem}

\begin{theorem}

The AGAP problem for graphs represented by OBDDs is EXP-complete.

\end{theorem}

\begin{proof}

Because the AGAP problem is in P for graphs represented by
adjacency matrices, it is in EXP for graphs represented by OBDDs.

Let $x$ be a string that encodes a $2^{p_M(n)}$-time-bounded Turing
machine $M$ and an input $y$.  We construct an AND-or graph with
two special vertices $s$ and $t$, such that $t$ is reachable from
$s$ if and only if $x \in \univ{EXP}$. The construction of the graph is 
very similar to the construction of the circuit in the proof that circuit
value is P-complete.

Once again let $\Quad = \{ (W,X,Y,Z) |$ if $W,X,$ and $Y$ are the
symbols in the $(j-1)$th, $j$th, and $(j+1)$th cells,
respectively, at some time instant, then $Z$ is the symbol in the $j$th
cell at the next time instant\}.  Let $<$ be some ordering
on the quadruples in $\Quad$.

We construct the graph $G_{M,y}$ in stages, starting with the
empty graph.

\begin{stage}{0}

Add two AND nodes, one labeled 0 and the other 1. These nodes
represent false and true, respectively.

\end{stage}

\begin{stage}{1}

For each $j, 0 \leq j \leq 2^{p_M(n)}$, and each $X$, where $X$ is
either a tape symbol or a composite symbol encoding a state of machine
$M$ and a tape symbol, add an OR node labeled $\var{0}{j}{X}$. Add the
edge $\pair{\var{0}{j}{X}}{1}$ if the $j$th symbol in the initial
configuration of $M$ on input $y$ is $X$. Otherwise, add the edge
$\pair{\var{0}{j}{X}}{0}$.

\end{stage}

\begin{stage}{2i}

For each $j$ and $k$, add an AND node labeled $\node{i}{j}{k}$. Add
edges $\pair{\node{i}{j}{k}}{\var{i-1}{j-1}{W}}$, 
$\pair{\node{i}{j}{k}}{\var{i-1}{j}{X}}$, and 
$\pair{\node{i}{j}{k}}{\var{i-1}{j-1}{Y}}$, where the $k$th
quad\-ruple in $\Quad$ is $(W,X,Y,Z)$, for some $Z$.

\end{stage}

\begin{stage}{2i+1}

For each $j$ and symbol $Z$, add an OR node labeled
$\var{i}{j}{Z}$. For each $k$, if $(W,X,Y,Z)$ is the $k$th
quadruple, for some $W$, $X$, and $Y$, then add the edge
$\pair{\var{i}{j}{Z}}{\node{i}{j}{k}}$.

\end{stage}

\begin{stage}{\bf \mbox{\boldmath $2^{p_M(n)}+2$}}

Add an OR node $s$. For all $j$, add edges
$\pair{s}{\var{2^{p_M(n)}}{j}{X}}$, where $X$ is a composite symbol
encoding a final state and some tape symbol.

\end{stage}

The basic idea of the construction is as follows. The node label
$\var{i}{j}{X}$ means that, during the computation, at time $i$, the
$j$th tape cell contains the symbol $X$.  From the definition of
$\Quad$, it can be seen that 
$$
\var{i}{j}{Z} = \bigvee_{(W,X,Y,Z) \in \Quad} ( \var{i-1}{j-1}{W}
\wedge \var{i-1}{j}{X} \wedge \var{i-1}{j+1}{Y}).
$$
The string $y$ is accepted if, at time $2^{p_M(n)}$, the machine 
reaches a final state, that is,
$$
\bigvee_j \left(\bigvee_{X \in F} \var{2^{p_M(n)}}{j}{X}\right),
$$ 
where $F$ is the set of composite symbols that encode a final state 
and symbol pair.  Hence, the graph $G_{M,y}$ is such that node 1 is 
reachable from node $s$ if and only if $M$ accepts input $y$.

\begin{claim}

The graph $G_{M,y}$ can be represented by a small OBDD.

\end{claim}

\begin{proof}

There are no edges of the form
$\pair{\var{i_1}{j_1}{k_1}}{\var{i_2}{j_2}{k_2}}$ or
$\pair{\node{i_1}{j_1}{k_1}}{\node{i_2}{j_2}{k_2}}$. Also, the OBDD
deciding whether there is an edge of the form
$\pair{\var{0}{j}{X}}{1}$ is simple: Based on the value of $j$, just
check if the $j$th symbol of the input is $X$. The case of
$\pair{\var{0}{j}{X}}{0}$ is similar.

That leaves edges of only the following two forms:
$\pair{\node{i}{j}{k}}{\var{i-1}{j^\prime}{X}}$, where $j^\prime = j$
or $j-1$ or $j+1$, and $\pair{\var{i}{j}{X}}{\node{i}{j}{k}}$. In each
case, determining whether nodes $\var{i_1}{j_1}{X}$ and
$\node{I_2}{j_2}{k}$ are adjacent involves checking whether $i_1, i_2$
and $j_1, j_2$ differ by a constant and whether the symbol $X$ occurs
in the $k$th quadruple. That both these checks can be done by a
small OBDD was seen in the proof of Theorem~\ref{cook-red}.
\end{proof}

Thus the graph $G_{M,y}$ can be represented by a small OBDD that can
be constructed in polynomial time.  Furthermore, node $1$ is reachable from
$s$ in $G_{M,y}$ if and only if $x \in \univ{EXP}$.  Hence, the AGAP 
problem is EXP-complete for graphs represented by OBDDs.
\end{proof}

\section{Open questions} \label{sec:open}

The results that we prove in this paper are all negative: 
In the worst case, succinct encoding of instances using OBDDs
generates problems that are hard for PSPACE, EXP, or NEXP.  However,
one of our main motivations for this investigation is the observed
good performance of computer-aided verification tools on OBDD-encoded
instances.  Thus worst-case hardness results do not adequately capture
the complexity of the problems on real-world instances. It would
be desirable to have precise characterizations of the special cases
that occur in practice and of the special cases that can be solved
efficiently.

It would also be nice to have a general hardness result for OBDDs
that is analogous to Papadmitriou and Yannakakis's result for
circuits.  
%
In other words, is there a class of reductions such that
if any problem is complete for NP via a reduction in the class, 
the problem is
also complete for NEXP when instances are encoded as OBDDs? 
There has been
some recent work in this direction (refer to \cite{cj99-05-26}). 
Recall from
Definition~\ref{dfn:gr-rep} that an OBDD representation of a graph
is an OBDD that encodes the adjacency relation on vertices. Veith
\cite{cj99-05-26} obtains the general result for graphs that are encoded by
OBDDs wherein the ordering of the 
variables is {\em fixed}, namely, the
one where the bits of the first and second vertex are fed in
alternating order. He shows that any problem that is
complete for NP via {\em quantifier-free} reductions is also complete for
NEXP when the instances are encoded by OBDDs with the above
ordering. However, the question remains open for problems where
instances are encoded by OBDDs with a different variable ordering.

\section{Acknowledgement}

It is a pleasure to thank Ed Clarke for helpful comments on an earlier
draft of this paper. We would also like to thank Helmut Veith for
communicating his results to us.

\subsection*{Acknowledgment of support}
Kannan's work was done in part as a consultant to AT\&T
and supported in part by NSF 
grant CCR96-19910 and ONR Grant N00014-97-1-0505.
Vardi's work was done as a visitor to DIMACS and Bell Laboratories
as part of the DIMACS Special Year on Logic and Algorithms and
was supported in part by NSF grants CCR-9628400 and CCR-9700061
and by a grant from the Intel Corporation.
Viswanathan was supported by grants NSF CCR-9415346, NSF CCR-9619910,
AFOSR F49620-95-1-0508, ARO DAAH04-95-1-0092, and ONR N00014-97-1-0505.


\bibliography{cj99-05}
\bibliographystyle{alpha}

\end{document}

