%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}