%% Theory of Computing
%% File: v010a012.tex
%% Publication date: October 8, 2014
%% Authors: Eric Allender, Shiteng Chen, Tiancheng Lou, Periklis A. Papakonstantinou, and Bangsheng Tang
%
%
%
%

\documentclass{toc}

%
%
\tocdetails{%
volume=10, number=12, year=2014, firstpage=297,
%
%
%
received={August 8, 2012},
revised={July 14, 2013},
published={October 8, 2014},
%
doi={10.4086/toc.2014.v010a012}
}
%
\usepackage{latexsym}
\usepackage{amsbsy}
\usepackage{booktabs} %
\usepackage{array} %
\usepackage{verbatim} %
\usepackage{paralist} %
\usepackage{subfig} %
%
\usepackage{algorithm}
\usepackage{algpseudocode}
\usepackage{xspace}
\usepackage{xfrac}

\newcommand{\mathopp}{\mathbf}

\newcommand{\pw}{\mathcal{PW}}
\newcommand{\tw}{\mathcal{TW}}

%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
\newcommand{\np}{\cclass{NP}}
\newcommand{\p}{\cclass{P}}
\newcommand{\NL}{\cclass{NL}}
\newcommand{\cnf}{\cproblem{CNF}}
\newcommand{\pspace}{\cclass{PSPACE}}
\newcommand{\dspace}{\cclass{DSPACE}}
\newcommand{\nspace}{\cclass{NSPACE}}
\newcommand{\nauxpda}{\cclass{NAuxPDA}}
\newcommand{\auxpda}{\cclass{AuxPDA}}
\newcommand{\atm}{\cclass{ATM}}
\newcommand{\sat}{\cproblem{SAT}}
\newcommand{\ksat}{k\textrm{-}\cproblem{SAT}}
\newcommand{\sac}{\cclass{SAC}}
\newcommand{\nsc}{\cclass{NSC}}
\newcommand{\SC}{\cclass{SC}}
\newcommand{\nc}{\cclass{NC}}
\newcommand{\ac}{\cclass{AC}}
\newcommand{\tisp}{\cclass{TISP}}
\newcommand{\ntisp}{\cclass{NTISP}}
%
\newcommand{\logcfl}{\cclass{LOGCFL}}
\newcommand{\sacQuasi}{\cclass{SAC}_{\textsf{quasi}}}
\newcommand{\sattw}{\cproblem{SAT}_{\mathsf{tw}}}
\newcommand{\satpw}{\cproblem{SAT}_{\mathsf{pw}}}
\newcommand{\conp}{\cclass{coNP}}
%
\newcommand{\satisfiability}{\textsf{satisfiability}}
%

\newcommand{\logspace}{\cclass{LOGSPACE}}
%
%
%
%
%
%

\newenvironment{oproof}{\begin{proof}}{\renewcommand{\qedsymbol}{}\end{proof}\vspace*{-5ex}}
\newenvironment{iproof}{\begin{proof}}{\let\altsymbol\qedsymbol\renewcommand{\qedsymbol}{\altsymbol\altsymbol}%
  \end{proof}}

\newcommand{\polylog}{\operatorname{polylog}}
\newcommand{\poly}{\mathopp{poly}}
\newcommand{\eps}{\varepsilon}
\newcommand{\GR}{\textsf{GR}}
%

\newcommand{\etal}{et al.\xspace}

%
%
%
%

%

%
%
%

%
%
%

%
%
\runningtitle{Width-Parameterized SAT: Time-Space Tradeoffs}

%
\tocpdftitle{Width-Parameterized SAT: Time-Space Tradeoffs}


%
%
%
\runningauthor{E.~Allender, S.~Chen, T.~Lou, 
P.~A.~Papakonstantinou, and B.~Tang}
\copyrightauthor{Eric Allender, Shiteng Chen, Tiancheng Lou, 
Periklis A. Papakonstantinou, and Bangsheng Tang}

%
%
%
\tocpdfauthor{Eric Allender, Shiteng Chen, Tiancheng Lou,
Periklis A. Papakonstantinou, Bangsheng Tang}

\begin{document}

\begin{frontmatter}
%
%
\title{{Width-Parameterized SAT:\\ Time-Space Tradeoffs}}

%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%


%
%
%
%
\author[allender]{Eric Allender\thanks{Supported by National Science
Foundation grants CCF-0832787 and CCF-1064785.}}
\author[chen]{Shiteng Chen\thanks{Supported by National Basic Research Program
of China Grant 2011CBA00300, 2011CBA00301, and the National Natural Science
Foundation of China Grant 61033001, 61061130540, 61073174, 61250110577.}}
\author[lou]{Tiancheng Lou$^\dag$}
\author[papakonstantinou]{Periklis A. Papakonstantinou$^\dag$}
\author[tang]{Bangsheng Tang$^\dag$}

%

\begin{abstract}
%
Alekhnovich and Razborov (2002) presented an algorithm that solves $\sat$ 
on instances $\phi$ of size $n$ and tree-width $\tw(\phi)$, using time 
and space bounded by $2^{O(\tw(\phi))}n^{O(1)}$. 
Although several %
follow-up works 
appeared over the last decade, the first open question of Alekhnovich and 
Razborov remained essentially unresolved: Can one check satisfiability 
of formulas with small tree-width in polynomial space and time as above? 
We essentially resolve this question, by (1) giving a polynomial space 
algorithm with a slightly worse run-time, (2) providing a complexity-theoretic
characterization of bounded tree-width $\sat$, which strongly suggests that
no polynomial-space %
algorithm can run significantly faster, and (3) presenting
a spectrum of algorithms trading off time for space, between our \pspace\xspace
algorithm and the fastest known algorithm.

First, we give a simple algorithm that runs in polynomial space and achieves 
run-time $3^{\tw(\phi)\log n}n^{O(1)}$, which approaches the run-time of 
Alekhnovich and Razborov (2002), but has an additional $\log n$ factor 
in the exponent.  Then, we conjecture that this annoying $\log n$ factor 
is in general unavoidable.

Our negative results show our conjecture true if one believes a well-known 
complexity assumption, which is the $\SC\neq \nc$ conjecture and its scaled 
variants. Technically, we base our result on the following lemma. 
For arbitrary $k$, $\sat$ of tree-width $\log^k n$ is complete for the 
class of problems computed by circuits of logarithmic depth, semi-unbounded 
fan-in and size $2^{O(\log^k n)}$ ($\sac^1$ when $k=1$).
Problems in this class can be solved  simultaneously in
time-space $(2^{O(\log^{k+1}n)}, O(\log^{k+1}n))$, 
and also in ($2^{O(\log^k n)}$, $2^{O(\log^k n)}$).
Then, we show that our conjecture (for $\sat$ instances with poly-log 
tree-width) is equivalent to the 
question of whether the small-space %
simulation of semi-unbounded circuit 
classes can be sped up without 
incurring a large space penalty. This is a recasting of the conjecture
that $\sac^1$ (and even its subclass $\NL$) is not contained in $\SC$.

Although we cannot hope for an improvement asymptotically in the exponent 
of time and space, we introduce a new algorithmic technique which trades
constants in the exponents: 
for each $\eps$ with $0< \eps <1$, we give an algorithm in time-space 
\[
\big( 3^{1.441(1-\eps)\tw(\phi)\log{|\phi|}}|\phi|^{O(1)},\;
2^{2\eps\tw(\phi)}|\phi|^{O(1)}  \big)\,.
\] 
We systematically study the limitations of our technique for trading off 
time and space, and we show that our bounds are the best achievable using 
this technique.  
\end{abstract}


%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%

\tocacm{F.1.3, F.2.2}
\tocams{68Q15, 68Q25}

%
%
%
%
%
%
%
%
%
%
\tockeywords{complexity theory, algorithms, complexity classes, circuit complexity, parameterized complexity, nondeterminism, CNF-DNF formulas, Boolean formulas, completeness, SAT, time-space tradeoff, treewidth, pathwidth}


\end{frontmatter}




%
%


%

\section{Introduction}	\label{sec:intro}
%
%

$\sat$ is the prototypical $\np$-complete problem. In the real-world $\sat$ instances tend to have 
structure. Also, in practice $\sat$-solvers abort due to lack of memory. 
In this paper we provide conclusive, asymptotically tight answers regarding time-space tradeoffs for $\sat$ 
instances that are structured, where this structure is quantified by \emph{tree-width}.\footnote{A formal definition of tree-width can be found in 
\expref{Section}{sec:preliminary}, an informal exposition is found earlier in \expref{Section}{sec:related}.}

This restriction of $\sat$ was studied by Alekhnovitch and Razborov~\cite{alekhnovich2002satisfiability} 
(for references prior to this see within), 
who gave algorithms that work in time $2^{O(\tw(\phi))}|\phi|^{O(1)}$ and in space 
$2^{O(\tw(\phi))}|\phi|^{O(1)}$, where $\tw(\phi)$ is the tree-width of a CNF 
formula $\phi$, and $|\phi|=n+m$ where $n$ and $m$  are the number of
variables and clauses, respectively. The authors of~\cite{alekhnovich2002satisfiability}
state their results in terms of the branch-width of the formula, which is within a 
constant factor of the tree-width. They conclude:

\begin{quote}
``The first important problem is to overcome the main difficulty of the practical
implementation which is the huge amount of space used by width-based 
algorithms. \ldots
Thus we ask if one can do anything intelligent in polynomial space to check 
satisfiability of formulas with small branch-width?''
\end{quote}
The question raised by Alekhnovich and Razborov is a major issue in practical
$\sat$-solving.   
Modulo complexity assumptions we fully answer this question.

\subsection{Our contribution and techniques}

We devise a simple space-efficient algorithm for $\sat$ instances in 
CNF, which runs in time
\[
3^{\tw(\phi)\log{|\phi|}}|\phi|^{O(1)}
\]
and space
\[
|\phi|^{O(1)}\,.
\]
This is the first algorithm with running time exponential
in the tree-width of the incidence graph (unlike~\cite{BDP} which is just on the primal graph)
of arbitrary CNF instances (unlike~\cite{GP08} which is just for $k$-CNFs), 
that runs in polynomial space. 
Compared to the question of~\cite{alekhnovich2002satisfiability} this algorithm suffers
a $\log|\phi|$ factor in the exponent of the running time. Our work revolves around this 
logarithmic factor. First, we conjecture that it cannot be removed:

\begin{conjecture}\label{conj:mainconj}
Let $\mathcal{A}$ be an algorithm for $\sat$ that runs in time $2^{\tw(\phi)
\delta(|\phi|)}|\phi|^{O(1)}$.
Consider CNF formulas where $\tw(\phi)=O(|\phi|^{1-\epsilon})$, for some 
fixed $\epsilon<1$.
If $\delta(\phi)=o(\log |\phi|)$ then $\mathcal{A}$ uses space $2^{\Omega(\tw(\phi))}$.
\end{conjecture}

Second, we show that the above conjecture is equivalent to a widely-believed 
computational complexity assumption (scaled for a wider range of parameters). 
That is, we offer a complexity-theoretic connection 
that supports this conjecture. 
This computational complexity conjecture comes under the cryptic statement
$\nc\not\subseteq \SC$.
This is well-known to complexity theorists, and also of
immense practical interest.
$\SC$ is the class of problems
that can be decided by algorithms that work simultaneously in poly-logarithmic space
and polynomial time (\ie, efficient time and efficient space computation). $\nc$ is the class of 
problems that can be decided  by circuits simultaneously of polynomial size and 
poly-logarithmic depth (\ie, parallel computation which uses a small number of processors
and small parallel time). There is an, almost exact, correspondence between algorithm space and circuit depth 
(\eg, given an algorithm that uses poly-logarithmic space we can construct a parallel algorithm that runs in 
poly-logarithmic parallel time) and between algorithm time and circuit size. 
These correspondences are believed to break down when we \emph{simultaneously} bound ``time and space''
and simultaneously bound ``size and depth.'' That is, $\nc\not\subseteq \SC$ means that in general we cannot
trade efficient \#parallel processors-parallel time computation for efficient sequential time-space computation. 
Details and additional intuition are given in \expref{Section}{sec:complexity}.

Semi-unbounded combinatorial circuits play an important role in this work. 
A semi-unbounded circuit ($\sac$) has AND gates of bounded fan-in, OR gates of unbounded fan-in,
and all the negations at the input level. Despite their exotic nature these circuits have essential
differences from bounded and unbounded fan-in circuits; see \expref{Section}{subsec:primer_SAC} for a discussion. 

In \expref{Section}{sec:complexity} we show:

\medskip
\noindent
{\bf \expref{Theorem}{thm:sat_pw}.} $\sat$ of a given tree decomposition
of width $\log^k n$ is complete for the class
\[
\sacQuasi^k:=\sac\bigl(O(\log n), 2^{O(\log^k n)}\bigr)\,,
\] 
\ie, semi-unbounded fan-in circuits of $O(\log n)$-depth, and $2^{O(\log^k n)}$-size.
\medskip
 
This is shown through a generic reduction in the spirit of~\cite{gottlob2001complexity}. 
We observe that $\nsc^k$, defined as $\nsc^k=\ntisp(n^{O(1)}, O(\log^k n) )$ is contained
in $\sacQuasi^k$ which is in turn contained in $\nsc^{k+1}$,
where $\ntisp$ denotes the set of problems decidable by non-deterministic
Turing Machines that are simultaneously TIme-SPace bounded, and we
show:

\medskip
\noindent
{\bf \expref{Theorem}{thm:sat_tw}.} $\sat$ of a given path decomposition
of width $\log^k n$ is complete for $\nsc^{k}$,
\medskip

Note that the $\nsc$ levels are direct space-scaled analogs of $\NL$ and these
$\sac$ classes are direct size-scaled analogs of $\sac^1$. Therefore,  
separating the complexity of $\sat$ parameterized by path-width and tree-width is
equivalent to separating these classes, and hence, by padding, separating $\NL$ and $\logcfl=\sac^1$.
More importantly, putting these developments together we conclude that our conjecture
implies $\nc\neq\SC$, and in fact as the tree-width ranges over different functions of the input length
our conjecture is shown to be equivalent to a resource-scaled analog of $\nc\neq\SC$.
Somewhat less rigorously:
\begin{quote}
\emph{Shrinking down the space, even by just a little, in a reasonably fast algorithm for $\sat$ of bounded tree-width,
is the same as saying
that every highly parallelizable problem can be sequentially computed simultaneously in small time and space.}
\end{quote}

Assuming for now that \expref{Conjecture}{conj:mainconj} holds, 
it makes sense to devise algorithms that approach these limits.  
This is the topic of \expref{Section}{sec:alg}, which 
constitutes the more technically involved part of this work, 
though the practical significance of these algorithms is debatable. 

We use our space-efficient algorithm, together with a time-efficient dynamic
programming algorithm (essentially the algorithm of~\cite{SS10}), as the
``end-points''  for a spectrum of algorithms that trade off time and space
complexity between these two extremes.  But there is a catch.
If we combine the time-efficient dynamic programming algorithm 
and our recursive algorithm in the obvious way, then we gain the worst of both worlds.
Here ``obvious'' means that we discretize the space of truth assignments
during the execution of the recursive algorithm and combine using dynamic
programming.
Instead, we introduce an implicit family of proof systems.
We use two free parameters to specify an algorithm in this family.
One parameter is an integer which is at least $2$.
This controls the ``complexity'' of the rules
applied, for performing an unbalanced type of recursion of some sort.
The larger this parameter is, the smaller the running time is and the more 
space is used.
The second parameter is a real number in $(0,1)$ that
controls the discretization of the truth assignment space.
This family of algorithms is presented in \expref{Section}{sec:alg}, and in its full generality in 
\expref{Section}{sec:alg2}. In the same sections we show that all of the infinitely-many pairs of values are of interest, 
depending on the different time-space bounds one may want to achieve.

\begin{remark}
Throughout this paper we assume that the tree (or path) decompositions 
are given in the input. 
To the best of our knowledge, the same is true in all other works in width-parameterized $\sat$. 
\end{remark}

\subsection{Related work}\label{sec:related}
Tree-width is a popular graph parameter introduced by Robertson and Seymour~\cite{robertson1983graph,robertson1986graph}.
The smaller the tree-width of a graph, the more the graph looks like a tree in some topological sense;
for a connected graph of $n$ vertices tree-width $1$ means that the graph is a tree, whereas tree-width $n-1$ means that it is
the complete graph.
Several hard computational problems on general graphs become computationally easier when the input graph
is of small tree-width; see, \eg,~\cite{bodlaender1993tourist} for a survey.

For $\sat$ instances the tree-width of a CNF formula is the tree-width of its associated graph (\eg, incidence graph,
primal graph, or intersection graph). Among those graphs, the most general one is the incidence graph (a bipartite graph
where one side has variable-nodes and the other clause-nodes). In some sense, the tree-width value on the incidence graph
lower bounds the tree-width value of the rest~\cite{szeider03}. 
In particular, the tree-width of the incidence graph of a CNF formula can be arbitrarily smaller 
than the tree-width of the CNF-formula graphs that were studied by Bacchus et al.~\cite{BDP}.
There is a vast literature (too large to concisely cite here) in empirical and theoretical studies in various 
width-parameterizations of $\sat$---we only cite some of the most relevant ones below. 


\paragraph{Algorithms for width-parameterized $\sat$.}
Prior to our work,~\cite{BDP,GP08} addressed the question of Alekhnovich and Razborov.
In~\cite{GP08} the authors gave a combinatorially non-explicit algorithm only for the $\ksat$ problem, where $k$ is constant, 
where the algorithm runs in time $2^{O(\tw(\phi)\log|\phi|)}$ and space $|\phi|^{O(1)}$, when $\tw(\phi)=\Omega(\log |\phi|)$.
The deficiencies of~\cite{GP08} (which we overcome in our current paper) are not only that 
their algorithm works only for $\ksat$, but also 
that the constant in the exponent of the running time cannot be bounded in any
easy way due to the non-explicitness of the argument presented there.
%
%
%
Bacchus et al.~\cite{BDP} present 
%
a polynomial-space DPLL algorithm with running time exponential in the tree-width of the 
\emph{primal graph} of a formula, hence their $\sat$ algorithm is strictly weaker than ours 
(although they also present algorithms for $\#\sat$ and similar problems).

There have been a number of follow-ups improving the running time of the
Alekhnovich and Razborov algorithm~\cite{alekhnovich2002satisfiability},  
considering different width-parameters: 
Fischer \etal~\cite{Fischer08} give algorithms for $\sat$ (and a somewhat generalized version of $\#\sat$) 
parameterized by tree-width and clique-width. Their tree-width algorithm
matches the running time and space of an algorithm of Samer and Szeider~\cite{SS10}, which we make use of later in this paper as a
time-efficient algorithm,
running in time-space
\[\big(2^{2\tw(\phi)}|\phi|^{O(1)},\;
2^{\tw(\phi)}|\phi|^{O(1)}\big)\,.
\] 
Also, we remark that algorithms (\eg, for graph problems) which replace the tree-width parameter $\tw$ 
in the exponent by a $\tw^2$ and at the same time reducing the space to polynomial (see \eg,~\cite{LMS11b}) are 
strictly worse than our algorithms (and in particular fail to reach our target lower bound for the Alekhnovitch-Razborov question). 
In particular, unlike the classical parameterized complexity approach, the interesting part of our treatment
(and in particular our complexity results) are for values of tree-width that are related to the input length,
and in fact $\Omega(\log n)$. 

\paragraph{Improving constants, previous work, and what's different.}
Improving the constant in the base of an exponential time algorithm is a well-established goal in
the field of exact computation for $\np$-hard problems; see \eg,~\cite{fomin.kratsch,woeginger2003exact} for an overview.
In particular, for $\ksat$ there is a line of work in algorithms that run in time $\alpha^n$ for $\alpha<2$; \eg,~\cite{MS11,paturi1998improved,schoning1999probabilistic,woeginger2003exact}.
An issue somewhat superficially related to our conjecture deals with 
time-space tradeoffs for algorithms
for $\np$-hard permutation problems,
as discussed for example in~\cite{bodlaender-formin-etal} and the references 
within (in particular~\cite{KP10}).
However, there is no easy way to adapt these techniques in our setting,
and if \expref{Conjecture}{conj:mainconj} is true, they cannot really be applied 
at all.
A key property of these previous algorithms is that as smaller subproblems 
are considered, 
the parameter \emph{number of nodes} becomes smaller.
There is no obvious way to achieve this when the parameter is the \emph{width} of the formula.

Finally, to the best of our knowledge our work is the first to address the 
issue of smooth time-space tradeoffs for width-parameterized $\sat$. Prior to our work there are others 
which solely discuss lower bounds on the running time; \eg, for graph problems 
(and under the very strong ETH assumption~\cite{IPZ01})~\cite{LMS11}. Another kind of tradeoff 
(between size of the separator and the sharpness) for graph problems was discussed in~\cite{FLGS10}.
 We should also mention that in two excellent works on constraint satisfaction problems Grohe~\cite{grohe} 
(assuming that $\cclass{FPT}\neq\cclass{W}[1]$) and Marx~\cite{marx2010can} 
(assuming ETH) essentially show that the running time of the known width-based algorithms is optimal. 


\paragraph{Hardness results and complexity characterizations.}
Every problem in $\np$ can be seen as a problem
where accepting instances can be verified in logarithmic space (\ie, we can settle for less
than polynomial time in the verification).
$\sat$ of bounded path-width has been shown~\cite{papakonstantinou2009note} complete 
for the class of problems that can be decided by a logarithmic space machine which has ``streaming access''
to the tape containing the witness; \ie, scanning the witness tape
at most a given number of times.
In particular,  $O(r(|\phi|))$ passes correspond to $\sat$ instances with given path-decompositions 
of width $r(|\phi|)\log|\phi|$. 
Specifically, deciding formulas 
with given path decompositions of width $O(\log |\phi|)$ is complete for $\NL$,
and~\cite{papakonstantinou2009note} asks whether the complexity of $\sat$ instances when the parameter is
tree-width $O(\log |\phi|)$ is more difficult. In this paper we 
answer this question affirmatively, unless\footnote{
It is conjectured, \eg~\cite{cook85}, that $\sac^1\neq\NL$. Note that $\sac^1$ is also known as $\logcfl$.}
$\NL=\sac^1$. 
Furthermore, we show an exact correspondence of these ``streaming verification'' classes with the levels of the 
known $\nsc$ hierarchy. 
Our new characterization through semi-unbounded circuits is of independent interest,
and seems more natural than the characterizations presented in~\cite{AADVW00}. 




\paragraph{Relation to Propositional Proof Complexity.}
%
Our work opens new, exciting directions for Propositional Proof Complexity. 
One way to make progress towards validating \expref{Conjecture}{conj:mainconj} is to
restrict attention to specific types of algorithms. 
The study of restricted proof systems is one such choice. In fact, Beame, Beck, and Impagliazzo~\cite{BBI}
very recently made progress towards \emph{exactly} validating our question. 
In particular, they proved a Resolution 
Refutation size-space tradeoff, which implies that there exists a family of formulas $\phi$ of 
tree-width $\tw(\phi)$ where for every $k>0$ every resolution refutation of size $n^k$ requires space
\[
2^{\tw(\phi)\frac{\log\log n}{\log\log\log n}}\,.
\]
This very significant development is the first super-polynomial
lower bound of this sort, and through our work it can be interpreted as validating the 
$\sac^1\not\subseteq \SC$ conjecture, at least for a class of restricted algorithms.
This is a new direction; lower bounds in proof complexity are clearly 
connected to the $\np\neq\conp$ conjecture~\cite{CR}, but have not previously
seemed to have a bearing on the $\SC\neq\nc$ question.


\section{Preliminaries}	\label{sec:preliminary}
%

%

We introduce notation, terminology, and conventions used throughout the paper.

\subsection{Notation}
All logarithms are of base $2$, and all propositional formulas are in Conjunctive Normal Form (CNF).
$\sat$ is the decision problem where given an arbitrary CNF formula we want to decide if
it is satisfiable. We let $\ksat$ denote the restriction of $\sat$ to CNFs where each clause has at most
$k$ literals. For a formula $\phi$, $m$ denotes the number of clauses, $n$ the number of variables,
and $C_i$ and $x_j$ stand for the $i$-th clause and $j$-th variable respectively.
For convenience we write $|\phi|=m+n$. When there is no confusion (\eg, when defining complexity classes) 
$n$ is used to denote the input length. 



\subsection{Tree-width}

\begin{definition}
Let $G=(V,E)$ be an undirected graph. A \emph{tree decomposition} of
$G$ is a tuple $(\mathcal{T},X)$, where $\mathcal{T}=(W,F)$ is a tree,
and $X=\{X_1,\cdots,X_{|W|}\}$ where $X_i\subseteq V$ such that
\begin{enumerate}[(1)]
\item $\bigcup_{i=1}^{|W|}X_i=V$,
\item $\forall (i,j)\in E$, $\exists t\in W$, such that $i, j\in X_t$,
\item $\forall v$, the set $\{t:v\in X_t\}$ forms a subtree of $\mathcal{T}$.
\end{enumerate}
Each of $X_i$ is called a \emph{bag}, the width of $(T,X)$ is defined as $\max_{t\in W}|X_t|-1$, and the \emph{tree-width} $\tw(G)$ of graph $G$ is defined as the minimum width over all possible tree decompositions.
\end{definition}

When the tree decomposition $\mathcal{T}=(W,F)$ is restricted to a path, the decomposition is called a \emph{path decomposition}, and the specific tree-width is called the path-width $\pw(G)$. The following inequality holds (\eg,~\cite{bodlaender1998partial})
\begin{eqnarray}
\tw(G)\le\pw(G)\le O\left(\log{|V|}\cdot\tw(G)\right)\,.\label{formula:pw_tw}
\end{eqnarray}

\begin{definition}
The \emph{incidence graph} $G_{\phi}$ of a $\sat$ instance $\phi$ is a bipartite graph, where in one side of the bipartization each node is associated
with a distinct variable, and in the other each node is associated with a clause. There is an edge between a clause-node and a
variable-node if and only if the variable appears in a literal of the clause. The tree-width of a formula $\phi$ is the tree-width
of its incidence graph, $\tw(\phi)=\tw(G_{\phi})$. \emph{When it is clear from the context we may abuse notation and write $\tw(\phi)$
to denote the width of a given decomposition of $G_\phi$}.
\end{definition}

We assume that a tree decomposition of the incidence graph of $\phi$ is given as input along with $\phi$. For convenience, we assume without loss of generality that the input tree decompositions $((W,F),X)$ have the following two properties.
\begin{enumerate}[(1)]
\item $|W|=O(\tw(\phi)\cdot|V|)=O(\tw(\phi)|\phi|)$, and
%
\item the tree $\mathcal{T}=(W,F)$ has bounded degree $3$.
\end{enumerate}
We call a tree decomposition \emph{nice} if it satisfies the two properties above. A tree decomposition can be converted to a nice one in
linear time (see \eg,~\cite{kloks1994treewidth,bodlaender1998partial}). 
The maximal degree in the tree decomposition is denoted by $d$.
By the property above, $d\le 3$. If the input is given with a \emph{path} decomposition, then $d \leq 2$.

\begin{remark}
We present our results with the parameter $d$. One may replace $d$ by $2$ or $3$ when the structure of the input decomposition is known to be a path or a (nice) tree.
\end{remark}



\subsection{Assignments}
\label{subsec:assignments}
%
We introduce terminology and notation to talk about truth assignments on bags. Let $X$ be a bag in the tree decomposition, $\mathcal{V}$ be the variables and $\mathcal{C}$ be the clauses in $X$. Also, $n_\mathcal{V}=|\mathcal{V}|$ and $m_\mathcal{C}=|\mathcal{C}|$. An \emph{assignment} $R_X$ for $X$ is a binary vector of length $n_\mathcal{V}+m_\mathcal{C}$. The first $n_V$ bits indicate the truth values of the corresponding variables. Note that the term ``assignment'' does not correspond only to a ``truth assignment'' on the variables in $X$. It is an assignment of bit values both to variables and to clauses.

What values the last $m_{\cal C}$ bits have is a subtle issue explained in 
\expref{Section}{sec:alg}. For the dynamic programming algorithm things are 
pretty clear. However, for the space-efficient and trade-off algorithms, things become more subtle. Intuitively, a bit corresponding to a clause $C$ is $1$ if we ``have decided'' to eventually satisfy this clause (this has to do with where we are in the execution of the algorithm). Such a decision is different for different algorithms, but we use the same data-structure. 

Actually, the most straightforward way of defining the clause bits is to let it denote whether the corresponding clause ``is'' satisfied. To ensure that a clause is satisfied in one of the branches in the tree decomposition, we need to enumerate all $2^d-1$ combinations of branches on which the clause is satisfied. However, if one is interested in only the satisfiability problem (and not, \eg, in $\#\sat$) we observe that $d$ combinations suffice.


\section{A complexity-theoretic characterization} \label{sec:complexity}
%

%

We show that (i) our \expref{Conjecture}{conj:mainconj} is equivalent to a widely believed complexity 
assumption (and its scaled analogs), and 
(ii) under a different well-known complexity assumption
($\NL \subsetneq \logcfl$), for the same width 
parameter $w(|\phi|)$
$\sat$ of tree-width $O(w(|\phi|))$ cannot be efficiently reduced to $\sat$ of path-width $O(w(|\phi|))$.
Both of these results follow by first proving that $\sat$ parameterized by path- and tree-width 
is complete for natural complexity classes. 
To obtain these results, we heavily rely on properties of semi-unbounded combinatorial circuits. 
In \expref{Section}{subsec:primer_SAC} we give a primer with basic intuition about these circuits.
Also, based on properties of these circuits and on the relation between path-width and tree-width 
in equation~\eqref{eq:characterization} in \expref{Section}{subsec:characterization}, we provide a new 
characterization of $\nsc$. 


%
%
%

\subsection{A primer on semi-unbounded fan-in circuits} 	\label{subsec:primer_SAC}
%
The statements of the lower bounds do not explicitly refer to semi-unbounded families of circuits, 
but we use them inside the arguments. 
A circuit is \emph{semi-unbounded} when it has unbounded fan-in $\textsf{OR}$ gates, bounded 
fan-in $\textsf{AND}$ gates, 
and all the negations are at the input level. The class of problems that can be decided by such circuits
of depth $O(\log^i n)$ and polynomial size is denoted by $\sac^i$. Clearly, $\nc^i\subseteq \sac^i \subseteq \ac^i$,
where $\nc$ and $\ac$ denote the complexity classes characterized by the same parameters with bounded fan-in and 
unbounded fan-in families of circuits, respectively. There is also the issue of uniformity; 
we provide the necessary background regarding circuit uniformity in the next sub-section. 
For the moment, the reader should make use of
an informal uniformity assumption, meaning merely that there is an efficient algorithm
describing how to construct the circuits for inputs of size $n$.

\paragraph{What is special in $\sac$ circuits?} 
Suppose that you are given oracle access to the description of an \emph{unbounded} circuit $C$ 
(with all negation gates on the input level) and an input $x$, 
and you want to verify recursively that $C(x)= 1$.  The standard algorithm would be to start at the output 
gate and execute the following
recursive algorithm: if the current gate $g$ is an OR gate, nondeterministically pick a gate $h$ that feeds 
into $g$ and verify that $h$
evaluates to 1; if the current gate $g$ is an AND gate with $h_1, \ldots, h_m$ feeding into it, recursively 
verify that each of the $h_i$
evaluates to 1.  An accepting run of this algorithm corresponds to a (possibly huge) tree, called 
a ``proof tree''~\cite{venkateswaran1987properties}; 
if the circuit $C$ has bounded fan-in (or even
semi-unbounded fan-in), then the size of this tree is bounded by $2^{\rm depth}$.  In the bounded 
fan-in case, restricting the depth of $C$
automatically implies restricting the size of $C$; in the semi-unbounded fan-in case this is not true.  
The important aspect of semi-unbounded
fan-in circuits that we will utilize, is that the proof tree can be much smaller than the circuit 
(unlike the bounded-fan-in case), and has 
size exponential in the depth (unlike the unbounded-fan-in case).



\paragraph{An observation on uniformity.}
%
Consider a family of semi-unbounded circuits of size $2^{n^{O(1)}}$ and depth $O(\log n)$ that
is polynomial time uniform, in the sense that,
given the names of two gates $g$ and $h$, one can determine in time 
polynomial in $n$ whether there is an edge from $g$ to $h$, and what kind of
gates $g$ and $h$ are. (Note that $n^{O(1)}$ bits are required, merely to write 
down the name of one of the gates.) Then, for an input $x$, $|x|=n$, the 
problem of evaluating the membership of the family $C_n(x)$ is in $\np$. 
That is, given $x$ we guess a proof as described above and then verify that 
it is a valid proof. Clearly, every problem $L\in\np$ can be computed by such 
a circuit since in $\log n$ depth we can verify that a given witness $y$
is an encoding of a valid accepting computation path on input $x$, and hence
we obtain a circuit for $L\cap \{0,1\}^n$ by putting a big \textsf{OR} gate 
as the output gate, computing the disjunction, over all potential witnesses
$y$, of the $O(\log n)$ depth circuit testing if $y$ is a witness for the
input $x$). In other words, $\np$ is precisely the class of 
problems computed by uniform semi-unbounded circuits of size
$2^{n^{O(1)}}$. Observe that if we do 
not insist on the uniformity, then an arbitrary function can be computed by 
a $2^{O(n)}$-size and $O(\log n)$-depth semi-unbounded (non-uniform) circuit.



\paragraph{Relations of $\sac$ circuits to other models of computation.}
%
Semi-unbounded fan-in circuits are intimately related to Alternating Turing Machines ($\atm$s) and 
to Nondeterministic Auxiliary PushDown Automata ($\nauxpda$s). We provide definitions later on; 
for a more detailed treatment see, \eg,~\cite{ruzzo1980tree}. For the moment let us say that an $\atm$ 
and a $\nauxpda$ are basically the same thing. Also, recall that an $\atm$ is a nondeterministic 
Turing Machine with two kinds of nondeterministic states: existential and universal. An existential state 
is accepting if and only if at least one successor configuration is accepting, whereas a universal state 
is accepting if and only if each successor configuration is accepting. Although it requires a bit of work 
to show equivalence~\cite{venkateswaran1987properties} it should come at no surprise that proofs 
for $\sac$ circuits are related to $\atm$ computations. 



%
%
%

\subsection{Complexity theory notation and some preliminaries}
%
$\nsc$ is the nondeterministic analog of $\SC$, the class of languages decidable simultaneously
in polynomial time and poly-logarithmic space. Define
$\nsc^k:=\ntisp\big(n^{O(1)}, O(\log^k n)\big)$. 
It is widely conjectured that $\SC\neq\nc$. 
Here is a stronger intuitive form of this conjecture.

\begin{conjecture}
The $\NL$-complete graph reachability problem\footnote{Given
a directed graph $G=(V,E)$ and two designated vertices $s,t\in V$, is $t$ reachable from $s$?}
cannot \emph{simultaneously} be solved deterministically in sub-polynomial 
space and polynomial time.  That is, depth-first search 
cannot be simulated quickly in small
space, and hence $\NL \not\subseteq\tisp(n^{O(1)}, n^{o(1)})$.
This implies the weaker conjecture 
$\sac^1\not\subseteq\tisp(n^{O(1)}, n^{o(1)})$.
\end{conjecture}

We denote by $\sattw(w(|\phi|))$ the problem of deciding $\sat$ of a given CNF formula together with a
tree decomposition of width $w(|\phi|)$. Similarly, for path-width we use the notation $\satpw(w(|\phi|))$. 
\cite{papakonstantinou2009note} shows that $\satpw(w(|\phi|))$ is complete for the class $\NL[{w(|\phi|)}/{\log|\phi|}]$, 
characterized by log-space bounded Turing Machines augmented with a polynomially long 
read-only, nondeterministic tape on which they make $O({w(|\phi|)}/{\log|\phi|})$ passes. 

We use the notation $\sac(\textsf{depth},\textsf{size})$.  We follow standard
conventions when defining levels of the $\nc$ hierarchy, by defining
$\sac^k:=\sac(O(\log^k n), n^{O(1)})$.  However, in this paper a different
parameterization will be of equal importance: by restricting the depth of
semi-unbounded fan-in circuits to be $O(\log n)$, and allowing the size to be
quasipolynomial, we obtain subclasses of $\np$ denoted by
\[
\sacQuasi^k:=\sac\bigl(O(\log n), 2^{O(\log^k n)}\bigr)\,.
\]
The study of $\sac$ circuits, 
and the various classes $\sac^i$ has received considerable attention, 
\eg,~\cite{BCDRT,venkateswaran1987properties}. The $\sacQuasi^k$ classes 
(very shallow quasi-polynomial size circuits) are introduced in this paper; 
they characterize the $\nsc$ hierarchy (equation~\eqref{eq:characterization}). 
For these families of circuits we use
%
%
%
\cclass{DLogTime}-uniformity~\cite{bis}.
%
This means that the \emph{direct connection language} for the circuit
family can be recognized in linear time.  The direct connection
language takes inputs of the form $\langle n,i,d,j,t\rangle$ such that
$d>0$ and the $d$th input of the gate $i$ in the circuit for inputs of
length $n$ is of type $t(\in\{\textsf{AND}, \textsf{OR}, 0, 1\})$ and
has index $j$, or else $d=0$ and gate $i$ is of type $t$.  Since the
string $\langle n,i,d,j,t\rangle$ has length logarithmic in the size
of the circuit for inputs of length $n$, it follows that, for
$\sacQuasi^k$ circuits, questions about connectivity in the circuits
for length $n$ can be answered in time $O(\log^k n)$.

Simultaneously depth-size bounded semi-unbounded circuits are intimately 
related to space-time bounded $\nauxpda$s. A $\nauxpda$ is a nondeterministic 
space-bounded Turing Machine equipped with an unbounded stack 
(see~\cite{cook1971characterizations} for a precise definition). 
$\nauxpda(s(n), t(n))$ is the class of languages decidable by a $\nauxpda$ in 
space $O(s(n))$ and time $O(t(n))$.  Although general Turing machine \emph{time}
is related to circuit \emph{size} while circuit \emph{depth} is related to 
\emph{space}, on $\nauxpda$s the correspondence is reversed; simultaneous
bounds on circuit size and depth correspond to bounds on space and time,
respectively.  Generalizing the arguments 
in~\cite{ruzzo1980tree} and~\cite{venkateswaran1987properties} we obtain:

\begin{lemma} \label{lem:sac-nauxpda}
$\sacQuasi^k=\nauxpda\bigl(O(\log^k n), n^{O(1)}\bigr)$, for $O(\log^k n)$ time uniform $\sac$ circuits. 
\end{lemma}

\begin{proof}
The proof of $\sacQuasi^k\supseteq\nauxpda(O(\log^k n),n^{O(1)})$ can be shown
by following the proof for the special case $k=1$ (\ie,
$\nauxpda(O(\log{n}), n^{O(1)})=\sac(O(\log{n}), n^{O(1)})$)~\cite{ruzzo1980tree,venkateswaran1987properties}.  (See also~\cite{vollmer}.)
However, in the proof
of \expref{Lemma}{lemma:sattw_hard_for_sac} we will need to assume that the
uniform $\sacQuasi^k$ have certain properties, and thus we follow a different
outline here, to establish that those properties hold.

Ruzzo~\cite[Theorem 1 \& Corollary 7]{ruzzo1980tree} showed that any language 
in $\nauxpda(O(\log^k n),n^{O(1)})$ is accepted by a $\nauxpda$ respecting these
same resource bounds, where additionally the height of the pushdown is
$O(\log^{k+1}n)$ (and pushes and pops consist of moving strings of length 
$O(\log^k n)$ to and from the stack---hence it is useful to think of the
stack as having height $\log n$, over ``symbols'' of length $O(\log^k n)$).
It is easy to see that such a machine can also be assumed to be somewhat ``oblivious,'' in the sense
that the positions of the worktape and input heads at time $t$ are the same
for all inputs of length $n$.  Rossmanith and Niedermeier subsequently
improved on this, to show that the $\nauxpda$ can be assumed to be completely
oblivious, in the sense that the sequences of pushes and pops are also the
same for all inputs of length $n$~\cite[Theorem 28]{nie.ros}.  (Rossmanith
and Niedermeier state their theorems in terms of machines with a logarithmic
worktape bound, but their proof works also for larger space bounds, as long as
the time is polynomial.)  In particular, the pushes and pops follow a very
regular pattern, so that the computation is divided into phases corresponding
to the height of the stack.  The computation starts and ends with stack
height zero, and precisely half-way through the computation, the stack height
is also zero.  Call these three configurations $C_0, D_0$, and $E_0$.
The computation from $C_0$ to $D_0$ and from $D_0$ to $E_0$ all takes place
with a stack height of at least 1 ``symbol'' (where the stack ``symbols''
are of $O(\log^kn)$ bits each); these are the two ``phases'' with height 1.
In general, there are $2^i$ phases with height $i$, for each 
$i \leq i_{\max} = O(\log n)$.  Each such phase (for $i<i_{\max}$) has some start
configuration $C_i$ and end configuration $E_i$ that take place at times
that depend only on the input length $n$, and there is a configuration $D_i$
that also has stack height $i$, such that the computations between
$C_i$ and $D_i$ and between $D_i$ and $E_i$ have exactly the same length and
are both phases with stack height $i+1$.  (The phases at height $i_{\max}$
start in a configuration $C$ that has a number $j\leq n$ recorded in it,
and ends in a configuration that records the $j$-th input symbol; no stack
manipulation occurs in such a phase.)

Thus in order to show that
\[
\nauxpda\bigl(O(\log^k n),n^{O(1)}\bigr)\subseteq\sacQuasi^k\,,
\]
it suffices to build circuits to simulate oblivious machines that have
this very restrictive computation pattern.  The output gate will check if
the height zero phase starts with the initial configuration $C_0$ and ends with
the accepting configuration $E_0$; it is an \textsf{OR} gate, connected to
gates labeled with triples $(C_0, D_0, E_0)$ for all $D_0$, to see if there is
a computation from $C_0$ to $E_0$ passing through $D_0$.  In general, gates
labeled $(C_i, D_i, E_i)$ (or $(C_i, D_i, E_i,\gamma)$) 
where $C_i$, $D_i$, and $E_i$ encode the worktape
contents and input head positions (but not the stack contents) for some
phase with stack height $i$ (and $\gamma$ is a stack symbol of length 
$\log^k n$) are \textsf{AND} gates, testing whether there are
computations from $C_i$ to $D_i$ and from $D_i$ to $E_i$, respectively.
The children of these \textsf{AND} gates, corresponding to some
computation between stack height $i$ configurations $A$ and $B$, are
\textsf{OR} gates over all $(C_{i+1},D_{i+1},E_{i+1},\gamma)$ such that:
\begin{itemize}
\item there is a move from $A$ to $C_{i+1}$ pushing $\gamma$, and
%
\item there is a move from $E_{i+1}$ to $B$ popping $\gamma$.
\end{itemize}
(If $i+1=i_{\max}$, then instead of $(C_{i+1},D_{i+1},E_{i+1},\gamma)$, the gates
have the format $(C_{i+1},E_{i+1},\gamma)$, and these gates are (possibly 
negated) input gates, recording whether the given input symbol is consistent
with a transition from $C_{i+1}$ to $E_{i+1}$.)

It should be clear that the circuit directly simulates the $\nauxpda$.
For more details about the uniformity of the circuits, we refer the reader
to~\cite{nie.ros,venkateswaran1987properties,vollmer}.


Now we prove the other direction: 
\[
\nauxpda\bigl(O(\log^k{n}), n^{O(1)}\bigr)\supseteq\sac\bigl(O(\log{n}),
2^{O(\log^k{n})}\bigr)\,.
\]
Let $L$ have $\sac(O(\log{n}), 2^{O(\log^k{n})})$ circuits.  A $\nauxpda$ 
accepts $L$ as follows.  On input $x$, compute the name of the output gate of
the circuit (call it $g$), and write $g$ on the worktape.  Start the routine
$\operatorname{EVAL}(g)$, described below.

\begin{algorithm}
\caption{$\operatorname{EVAL}(g)$}
\label{alg:eval}
\begin{algorithmic}[1]
\If {$g$ is a (negated) input gate connected to input bit $x_i$}
\State accept iff $x_i$ is 1 (0, respectively)
\EndIf
\If {$g$ is an \textsf{OR} gate}
\State nondeterministically guess a gate name $h$ and check that
$h\rightarrow g$ is an edge in the circuit
\State \Return $\operatorname{EVAL}(h)$
\EndIf

\If {$g$ is an \textsf{AND} gate}
\State compute the gates $h_1$ and $h_2$ that feed into $g$  
\State push $h_2$ onto the stack and call $\operatorname{EVAL}(h_1)$
\If {this evaluates to 0}
\State {halt and reject}
\Else
\State \Return $\operatorname{EVAL}(h_2)$
\EndIf
\EndIf
\end{algorithmic}
\end{algorithm}


The run-time required to to evaluate a gate $g$ at depth $d$ is $2^dn^{O(1)}$,
assuming $\logspace$ uniformity.  This is polynomial in $n$, since 
$d = O(\log n)$.  The space required is dominated by the number of bits
needed, to write down the name of a gate, which is $O(\log^k{n})$.

This completes the proof, but let us mention here that later, in
\expref{Lemma}{lemma:sat_tw_in_nauxpda} and \expref{Lemma}{lemma:sattw_hard_for_sac}, we show that $\sattw(\log^k |\phi|)$ is hard for 
$\sac(O(\log{n}), 2^{\log^k{n}})$, and is contained in 
\[
\nauxpda\bigl(O(\log^k{n}), n^{O(1)}\bigr)\,.\qedhere
\] 
\end{proof}


The reader may be surprised that acceptance of a super-polynomial size circuit can be verified in (nondeterministic) polynomial 
time. This is related to the structure and size of \emph{proofs} of accepting inputs for semi-unbounded circuits.
In particular, the size of such a proof/certificate is exponential in the depth of the circuit  
(see the proof of \expref{Lemma}{lemma:sattw_hard_for_sac} for details).


%
%
%

\subsection{Completeness for \texorpdfstring{$\satpw(\log^k |\phi|)$}{SATpw(polylog)} and \texorpdfstring{$\sattw(\log^k |\phi|)$}{SATtw(polylog)}, and a new circuit characterization of the $\nsc$ hierarchy}\label{subsec:characterization}
In \expref{Theorem}{thm:sat_pw} we show that $\satpw(\log^k |\phi|)$ is complete for $\nsc^k$ and
\expref{Theorem}{thm:sat_tw} states that $\sattw(\log^k |\phi|)$ is complete for $\sacQuasi^k$. 
We remark that the tree-width/path-width relation $\pw(G)\leq \tw(G)\log n$ 
can be shown via a reduction computable in $\logspace$~\cite{BGHK95}.
Putting these together (or this can also be seen via a direct argument)
we have the following characterization of the $\nsc$ levels:

\begin{equation} \label{eq:characterization}
\underbrace{\NL}_{\nsc^1}\subseteq \underbrace{\sac^1}_{\sacQuasi^1}\subseteq \nsc^2\subseteq \sacQuasi^2\subseteq \nsc^3\subseteq \dots \subseteq \nsc=\sacQuasi\,.\end{equation}

Our completeness results require us to present upper bounds on the complexity
of $\sat$ with small tree-width and path-width.  For these upper bounds, we
need the notation of \emph{consistency}.  Since we have extended the notion of assignment to also 
include assignments to \emph{clauses}, we also need to have a
correspondingly extended notation of consistency of assignments.  The rigorous definition of 
consistency is deferred until the next section; for this section
it suffices to rely on an intuitive understanding of the notion. Intuitively, 
assignments to two bags are said to be consistent, if the bits corresponding 
to variables agree, and some additional constraints imposed by the bits corresponding to clauses are 
satisfied such that a satisfying truth assignment can be deduced. 
For this section, it suffices to know that, if assignments for two bags are
written on the worktape, then it is very easy to determine if the assignments 
are consistent.
Also, by the connectivity properties of tree decompositions, it suffices to check consistency of 
neighboring bags.

Now, we turn to showing these completeness results. The following lemma implies \expref{Theorem}{thm:sat_pw}.

\begin{lemma}\label{lemma:nsc_nl}
$\nsc^k=\NL[\log^{k-1}n]$, for $k\in\mathbb{Z}^+$.
\end{lemma}
\begin{proof}
Let's see why $\nsc^k\subseteq\NL[\log^{k-1}n]$ first. Let $M$ be a machine that accepts a 
language $L\in\nsc^k$.  {}From $M$, we construct a machine $M'$ that
uses only logarithmic space on its worktape, and that makes $O(\log^{k-1}n)$ 
passes over a tape of polynomial length that holds the sequence of
``nondeterministic'' bits.
On accepting computations, the nondeterministic tape of $M'$ will contain an
encoding of a computation of $M$: \ie, a sequence of
encodings of successive configurations (from initial state to accepting state)
of a complete run of $M$ accepting the given input.  (Clearly, such an
encoding will have polynomial length since the running time of $M$ is 
polynomial and the length of each configuration is $O(\log^k n)$.)  A 
configuration will include state, head position and worktape.  Without 
loss of generality we assume that all the encodings of configurations have the
same size, and that the worktape is divided evenly into blocks of length $O(\log n)$. 
Note that because of the locality of computation, two adjacent 
configurations only differ in $O(1)$ bits; the $i$th blocks of the worktape of two consecutive 
configurations will be identical when the head is not in the corresponding block, 
and otherwise will differ only in $O(1)$ bits. 

In the $i$th 
pass, starting from the initial configuration, $M'$ will check that the
$i$th blocks of each two consecutive configurations are correct.  To do this,
$M'$ will read blocks $i-1, i$, and $i+1$ of each two consecutive 
configurations into its worktape in turn, as well as the state and head 
position of both configurations.  If the head 
is not in the $i$th block, then $M'$ will merely check that $i$th blocks of
the two configurations are identical; if the head is in the $i$th block, $M'$ will check 
whether the move is a legal move of $M$.  Some additional 
bookkeeping is necessary when the head is moving into or out of the $i$th 
block; in those cases, the blocks $i-1$ and $i+1$ will also need to be
consulted.  If the $i$th blocks of configurations $j$ and $j+1$ are deemed to
be consistent, then the process is repeated for configurations $j+1$ and $j+2$.
It should be clear that $M'$ uses logarithmic space and makes only 
$O(\log^{k-1}n)$ passes over its nondeterministic tape.

For the other direction, it is sufficient to present a complete problem for $\NL[\log^{k-1}n]$ 
that is contained in $\nsc^k$. $\satpw(\log^k{|\phi|})$ is such a problem, by the following characterization:

\begin{lemma}[\cite{papakonstantinou2009note}]\label{lemma:sat_pw_nl}
$\satpw(\log^k{|\phi|})$ is complete for $\NL[\log^{k-1}n]$, for $k\in\mathbb{Z}^+$, 
under log-space many-to-one reductions.
\end{lemma}

A nondeterministic machine $M''$ for $\satpw(\log^k{|\phi|})$ runs as follows: on its worktape, 
$M''$ guesses assignments (each of length $\log^k |\phi|$) for each bag, in the order of path 
decomposition (storing only the assignments for
three bags at any one time).  In order to check the correctness of the assignment for the $j$th bag, 
the assignments for bags $j-1, j$, and $j+1$ on the working tape,
and the consistency of these assignments can be checked in polynomial time.  
By the properties of path decompositions, checking consistency of consecutive 
bags is sufficient for correctness.  $M''$ uses $O(\log^k n)$ space and 
polynomial time.
\end{proof}

\expref{Lemma}{lemma:sat_pw_nl} and \expref{Lemma}{lemma:nsc_nl} immediately yield
the following theorem:


\begin{theorem} \label{thm:sat_pw}
$\satpw(\log^k{|\phi|})$ is complete for $\nsc^k$, for $k\in\mathbb{Z}^+$, 
under log-space many-to-one reductions.
\end{theorem}
 


\begin{theorem}\label{thm:sat_tw}
$\sattw(\log^k{|\phi|})$ is complete for $\sacQuasi^k$, for  $k\in \mathbb{Z}^+$, 
under log-space many-to-one reductions.  
\end{theorem}
\begin{oproof}
Containment is by \expref{Lemma}{lemma:sat_tw_in_nauxpda} and \expref{Lemma}{lem:sac-nauxpda}, 
and hardness is by \expref{Lemma}{lemma:sattw_hard_for_sac}.

\begin{lemma}\label{lemma:sat_tw_in_nauxpda}
$\sattw(\log^k{|\phi|})\in\nauxpda\bigl(O(\log^k{n}),n^{O(1)}\bigr)$.
\end{lemma}
\begin{proof}
The algorithm witnessing this containment is very natural when expressed as a $\nauxpda$;
it is a modification of the algorithm in~\cite{GP08} with an additional trick to handle arbitrary CNF 
clauses, and has a very similar structure to the proof that $\satpw(\log^k{|\phi|})$ is in $\nsc^k$.

The $\nauxpda$ will perform a depth-first traversal of the tree decomposition,
guessing assignments corresponding to the bags (each of length 
$O(\log^k{|\phi|})$) using the worktape and the stack to check
consistency of the assignments.  More precisely, the $\nauxpda$ will start
at the root and guess an assignment for the root node, and then recursively
search the tree rooted at that node, given the current assignment.

To search the tree rooted at a given node $v$, given an assignment, the 
$\nauxpda$ will first check if $v$ has any children.  If not, the
$\nauxpda$ will halt and reject if the assignment is not accepting, and 
otherwise will pop the stack to continue searching the tree rooted at
$v$'s parent.  Otherwise, the $\nauxpda$ will guess assignments for $v$'s
children (of which there are $\leq 2$), and check that the
assignments are consistent, then push the second child and its assignment 
onto the stack, along with information about $v$ and its assignment, and then
search the tree rooted at the first child.  When that subtree has been 
searched, the $\nauxpda$ will pop the information for the second child off of 
the stack and search it.  If both subtrees are successfully searched, then
the $\nauxpda$ pops the stack to continue searching the tree rooted at
$v$'s parent.

It can be seen from the description that this machine requires $O(\log^k{|\phi|})$ space, and polynomial time.
\end{proof}

Hardness is more interesting. 
We do a reduction from an arbitrary language in $\sacQuasi^k$. Similar ``generic reductions'' 
(\ie, reducing the computation of families of $\sac$ circuits) for tree-width-related problems have appeared 
before, \eg,~\cite{gottlob2001complexity} . 


\begin{lemma}\label{lemma:sattw_hard_for_sac}
$\sattw(\log^k{|\phi|})$ is hard for $\sacQuasi^k$, under $\logspace$ many-to-one reductions.
\end{lemma}

\begin{iproof}
Fix $L\in \sacQuasi^k$ and an input $x$. Let $C$ be the associated $\sac$ circuit, with uniformity 
realized by a Turing Machine $M$ (\ie, the machine that decides the direct connection language). 
We construct a formula $\phi$ that is satisfiable if and only if $C(x)=1$. 
Without loss of generality we assume the that the
circuit $C$ is of the type constructed in the proof of the first part of
\expref{Lemma}{lem:sac-nauxpda}.  In particular, note that we may assume the
following normal form for $C$: 
(i) $C$ is \emph{layered}, (ii) $C$ is \emph{strictly alternating}: odd-layer gates are \textsf{OR}, 
even-layer gates are \textsf{AND}, (iii) $C$ has an odd number of layers, and (iv) the 
\textsf{AND} gates in $C$ have fan-in $2$. 

\begin{figure}[ht]                                                        
\begin{center}                                                            
\subfloat[A semi-unbounded circuit together with a proof-tree. 
The NOT gates are assumed to be part of the input]
{\includegraphics[height=110pt]{sac.pdf}\label{subfig:proof_tree}}
\hspace{40pt} \subfloat[The skeleton of the proof-trees]
{\includegraphics[height=110pt]{skeleton.pdf}\label{subfig:skeleton}}
\end{center}                                                              
\caption{Proof-tree. In (b), a $\sattw(\log^k{|\phi|})$ instance is
constructed from the skeleton: each node corresponds to
$O(\log^k{n})$ Boolean variables; clauses are constructed for each oval 
with dashed border; and only those variables corresponding to a node
shared by different dashed circles must be put into a bag in the
tree decomposition. This ensures $O(\log^k{n})$ tree-width.}
\label{fig:logcfl_hard}
\end{figure}     


A \emph{proof-tree} is a tree with the same layering as the circuit. Each node of the tree 
is labelled by an index of a gate from the corresponding layer of the circuit. 
At odd layers, each node has one child, while at even layers, each node has two children. 
Two connected nodes must be labelled such that the corresponding gates are connected. 
At the bottom layer, each node must be labelled by an input gate or a NOT gate which 
outputs value $1$. See \expref{Figure}{subfig:proof_tree} for an illustration of an example.

A proof-tree witnesses that $C(x)=1$. The main observation is that by the above normal form 
every proof-tree must have the same shape.  A \emph{skeleton} is a proof-tree without 
labels (see \expref{Figure}{subfig:skeleton}). Therefore, $C(x)=1$ if and only if there 
exists a labeling to the nodes of the skeleton which turns it into a valid proof-tree. 
It is important to note that, since $C$ has the form given in the proof of
\expref{Lemma}{lem:sac-nauxpda}, for any node $v$ in the skeleton, all valid labels
for $v$ will give $v$ a label corresponding to a gate that is checking the
\emph{same} phase with a given stack height; that is, all such labels will
correspond to a segment of the computation of a $\nauxpda$ with the \emph{same}
start and end times.
We encode this labeling as a CNF formula as follows. Associate a node $v$ in the skeleton 
with bit vectors $x_v, d_v, t_v$, where $|x_v|=|d_v|=\log^k{n}$, $|t_v|$ is constant. 
An assignment to these Boolean vectors can be viewed as a labeling in the following sense: 
$x_v$ indicates the index of the gate, $t_v$ indicates its type, while $d_v$ together with 
another $x_u$ indicates which predecessor in the circuit it should choose in the proof-tree. 
More specifically, for every node $v$ at an even-numbered layer in the skeleton with 
children $u_l$, $u_r$ we have:
$M(\langle n, x_v, 0, \overline{0}, \textsf{AND}\rangle)=1,$ 
$M(\langle n, x_v, d_v, x_{u_l}, \textsf{OR}\rangle)=1,$ and 
$M(\langle n, x_v, d_v, x_{u_r}, \textsf{OR}\rangle)=1.$
When $v$ is at an odd-layer, and $u$ is its child,
we have $M(\langle n, x_v, 0, \overline{0}, \textsf{OR}\rangle)=1$, and either
$M(\langle n, x_v, d_v, x_u, \textsf{AND}\rangle)=1$ or  
$M(\langle n, x_v, d_v, x_u, 1\rangle)=1$.

A correct proof-tree exists if and only if, for each edge $(v,u)$, in the 
skeleton, the assignments to the variables in $x_v, d_v$ and $x_u$ can
be picked so that $M$ accepts the corresponding tuples.
This condition can be formalized as $\exists s, M'(s)=1$, where $|s|=O(\log^k{n})$, 
corresponding to the input bits provided to a Turing machine $M'$ (a 
modification of $M$) having running time $O(\log^k{n})$ on $s$. 
We would like to encode this \`a la Cook-Levin (see \eg,~\cite{arora2009computational}) 
as a CNF of size $O(\log^k{n})$---but there is a catch.
Using the tools provided in~\cite{arora2009computational}, this is only 
possible if $M'$ is \emph{oblivious}---and a na\"{i}ve approach to making $M'$
oblivious would introduce an unwanted $\log\log n$ factor; thus we need to
look more closely at the condition that $M'$ is checking.

$M'$ is taking $s$ as input, and checking that $s$ is giving information about
adjacent gates in $C$.  Since all of the valid labels for a node in the skeleton
are concerned with the \emph{same} segment of an oblivious $\nauxpda$'s 
computation, we can use the standard technique 
(\eg,~\cite{arora2009computational}) to build a CNF of size $O(\log^k n)$ 
verifying that the connectivity information is correct.  (For example, $s$
could give the encodings for gates labeled
$(A,B)$ and $(C,D,E,\gamma)$, and we need to verify that the $\nauxpda$ can
move from $A$ to $C$ pushing $\gamma$, and move from $E$ to $B$ popping 
$\gamma$). 
At the end we take the conjunction of all the CNFs corresponding to the nodes and edges, 
which is also a CNF $F$, where $F$ is satisfiable if and only if $C(x)=1$.

It remains to show that $F$ has tree-width $O(\log^k{n})$. 
Notice that clauses in $F$ are defined for only one specific node, and variables appear in 
clauses corresponding to at most two nodes. Therefore  there is a natural tree decomposition 
associated with $F$, as illustrated in \expref{Figure}{subfig:skeleton}, that is, clauses and 
variables corresponding to an edge in the skeleton form a bag, and two bags are connected 
when they share variables. By the argument above, this tree
decomposition has tree-width $O(\log^k{n})$.
\end{iproof}
\end{oproof}

\begin{remark}
In general, when the tree-width is anything larger than poly-logarithmic, the previous 
reductions still hold. In particular, $\sattw(w(|\phi|))$ is complete
for \[
\sac\bigl(O(\log |\phi|), 2^{O(w(|\phi|))}\bigr)\,.
\]
\end{remark}

\begin{remark}
The proof of \expref{Lemma}{lemma:sattw_hard_for_sac} constructs a $\sat$
instance $\phi$ for which not only the \emph{incidence} graph has small
treewidth, but also the \emph{primal graph} has small treewidth.  Thus,
although the treewidth of the primal graph can be \emph{much} larger than 
the treewidth of the incidence graph, $\sat$ instances of small treewidth
are complete for the $\sacQuasi^k$ classes, no matter whether treewidth is
measured with respect to the incidence graph, as in this paper, or with respect
to the primal graph, as in~\cite{BDP}.  
\end{remark}

%
%
%

\subsection{Connecting \expref{Conjecture}{conj:mainconj} to complexity theory 
assumptions and the separation of \texorpdfstring{$\satpw(\log^k |\phi|)$}{SATpw(polylog)} from \texorpdfstring{$\sattw(\log^k |\phi|)$}{{SATtw(polylog)}}}

We list corollaries of the completeness results obtained in the previous sub-section. 

\begin{corollary}
$\sacQuasi^k\not\subseteq \tisp\bigl(2^{O(\log^k n)}, n^{o(1)}\bigr)   \iff$  \expref{Conjecture}{conj:mainconj} for tree-width $O(\log^k |\phi|)$.
\end{corollary}

In particular, when $k=1$, we have that \expref{Conjecture}{conj:mainconj} for 
tree-width $O(\log |\phi|)$ is equivalent to 
\[
\sac^1\not\subseteq \tisp\bigl(n^{O(1)}, n^{o(1)}\bigr)\,.
\]

This corollary is just a resource-scaled form of our initial equivalence for logarithmic tree-width. 
In fact, by padding\footnote{
Philosophically, the assumption 
\[
\sacQuasi^k\not\subseteq \tisp\bigl(2^{O(\log^k n)}, n^{o(1)}\bigr)
\]
is not really different than 
the widely-believed assumption $\sac^1\not\subseteq \tisp(n^{O(1)}, n^{o(1)})$. By analogy let us consider
$\p\neq\np$ and $\cclass{E}\neq \cclass{NE}$. It is true that $\cclass{E}\neq \cclass{NE}$ 
is stronger in the sense that 
$\cclass{E}\neq \cclass{NE}$ implies $\p\neq\np$ (via a simple padding
argument), and it is also the case that at the current state-of-the-art we 
have no idea how to obtain the converse implication.  (In fact, this is true for the vast majority of 
these resource-scaled 
analogs of other complexity conjectures).  Also, it is worth noting that the
converse fails relative to some oracles~\cite{wilson}.  However, in principle we see no real reason 
why one should believe in one
and not in the other (especially when the scaling in the resource bounds is moderate); they are merely 
different manifestations of the same underlying question. Our conjecture is equivalent 
to $\sac^1\not\subseteq \tisp(n^{O(1)}, n^{o(1)})$ for logarithmic tree-width, whereas for larger tree-width we have only
shown equivalence to the scaled analogs of $\sac^1\not\subseteq \tisp(n^{O(1)}, n^{o(1)})$.
} 
we have:

\begin{corollary} \label{cor:nc-vs-sc}
\expref{Conjecture}{conj:mainconj} for tree-width $\polylog(|\phi|)$ $\implies$ $\sac^1\not\subseteq\SC$.
\end{corollary}

Thus, modulo these complexity assumptions this settles the lower bound of the Alekhnovich-Razborov question.
Note that \expref{Corollary}{cor:nc-vs-sc} opens new avenues for propositional proof complexity~\cite{BBI}; 
\ie, validating our conjecture for restricted types of algorithms implies progress towards $\nc\neq\SC$.

As another corollary, assuming that $\NL\subsetneq\sac^1$, we separate the complexity of $\satpw$ and $\sattw$.

\begin{corollary}
$\sattw(\log |\phi|)$ is not log-space reducible to $\satpw(\log |\phi|)$, unless $\NL=\sac^1$.
\end{corollary}

In fact, the above holds up to $\NL$-reductions. This corollary extends to every poly-logarithmic width 
under the scaled assumption $\nsc^k\subsetneq\sacQuasi^k$. 
This is the first separation result for width parameterizations of $\sat$ for the same width parameter. 
Prior to our work there were only results in the opposite direction~\cite{GP08}, where some width parameters 
(\eg, band-width and path-width) were shown to be log-space-equivalent,  although
combinatorially they can be off by an exponential.

 



%
%
%
%


\section{Tradeoff algorithms on a single parameter} \label{sec:alg}
%
%

We consider two basic algorithms. One is time-efficient, which works
in time-space 
\[
\big(2^{2\tw(\phi)}|\phi|^{O(1)}, 2^{\tw(\phi)}|\phi|^{O(1)}\big)\,,
\]
 whereas the space-efficient one works in time-space 
\[
\bigl(3^{\tw(\phi)\log{|\phi|}}|\phi|^{O(1)}, |\phi|^{O(1)}\bigr)\,.
\]
The first one~\cite{SS10} is the most time-efficient (with respect to the constant in the exponent) algorithm known. The second is our contribution, and it is the first space-efficient algorithm for arbitrary CNFs for tree decompositions on the incidence graph. Our main contribution is combining these two algorithms in a non-trivial way to obtain a tradeoff. Later on, in \expref{Section}{subsec:warmup}, we provide a primer to algorithms for $\sat$ instances with given tree decompositions. 

\paragraph{Overview of the time- and space- efficient algorithms.}

The time-efficient algorithm does dynamic programming using the tree 
decomposition in a typical way~\cite{bodlaender1993tourist}: root the tree to 
make it a binary tree, then for each bag define a $2^{\tw(\phi)}$ size 
Boolean array; entry $j$ in the array will be 1 if the subformula rooted at 
the bag is satisfiable, when the variables are given assignment $j$, and will 
be 0 otherwise. Clearly, computing the array for the root will solve the 
satisfiability of the formula, and indeed by the property of a tree 
decomposition, the array values can be computed in a leaves-to-root fashion.

To simplify the overview of the space-efficient algorithm we shall temporarily assume that each clause appears in a bag together with all of its variables.\footnote{We remove this assumption later; see
\expref{Section}{subsec:warmup}.}
Observe that if we fix a truth assignment on a bag, then solving $\sat$ on the given tree decomposition reduces to solving \eg, $3$ independent subproblems---think of splitting the degree-$3$ tree into three subtrees by cutting the original one at this bag. The algorithm works by recursively enumerating and checking truth assignments on the bags. Its performance is determined by the size of the subproblems (ideally all the subtrees have the same size). In \expref{Section}{subsec:splitting} (\expref{Lemma}{lemma:cutting} below) we show that there always exists a good choice for a bag, reminiscent to the well-known ``\sfrac{1}{3} - \sfrac{2}{3} lemma'' for binary trees. The lemmas in \expref{Section}{subsec:splitting} are a bit of an overkill for the analysis of this simple algorithm, but they are also applied in the analysis of the  tradeoff. 


\paragraph{The tradeoff algorithm: where is the complication?}
Let us consider for a moment an execution of the space-bounded algorithm. We can visualize each step of the recursion as splitting the tree decomposition at a node (bag)---this bag is replicated at each of the subproblems with the fixed truth assignment. Let the process evolve for a while, and when the forest has enough trees let us single out one such tree. At the boundary (the leaves) of this tree there can be as many as $\log|\phi|$ nodes to which we previously fixed an assignment, \ie, by splitting.
 \emph{The logarithmically large number of nodes does not affect the
   performance of the space-efficient algorithm} (at each point of the
 recursion each bag/node is associated with a single assignment). Now,
 we switch gears to devise a tradeoff algorithm. A natural thing to do
 is first to discretize the truth assignment space associated with
 each bag, say in $2^{(1-\eps)\tw(\phi)}$ many chunks each of size
 $2^{\eps\tw(\phi)}$, and we perform the recursion as in the
 space-efficient algorithm but now instead of one assignment we assign
 the whole chunk. This brings the enumeration, at each recursive step,
 from $2^{\tw(\phi)}$ down to $2^{(1-\eps)\tw(\phi)}$. On the other
 hand combining the chunks of the truth assignments into one
 consistent chunk associated with this tree may increase the space as
 much as $2^{\eps\log|\phi|\tw(\phi)}$. Overall this is a time-space 
\[
\big( 2^{(1-\eps)\log|\phi|\tw(\phi)},2^{\eps\log|\phi|\tw(\phi)}\big)
\]
algorithm, worse both than the time- and space-efficient ones! To devise our tradeoff algorithm we show that it is possible to \emph{simultaneously} (i) perform the splitting in a way that at each step of the execution the forest consists of trees each with at most a constant number of split-nodes and (ii) this splitting results in subproblems of somewhat balanced sizes. Furthermore, we show that it is possible to control the number of splitting nodes per tree in the forest in a way that yields a tradeoff on this parameter (\expref{Section}{sec:alg2}). This is a different (and competing) tradeoff from the one by the discretization factor $\eps$; \ie, our most general tradeoff algorithm is controlled by two parameters. 





\subsection{A primer to algorithms for width-parameterized \texorpdfstring{$\sat$}{SAT}}    \label{subsec:warmup}
%
The structure of a tree decomposition is associated with the concept of separability (see \eg,~\cite{bodlaender1998partial}). Intuitively, the smaller the tree-width is, the easier the graph can be broken into separate components by removing nodes. 
Separability allows us to devise more efficient algorithms for small tree-width $\sat$ than for general $\sat$. In some sense, the given tree decomposition allows us to ``localize'' an exhaustive search. The following example sheds some light on how this can be done towards devising a space-bounded algorithm. 
Recall that, for this initial overview, we are assuming that all the variables of a clause appear in the same bag with the clauses. 
We will see later that removing this assumption in a time-efficient manner is non-trivial (in fact, removing it without increasing the base of the exponential running time is an interesting puzzle).

\begin{figure}[ht]                                                        
\begin{center}                                                            
\subfloat[Input tree decomposition.]{\includegraphics[height=120pt]{simple_example.pdf}\label{subfig:simple_example}}\hspace{40pt}
\subfloat[Fixing an assignment to the variables in the middle bag results in two independent instances.]{\includegraphics[height=120pt]{simple_example2.pdf}\label{subfig:after_splitting}
}
\end{center}                                                              
\caption{An example showing bounded tree-width $\sat$ can be solved efficiently.}
\label{fig:simple_example}
\end{figure}   

Suppose $x_i$'s, $x'_i$'s and $x''_i$'s are different sets of variables and the tree decomposition  is as in \expref{Figure}{subfig:simple_example}. 
Let us fix a truth assignment to the variables in the bag in the middle, \eg, $x_1=x_2=x_3=x_4=1$. Conditioned on this truth assignment we can simplify the instance by removing clauses that are already satisfied, and removing literals in a clause that are set to false. This will result in multiple sub-instances as shown in \expref{Figure}{subfig:after_splitting}. The properties of a tree decomposition assure that the sub-instances depend on different sets of variables, \ie, they are \emph{independent}. Since if instead they shared a common variable, this variable would have appeared in the middle bag, \eg, $x_2$. But this variable is already fixed by the truth assignment.


The satisfiability of the input instance, conditioned on the truth assignment given to the middle bag, is determined by the satisfiability of the two separate sub-instances. Therefore, it suffices to enumerate all truth assignments satisfying all the clauses in the middle bag without causing empty clauses in the simplification phase. Then, recurse into the two independent sub-instances to decide the satisfiability of the original instance. Furthermore, by choosing the middle bag carefully we can invoke this ``splitting'' on subtrees of somewhat balanced size. 

In each recursive step, the most time-consuming part is to enumerate all the assignments satisfying all the clauses in the chosen bag, which costs $O(2^{\tw(\phi)}|\phi|^{O(1)})$ time, and the total running time is $O(2^{\tw(\phi)\log{|\phi|}}|\phi|^{O(1)})$, which is much better than the current best algorithms for general $\sat$, which run in time exponential in $|\phi|$.

\paragraph{The subtle additional assumption.}
%
The assumption that all variables of a clause appear in the same bag with the clause is not a mild one (especially for CNFs of large cardinality).  Of course, in the actual algorithms we make no such assumption. In general, we may have to delay the decision to satisfy a clause. In the above algorithm, we only store the truth assignments to the variables. The following example shows that only storing this information is not enough when aiming at removing the assumption.

\begin{figure}[ht]                                                        
\begin{center}                                                            
{\subfloat[$\phi_1$]{\includegraphics[height=60pt]{bags1.pdf}}}
\hspace{10pt}{\subfloat[$\phi_3$]{\includegraphics[height=60pt]{bags3.pdf}}}
\hspace{10pt}{\subfloat[$\phi_2$]{\includegraphics[height=60pt]{bags2.pdf}}}
\end{center}                                                              
\caption{Three instances used in the example. Figures on the top are
the input tree decompositions, the bottom figures are the two
components after fixing assignment to the variables in the middle
bag.}\label{fig:example_in_preliminary}
\end{figure}     

Suppose $C_1=x_1\vee x_2\vee x_4\vee x_6$,
$C_2=\overline{x_1}\vee x_3\vee x_5$, $C_3=\overline{x_2}$,
$C_4=\overline{x_3}$, $C_5=\overline{x_4}$, $C_6=\overline{x_5}$ and
$C_7=\overline{x_6}$. Three instances $\phi_1$, $\phi_2$ and $\phi_3$
along with their tree decompositions are given in
\expref{Figure}{fig:example_in_preliminary}, where
$\phi_1=C_1\wedge\cdots\wedge C_7$, $\phi_2=C_1\wedge \cdots \wedge
C_5\wedge C_7$ (\ie, $C_6$ is missing), and
$\phi_3=C_1\wedge\cdots\wedge C_4\wedge C_6\wedge C_7$ (\ie, $C_5$ is missing). We say that a clause is satisfied by a literal under a truth assignment if the literal appears in the clause and is set to $1$. If an instance is satisfiable, then there is a truth assignment where every clause is satisfied by one of its literals.

Now, consider the splitting operation on the middle bag by fixing a truth assignment to it as above. For all three instances, the only possible assignment for $x_6$ is $0$, since $C_7$ must be satisfied by $x_6=0$. Similarly, in the left bag, we
must assign $x_2=0$ and $x_3=0$ to satisfy $C_3$ and $C_4$. In the left bag, the only variable left is $x_1$, which can satisfy either $C_1$ or $C_2$ but not both. The three instances differ in the right part where two variables $x_4$ and $x_5$ are left.

Satisfying $C_5$ requires $x_4=0$, which implies that $C_1$ can not be
satisfied by $x_4$. Similarly, satisfying $C_6$ requires $x_5=0$, so that $C_2$ can not be satisfied by $x_5$. In order to find a satisfying truth assignment, when processing the right part, we need information about which of $C_1$, $C_2$ is already satisfied in the left part.  (Since $\phi_1$ is not satisfiable, the final outcome will be the same in either case.)  $\phi_2$ is satisfied only when $C_1$ is already satisfied, while $\phi_3$ is satisfied only when $C_2$ is already satisfied. This piece of information is not carried through the middle bag by just the truth assignment to the variables. To overcome this issue we are going to use ``clause-bits,'' which we mentioned briefly in \expref{Section}{subsec:assignments}.

\subsection{Splitting, consistency, assignment groups} \label{subsec:splitting}
In this section we give some additional notation and technical lemmas which we apply in the analysis of the space-efficient (\expref{Section}{subsec:space}) and tradeoff algorithms (\expref{Sections}{subsec:trade_off} and~\ref{sec:alg2}). First we define an operation which allows a natural divide-and-conquer strategy, and a lemma follows the definition for choosing where the operation should occur. Then we define consistency with respect to our definition of assignments, which is somehow subtle and different from consistency of truth assignments. And in the last part of this section, we define a type of \emph{discretized assignment} which is crucial in the tradeoff algorithms.

\begin{definition}[Splitting operation]
Let $T=(V,E)$ be a tree, and $v\in V$. \emph{Splitting $T$ at $v$} is the following operation. Let $T_1,\dots,T_k$ be the trees after removing $v$ from $T$. The splitting operation results in a forest $\{v\}\cup T_1,\dots,\{v\}\cup T_k$, where $\{v\}\cup T_i$ is the subtree induced by the nodes in $T_i$ together with $v$. $v$ is called the \emph{splitting node} of this operation.
\end{definition}

Given a tree $T$ together with a sequence of splitting operations results in a forest where each subtree in the forest in general has many nodes marked as splitting nodes. Splitting nodes before a specific splitting operation are called \emph{previous splitting nodes}. A splitting operation also splits the set of previous splitting nodes $S$ into $S_i$'s, where $S_i$ is the set of splitting nodes contained in tree $T_i$, $1\le i\le k$.

Note that a splitting operation on a tree will result in a forest with more nodes than before, since we duplicate the splitting node and let it appear in each resulting tree. This fact will complicate the analysis of a recursive procedure. To overcome this, consider for each node, we create $d-1$ replicas. When a splitting operation occurs, each replica of the splitting node goes to one of the branches (and redundant ones get removed if there are). Each node can be treated as splitting node only once, so the replicas of a node will be distributed only once. These slightly modified splitting operations will never increase the number of nodes. When analyzing running time on a tree originally with $N$ nodes, one needs to use $d\cdot N$ as a upper bound of the number of nodes. We will see that this is negligible since the number of nodes only appears as a polynomial factor or an argument logarithmically in the exponent of the running time. For ease of exposure, we will stick to the notation $N$ as the number of nodes, while this should be the number after replicating.

A \emph{splitting algorithm} $\mathcal{A}$ computes a function that, given a tree $\mathcal{T}$ together with previous splitting nodes $S$, returns a node where the next splitting operation is going to be performed. A splitting algorithm formalizes the way of breaking an instance into sub-instances in the space-efficient algorithm. In particular, choosing the \emph{balancing splitting node} is done according to the following lemma.

\begin{lemma}\label{lemma:cutting}
Consider a tree of size $N$, a leaf $s$ and $0<\alpha<1$, and satisfying $N>1/\alpha$. Then, there is a node $p$ where after we split at $p$, the tree which contains $s$ is of size $\leq \lceil\alpha N\rceil$ and every other tree is of size $\leq\lceil(1-\alpha) N\rceil$. The node $p$ is called an $\alpha$-splitting node. Furthermore, such a $p$ can be found in time polynomial in $N$.
\end{lemma}
\begin{proof}
We prove this lemma by giving an algorithm for finding $p$. First root the given tree at $s$,
and then we iteratively construct a path $\langle s\equiv v_1,v_2,\dots,v_\ell \rangle$ as follows. After constructing the path from $v_1$ through $v_{i-1}$, $v_i$ is chosen to be child of $v_{i-1}$ which roots the largest subtree. We claim that there exists an $\alpha$-splitting node in this path.

Denote by $a_i$ the size of the subtree containing $s$ after splitting at
$v_i$, $1\le i\le \ell$. It is not hard to see that $a_1=1$, $a_\ell=N$, and $a_i$
strictly increases as $i$ increases. Therefore, there must be a $j$,
such that $a_j\le\alpha N$ and $a_{j+1}>\alpha N$. We claim that
$v_j$ is the node we need. If $a_{j+1}-a_j=1$, then splitting at $v_j$
results in two components, where the size of the component containing
$s$ is $\lceil\alpha N\rceil$, while the other one is of size
$\lceil (1-\alpha)N\rceil$. If $a_{j+1}-a_j>1$, then there must be a
branch at $v_j$, meaning that $v_j$ has at least two children.
Splitting at $v_j$ results in at least three components. One which contains
$s$ and is of size  smaller than $\alpha N$. The largest one among the rest
is of size smaller than $(1-\alpha)N$.
\end{proof}

\begin{corollary}       \label{lemma:half}
On a bounded-degree tree of size $N$, there exists a node $p$, such that after splitting at $p$ each subtree is of size at most $\lceil N/2\rceil$.
\end{corollary}

\paragraph{Consistent assignments.}
In what follows we assume that there is an initial tree
decomposition (recall that the bags are denoted by $X_i$) together with
a sequence of splitting operations $S$ that results in the subtrees
along with their splitting nodes.

We refer to an \emph{assignment on a subtree} as the assignment that
corresponds only to its splitting nodes. Formally, let $X^{*} =
\bigcup_{v_i\in S}{X_i}$, and let $\mathcal{V}$ be the variables and
$\mathcal{C}$ the clauses which have corresponding nodes in
$X^*$. $X^*$ is the set of variables and clauses on which we define
assignments. Suppose in one single splitting operation at the node
$p$, to which $X_p$ is the corresponding bag, $\mathcal{T}$ splits
into subtrees $\mathcal{T}_i$'s.
Further suppose $R_{\mathcal{T}}$ is an assignment to $\mathcal{T}$,
and $R_{\mathcal{T}_i}$ is an assignment to the subtree
$\mathcal{T}_i$. Note that the only difference between
$R_{\mathcal{T}}$ and $R_{\mathcal{T}_i}$'s is at $X_p$, and
$R_{\mathcal{T}}$ and $R_{\mathcal{T}_i}$'s are said to be
\emph{consistent} if
\begin{enumerate}[(1)]
\item for a variable $x$:
  \begin{enumerate}[a)]
  \item if $x$ appears in $X_p$, then all the bits for $x$ in each
    $R_{\mathcal{T}_i}$ are assigned to the same value;
  \item otherwise, all the bits for $x$ are assigned to the same value
    as in $R_{\mathcal{T}}$;
  \end{enumerate}
\item for a clause $C$:
\begin{enumerate}[a)]
\item if $C$ appears in $X^*$ and is assigned to $0$, then $\forall i$
  every bit for $C$ in $R_{\mathcal{T}_i}$ is assigned to $0$;
\item otherwise, $\exists$ exactly one $i$ such that in
  $R_{\mathcal{T}_i}$ the bit corresponding to $C$ is assigned to $1$.
\end{enumerate}
\end{enumerate}

\begin{figure}[ht]                                                        
\begin{center}                                                            
\includegraphics[height=160pt]{consistent_example.pdf}
\end{center}                                                              
\caption{Consistent assignments. $C_1=x_1\vee \overline{x_2}\vee x_3$, $C_2=x_3\vee \overline{x_4}$. Consider splitting at the gray bag, while fixing the value of the bits, $1$ for $C_1$, $0$ for $x_3$. Any possible consistent assignments for $\mathcal{T}_1$, $\mathcal{T}_2$, $\mathcal{T}_3$ will have $0$ for $x_3$; in this consistent assignment $C_1$ has value 1 in $\mathcal{T}_1$, and has value 0 in $\mathcal{T}_2$ and $\mathcal{T}_3$.}
\label{fig:consistent}
\end{figure}     

\begin{remark} \label{rem:exactly-one}
The latter point in the definition, where in exactly one of the subtrees we require that the corresponding bit equals to $1$, is somewhat subtle. The following lemma crucially depends on this property.
\end{remark}



\begin{lemma}\label{lem:assignment_consistent_count}
For every assignment $\mathcal{R}_{\mathcal{T}}$ to the tree
$\mathcal{T}$, the number of assignments $R_{\mathcal{T}_i}$ to
subtrees $\mathcal{T}_i$'s consistent with
$\mathcal{R}_{\mathcal{T}}$ is at most $d^{\tw(\phi)}$.  (Recall $d \in \{2,3\}$.)
\end{lemma}

\begin{proof}
Let $X_p$ be the bag corresponding to the splitting node $p$. For each variable $x$ in the bag $X_p$, there are $2$ possible assignments of the bit for $x$ in the $\mathcal{T}_i$'s. For each clause $C$ in $X_p$, if $C$ appears in $R_{\mathcal{T}}$ and is assigned to $0$, by the definition of consistency, all the bits for $C$ in the $\mathcal{T}_i$'s are assigned to $0$. Otherwise, in exactly one $\mathcal{T}_i$, the bit for $C$ is assigned to $1$; in this case there are at most $d$ valid assignments. Recall that $d$ is the maximum degree of the tree decomposition.
\end{proof}


We define a satisfying assignment in a way consistent with the role of clause bits in the assignments. 

\begin{definition}\label{def:satisfiable}
For a tree $\mathcal{T}$ with splitting nodes $S$, an assignment $R_{\mathcal{T}}$ is \emph{satisfying} if
there exists a truth assignment $A$ to every variable in $\mathcal{T}$, such that
\begin{enumerate}[(1)]
\item every truth value for a variable in $R_{\mathcal{T}}$ agrees with the corresponding value in $A$,
\item every clause $C$ that appears in $\mathcal{T}$ where $C$ does not appear in $S$, is satisfied by $A$,
\item every clause $C$ that appears in $S$ and the corresponding bit is assigned to $1$ by $R_{\mathcal{T}}$ is satisfied by $A$.
\end{enumerate}
\end{definition}

A satisfying assignment of the input tree decomposition with empty splitting nodeset implies that the input formula is satisfiable. The following lemma shows that the task of finding a satisfying assignment can be done recursively.

\begin{lemma}\label{thm:satisfiable}
An assignment $R_{\mathcal{T}}$ is \emph{satisfying} if and only if
there exist a \emph{satisfying} assignment $R_{\mathcal{T}_i}$ to each subtree
$\mathcal{T}_i$, such that all of the assignments $R_{\mathcal{T}_i}$ are
consistent with $R_{\mathcal{T}}$.
\end{lemma}

\begin{proof}
For a tree $\mathcal{T}$ with splitting nodes $S$, suppose that
splitting at node $p$ results in the subtrees $\{\mathcal{T}_i\}$.
Suppose that the assignment $R_{\mathcal{T}}$ is \emph{satisfying}.
By \expref{Definition}{def:satisfiable},
there exists a truth assignment
on variables within $\mathcal{T}$ that makes all of the clauses true. 
This truth assignment induces assignments $R_{\mathcal{T}_i}$ consistent with
$R_{\mathcal{T}}$, such that for these truth assignments the
conditions in \expref{Definition}{def:satisfiable} are met.  (Some of the clause
bits in the $R_{\mathcal{T}_i}$ may need to be set to zero, to ensure consistency.)

For the other direction suppose that there exist assignments $R_{\mathcal{T}_i}$
of the subtrees $\mathcal{T}_i$, such that the assignments
$R_{\mathcal{T}_i}$'s are consistent with $R_{\mathcal{T}}$ and all
$R_{\mathcal{T}_i}$'s are \emph{satisfying}. For each subtree
$\mathcal{T}_i$, there exists a truth assignment complying to
\expref{Definition}{def:satisfiable}. Since all these
truth assignments agree on their common variables (because the common variables
appear in splitting nodes in $S$), we can get a truth
assignment from their union, which also meets the axioms in
\expref{Definition}{def:satisfiable}. Therefore, the assignment
$R_{\mathcal{T}}$ is satisfying.
\end{proof}


An \emph{$\eps$-assignment group} $\eps$-$\GR_{\mathcal{T}}$ is a set of all possible assignments to $S$, where at most $(1-\eps)|S|\tw(\phi)$ entries  are fixed. By definition, $\eps$-assignment groups can be identified by the fixed entries.
Consider a tree $\mathcal T$, $\eps$-assignment group $\eps$-$\GR_{\mathcal{T}}$,
and subtrees $\mathcal{T}_i$ resulting from a split at some node $p$.  
Consider one such subtree ${\mathcal {T}_i}$; let $S_i$ be the set of splitting 
nodes for ${\mathcal {T}_i}$, and note that $S_i \subseteq S\cup\{p\}$ (and very
likely it is a proper subset).  By fixing the ``first'' 
$(1-\eps)\tw(\phi)$ entries corresponding to variables or clauses contained in the node $p \in S_i$ (using some fixed ordering), one obtains an $\eps$-assignment group $\eps$-$\GR_{\mathcal{T}_i}$ for $\mathcal{T}_{i}$. 

Given a tree $\mathcal T$ and subtrees ${\mathcal {T}_i}$ resulting from a split, the $\eps$-assignment groups
$\eps$-$\GR_{\mathcal{T}}$ and $\eps$-$\GR_{\mathcal{T}_i}$'s are called \emph{consistent} if 
there exist $R_{\mathcal{T}}\in\eps$-$\GR_{\mathcal{T}}$ and $R_{\mathcal{T}_i}\in\eps$-$\GR_{\mathcal{T}_i}$ for each $i$, such that $R_{\mathcal{T}}$ and the $R_{\mathcal{T}_i}$'s are consistent. 

Note that the fixed entries for the splitting node $p$ may be different among subtrees (because of the rules regarding clause bits), and note also that some of the unfixed entries in $\mathcal{T}$ may fixed in subtrees (because they appear in $p$). The following important lemma holds, which basically generalizes \expref{Lemma}{lem:assignment_consistent_count}.

\begin{figure}[ht]                                                        
\begin{center}                                                            
{
\subfloat[An $\eps$-assignment group where $(1-\eps)$ fraction of values are fixed]
{
\begin{minipage}{120pt}
\begin{eqnarray*}
&\underbrace{1 \hspace{5pt} 0 \hspace{5pt}  1 \hspace{5pt}  0 \hspace{5pt}  1 \hspace{5pt}  1 \hspace{5pt}  1}_{(1-\eps)|\mathcal{S}|\tw(\phi)} \hspace{5pt}  \underbrace{* \hspace{5pt}  * \hspace{5pt} *}_{\eps|\mathcal{S}|\tw(\phi)}&
\end{eqnarray*}
\end{minipage}
}
\hspace{40pt}
\subfloat[Assignments in the group]
{
\begin{minipage}{120pt}
\begin{eqnarray*}
&1 \hspace{5pt} 0 \hspace{5pt}  1 \hspace{5pt}  0 \hspace{5pt}  1 \hspace{5pt}  1 \hspace{5pt}  1 \hspace{5pt}  0 \hspace{5pt}  0 \hspace{5pt} 0&\\
&1 \hspace{5pt} 0 \hspace{5pt}  1 \hspace{5pt}  0 \hspace{5pt}  1 \hspace{5pt}  1 \hspace{5pt}  1 \hspace{5pt}  0 \hspace{5pt}  0 \hspace{5pt} 1&\\
&\vdots&\\
&1 \hspace{5pt} 0 \hspace{5pt}  1 \hspace{5pt}  0 \hspace{5pt}  1 \hspace{5pt}  1 \hspace{5pt}  1 \hspace{5pt}  1 \hspace{5pt}  1 \hspace{5pt} 1&
\end{eqnarray*}
\end{minipage}
}
}
\end{center}                                                              
\caption{$\eps$-assignment group.}
\label{fig:thislabelisneverused}
\end{figure}     


\begin{lemma}\label{lem:assignment_consistent_count_important}
The number of distinct $\eps$-$\GR_{\mathcal{T}_i}$'s
consistent with $\eps$-$\GR_{\mathcal{T}}$ is at most
$d^{(1-\eps)\tw(\phi)}$.
\end{lemma}


\begin{proof}
Here we only consider the first $(1-\eps)$ fraction of entries, which
are going to be fixed, since as pointed out in previous discussion, an
$\eps$-assignment group is identified by the values of the fixed
entries. For each variable $x$, there are $2$($\leq d$) possible
values. For each clause $C$, let $d_0(\leq d)$ be the number of
subtrees created by splitting at $p$. There are two different cases:
%

\begin{enumerate}[(1)]
\item \emph{$C$ is not in any previous splitting nodes, or $C$ is in some previous splitting node but its value is unfixed.} There are $d_0$ possible ways of assigning values to the bit for $C$, such that there is exactly one of $\mathcal{T}_i$'s, whose bit for $C$ is set to $1$ to ensure $C$ is satisfied.
\item \emph{$C$ is in some previous splitting node, and its value is fixed in $\eps$-$\GR_{\mathcal{T}}$.} If the bit for $C$ is assigned $1$, then there are
$d_0$ possible assignments to $C$ similar as above, otherwise
the only possible way is to set all bits for $C$ to $0$.
\end{enumerate}

Since there are at most $(1-\eps)\tw(\phi)$ entries that need to be fixed, in order to form the $\eps$-$\GR_{\mathcal{T}_i}$'s, the number of different combinations of
$\eps$-$\GR_{\mathcal{T}_i}$'s consistent with
$\eps$-$\GR_{\mathcal{T}}$ is at most $d^{(1-\eps)\tw(\phi)}$.
\end{proof}

\subsection{The space-efficient algorithm} \label{subsec:space}
%
The space-efficient algorithm is described in \expref{Algorithm}{alg:divide_and_conquer}. 
$\mathcal{T}$ is a tree with
previous splitting nodes $S$, and $R_\mathcal{T}$ is the assignment
fixed on the tree. A subtle point that affects the running time of this algorithm
is addressed in \expref{Remark}{rem:exactly-one}. 
The correctness of the algorithm directly follows by \expref{Lemma}{thm:satisfiable}.


\begin{algorithm}
\caption{SAT($\mathcal{T}$, $R_\mathcal{T}$).}
\label{alg:divide_and_conquer}
\begin{algorithmic}[1]
\If {all nodes in $\mathcal{T}$ are previous splitting nodes}
\If {every clause in $R_\mathcal{T}$ assigned value $1$ is satisfied
by some variable in $\mathcal{T}$}
\State \Return $\mathbf{True}$
\Else
\State \Return $\mathbf{False}$
\EndIf
\Else
\State split at the $1/2$-splitting node, and denote the subtrees as $\mathcal{T}_{i}$'s
\ForAll {$R_{\mathcal{T}_{i}}$'s consistent with $R_\mathcal{T}$}
\If {$\forall \mathcal{T}_{i}$,
SAT($\mathcal{T}_{i}$, $R_{\mathcal{T}_{i}}$) = $\mathbf{True}$}
\State \Return $\mathbf{True}$
\EndIf
\EndFor
\State \Return $\mathbf{False}$
\EndIf
\end{algorithmic}
\end{algorithm}


This algorithm requires only $|\phi|^{O(1)}$ space, because there are only
$O(\log{|\phi|})$ assignments to be stored during the process.
Suppose $T(N)$ is the running time on a decomposition with $N$ nodes. By \expref{Lemma}{lem:assignment_consistent_count}
\begin{equation*}
T(N)\leq O\left( d^{\tw(\phi)}\right) T\left({1\over 2}N\right)+|\phi|^{O(1)}
\end{equation*}
that is, $T(|\phi|)=O\left(d^{\tw(\phi)\log|\phi|}|\phi|^{O(1)}\right)$, where by the
normal form assumption $d=3$, \ie,
\[
T(|\phi|)=3^{\tw(\phi)\log|\phi|}|\phi|^{O(1)}\,.
\]








\subsection{Tradeoff algorithms}\label{subsec:trade_off}

We present a family of algorithms for bounded tree-width $\sat$ described in \expref{Algorithm}{alg:hybrid}. Different implementations of \textsc{Splitting Alg} (\expref{line}{line:splitting}) result in different algorithms. \textsc{SAT-tradeoff} is a procedure that takes a tree decomposition $\mathcal{T}$, a previous splitting node set $\mathcal{S}$, and an $\eps$-assignment group $\eps$-$\GR_{\mathcal{T}}$, and returns an array $M(\mathcal{T}, \eps$-$\GR_{\mathcal{T}})$ of $2^{\eps|\mathcal{S}|\tw(\phi)}$ entries, where the $i$th entry indicates whether the $i$-th assignment of $\eps$-$\GR_{\mathcal{T}}$ can be extended to a satisfying truth assignment. 

\begin{algorithm}[h]
\caption{\textsc{SAT-tradeoff}($\mathcal{T}$, $\mathcal{S}$, $\eps$-$\GR_{\mathcal{T}})$}
\label{alg:hybrid}
\begin{algorithmic}[1]
\State $M(\mathcal{T}, \eps$-$\GR_{\mathcal{T}}) \leftarrow$ all-zero array
\If {all nodes in $\mathcal{T}$ are in $\mathcal{S}$}
  \ForAll {$j:1\le j\le|\eps$-$\GR_{\mathcal{T}}|$}
  \State $R_{\mathcal{T}}$ $\leftarrow$ $j$th assignment in $\eps$-$\GR_{\mathcal{T}}$
    \If {every clause whose bit in $R_{\mathcal{T}}$ assigned $1$ is satisfied by some variable in ${\mathcal{T}}$}
      \State $M(\mathcal{T}, \eps$-$\GR_{\mathcal{T}})_{j} \leftarrow 1$
    \EndIf
  \EndFor
\Else
    \State split at \underline{\underline{\textsc{Splitting Alg}($\mathcal{T}$,  $\mathcal{S}$)}}, and denote the subtrees $\mathcal{T}_i$'s\label{line:splitting}\Comment{Replaceable}
  \ForAll {$\eps$-$\GR_{\mathcal{T}_i}$'s consistent with $\eps$-$\GR_\mathcal{T}$ by fixing $(1 - \eps)\tw(\phi)$ entries}
    \State $\forall i$, $M(\mathcal{T}_i, \eps$-$\GR_{\mathcal{T}_i}) \leftarrow\textrm{SAT-tradeoff}(\mathcal{T}, \mathcal{T}_i, \eps$-$\GR_{\mathcal{T}_i})$
  \ForAll {$j:1\le j\le|\eps$-$\GR_{\mathcal{T}}|$}
    \State $R_{\mathcal{T}}$ $\leftarrow$ $j$th assignment in $\eps$-$\GR_{\mathcal{T}}$
      \ForAll {$R_{\mathcal{T}_i}$'s chosen $\eps$-$\GR_{\mathcal{T}_i}$'s correspondingly}
        \If {$\forall i$, $M(\mathcal{T}_i,R_{\mathcal{T}_i}) = 1$ \textbf{and} $\forall \mathcal{T}_i$, $R_{\mathcal{T}_i}$'s are consistent with $R_{\mathcal{T}}$}
          \State $M(\mathcal{T}, \eps$-$\GR_{\mathcal{T}})_{j} \leftarrow 1$
        \EndIf
      \EndFor
    \EndFor
  \EndFor
\EndIf
\State \Return $M(\mathcal{T}, \eps$-$\GR_{\mathcal{T}})$
\end{algorithmic}
\end{algorithm}

A $type_{\ell}$ tree is a tree with $\ell$ previous splitting nodes. Let $\alpha$ be a parameter satisfying $0 < \alpha < 1/2$. The splitting algorithm $\mathcal{H}_2$ described in \expref{Algorithm}{alg:h2} has the property that it never creates a $type_{\ell}$ tree, for any $\ell\ge 3$.
\begin{figure}[ht]                                                        
\begin{center}                                                            
{\subfloat[]{\includegraphics[height=130pt]{algorithm_case_simple1.pdf}\label{subfig:simple_case1}}
\hspace{20pt}\subfloat[]{\includegraphics[height=130pt]{algorithm_case_simple3.pdf}\label{subfig:simple_case2}}
\hspace{20pt}\subfloat[]{\includegraphics[height=130pt]{algorithm_case_simple2.pdf}\label{subfig:simple_case3}}}
\end{center}                                                              
\caption{Choosing splitting node in three different cases. Rounding errors are ignored for simplicity.}\label{fig:algorithm_des3_simple}
\end{figure}     

\begin{algorithm}
\caption{$\mathcal{H}_2(\mathcal{T},\mathcal{S})$}\label{alg:h2}
\begin{algorithmic}[1]
\If {$\mathcal{T}$ with $\mathcal{S}$ is a $type_{0}$ tree}
\State \Return the $1/2$-splitting node
\ElsIf {$\mathcal{T}$ with $\mathcal{S}$ is a $type_{1}$ tree}
\State regard the previous splitting node as root
\State \Return the $\alpha$-splitting node  \Comment{\expref{Figure}{subfig:simple_case1}}
\ElsIf {$\mathcal{T}$ with $\mathcal{S}$ is a $type_{2}$ tree}
\State suppose $\mathcal{S}=\{p_1,p_2\}$
\State regard $p_1$ as root and compute the $1/2$-splitting node $q$
\If {$q$ is on the path between $p_1$ and $p_2$}
\State \Return $q$ \Comment{\expref{Figure}{subfig:simple_case2}}
\Else
\State \Return the least common ancestor of $q$ and $p_2$ \Comment{\expref{Figure}{subfig:simple_case3}}
\EndIf
\EndIf
\end{algorithmic}
\end{algorithm}

The performance of the tradeoff algorithms is not hard to analyze tightly (unlike the rather involved analysis of the two-parameter generalized tradeoff in \expref{Section}{sec:alg2}), and it is summarized in the following theorem.

\begin{theorem}\label{the:2d-time-complexity}
$\sat$ of tree-width $\tw(\phi)$ can be solved in simultaneously
\[
O\bigl(d^{1.441(1-\eps)\tw(\phi)\log {|\phi|}}|\phi|^{O(1)}\bigr)
\]
time and
\[
O\bigl(2^{2\eps\tw(\phi)}|\phi|^{O(1)}\bigr)
\]
space, where $\eps$ is a free
parameter, $0<\eps<1$.
\end{theorem}


\begin{proof}
Denote by $T_1(N)$, $T_2(N)$ the running time of \expref{Algorithm}{alg:h2} using
splitting rule
$\mathcal{H}_2$ on $type_{1}$ or $type_{2}$ trees each of $N$ nodes respectively.
Splitting a $type_{1}$ tree results in multiple $type_{1}$ trees
with size at most $(1 - \alpha) N$ and one $type_{2}$ tree with size
at most $\alpha N$, so we have
\[
T_{1}(N) \leq O(d^{(1-\eps)\tw(\phi)})\left(T_{1}\left((1 -
\alpha)N\right) + T_{2}\left(\alpha N\right)\right) +
2^{O(\tw(\phi))}\,.
\]
Splitting a $type_{2}$ tree, when the $1/2$-splitting is on the path between $p_1$ and $p_2$ results in two $type_{2}$ trees with size at most $N / 2$ and multiple $type_{1}$ trees. Otherwise, the splitting operation results in two $type_{2}$ trees with size at most $N / 2$ and several $type_{1}$ trees. Hence:
\[
T_{2}(N) \leq O(d^{(1-\eps)\tw(\phi)})\left(T_{1}(N) +
T_{2}(N / 2)\right) + 2^{O(\tw(\phi))}\,.
\]
Set $\alpha = \frac{3-\sqrt{5}}{2}$ to minimize the values of $T_1(N)$ and $T_2(N)$, we have
\begin{align*}
T_{1}(N) &\leq O(d^{(1-\eps)\tw(\phi)})\left(T_{1}\left((1 -
\alpha)N\right) + T_{2}\left(\alpha N\right)\right) +
2^{O(\tw(\phi))}\\
&\leq O(d^{(1-\eps)\tw(\phi)})T_{1}\left((1 - \alpha)N\right) +
O(d^{2(1-\eps)\tw(\phi)})T_{1}\left(\alpha N\right) +
2^{O(\tw(\phi))}\,.
\end{align*}
Therefore:
\[
T_{1}(N) \leq
d^{\frac{1}{-\log{(1-\alpha)}}(1-\eps)\tw(\phi)\log N}|\phi|^{O(1)}\,.
\]
Since $type_i$, $i\ge 3$ trees are not allowed, the space requirement is $2^{2\eps\tw(\phi)}|\phi|^{O(1)}$.
\end{proof}


\subsection{Optimality of the splitting algorithm for the single-parameter tradeoff}
The splitting algorithm presented above is a specific one, with the property that it  
does not create $type_i$ trees for any $i\ge 3$. 
Interestingly, it can be shown that this specific splitting algorithm is optimal over all splitting 
strategies which enjoy this property.

\begin{definition}
Denote by $\mathfrak{A}_c$ ($\forall c\ge 2$) the family of
algorithms for $\sat$ with bounded tree-width following the
framework in \expref{Algorithm}{alg:hybrid} which use a splitting
algorithm without creating $type_i$ trees $\forall i>c$.
\end{definition}

We lower bound the running time of all algorithms in
$\mathfrak{A}_2$ by showing hard instances based on generalizations of Fibonacci trees.

\begin{definition}
For any positive integer $h$, a \emph{$h$-Fibonacci tree}(denoted as
$F_{h}$) is a rooted tree recursively defined as following,
\begin{enumerate}[(1)]
\item if $h = 1$, $F_{h}$ contains only $1$ node;
\item if $h = 2$, $F_{h}$ contains $2$ nodes and one edge between them;
\item if $h > 2$, $F_{h}$ is constructed by a root connecting roots of two subtrees $F_{h-2}$ and $F_{h-1}$.
\end{enumerate}
An \emph{extended $(h,r)$-Fibonacci tree} (denote as $F^{*}_{h, r}$)
is constructed by adding one edge between a root node $r$ and the root
of subtree $F_{h}$.
\end{definition}

\begin{figure}[ht]                                                        
\begin{center}                                                            
\centering
{
\subfloat[$F_h$]{\includegraphics[height=80pt]{fib_tree_simple.pdf}}\hspace{50pt}
\subfloat[$F^*_{h,r}$]{\includegraphics[height=80pt]{fib_tree_simple_extended.pdf}}
}
\end{center}                                                              
\caption{Fibonacci tree and extended Fibonacci tree.}\label{fig:optimality_of_the_hybrid_simple}
\end{figure}     

In what follows, we focus on the structure of the trees and inspect the running time of an algorithm in $\mathfrak{A}_2$ on a formula with a tree decomposition with the specific structure, and omit the details of constructing a formula having tree decomposition of a certain structure here. Consider an extended $(h+2,r)$-Fibonacci tree $F^*_{h+2,r}$ with $N$ nodes, $h=\lceil\log_{(1+\sqrt{5})/2}{N}\rceil-2$. We prove that this is hard for any algorithms in $\mathfrak{A}_2$, namely,

\begin{theorem}\label{the:worst_case_bound_simple}
Every algorithm in $\mathfrak{A}_2$ runs in $\Omega\bigl(3^{1.441(1-\eps)\tw(\phi)\log N}|\phi|^{\Theta(1)}\bigr)$ time on $F^*_{h+2,r}$.
\end{theorem}

Before giving the proof of the theorem, we define two types of trees which appear in intermediate phases of the splitting algorithm and lower bound the running time on these trees: $\mathcal{T}_{1,h}$ (a special $type_1$ tree) is constructed by a splitting node connected to the root of a subtree $F_{h}$ (same shape as $F^*_{h,r}$, the node at the position of $r$ is a splitting node); and $\mathcal{T}_{2,h}$ (a special $type_2$ tree) is constructed by two separate splitting nodes connected to a node $r$ which roots a subtree $F^*_{h,r}$.

\begin{lemma}\label{lemma:t1t2}
Every algorithm in $\mathfrak{A}_2$ runs in $\Omega\bigl(3^{(1-\eps)\tw(\phi)h}|\phi|^{\Theta(1)}\bigr)$ time on $\mathcal{T}_{1,h}$, and runs on $\mathcal{T}_{2,h}$ in time $\Omega\bigl(3^{(1-\eps)\tw(\phi)(h + 1)}|\phi|^{\Theta(1)}\bigr)$.
\end{lemma}
\begin{proof}
The proof is by induction on $h$. Base cases are vacuous where $h\leq 2$.
Suppose the statement is true for any $h_0 < h$, consider the induction steps:
\begin{enumerate}[(1)]
\item For $\mathcal{T}_{1,h}$, if we split at the root of $F_h$, a
  $\mathcal{T}_{1,h-1}$ will be derived, the running time on which is
\[
\Omega\bigl(3^{(1-\eps)\tw(\phi)(h - 1)}|\phi|^{\Theta(1)}\bigr)\,;
\]
otherwise if we split at some node inside the subtrees $F_{h-1}$ or
$F_{h-2}$, the running time on the subtree containing two splitting
nodes (a new one and a previous one) is lower bounded by the running
time of a $\mathcal{T}_{2,h-2}$, which is 
\[
\Omega\bigl(3^{(1-\eps)\tw(\phi)((h - 2) + 1)}|\phi|^{\Theta(1)}\bigr)\,.
\]
To see this, assume for example that the splitting node $p$ is inside
the $F_{h-1}$. Imagine that all the nodes in $F_{h-1}$ except those on
the path between $p$ and the node $v$ which connects to the root of
$F_{h-2}$ are pruned for free, and then replace the path between $p$
and $v$ by an edge between them. A $\mathcal{T}_{2,h-2}$ is derived
this way, and note that the running time will not increase after the
procedure. Observe that enumerating all assignments for a newly
created splitting node requires time
\[
\Omega\bigl(3^{(1-\eps)\tw(\phi)}|\phi|^{\Theta(1)}\bigr)\,,
\]
so the running time for $\mathcal{T}_{1,h}$ is
\[
\Omega\bigl(3^{(1-\eps)\tw(\phi)h}|\phi|^{\Theta(1)}\bigr)\,.
\]
\item For $\mathcal{T}_{2,h}$, the splitting must occur at the node
  connecting the two splitting nodes, which creates a
  $\mathcal{T}_{1,h}$, the running time on which as shown above is
\[
\Omega\bigl(3^{(1-\eps)\tw(\phi)h}|\phi|^{\Theta(1)}\bigr)\,.
\]
Taking the time required for enumerating all assignments for the new
splitting node into consideration, the total running time for
$\mathcal{T}_{2,h}$ is therefore lower bounded by
\[
\Omega\bigl(3^{(1-\eps)\tw(\phi)(h+1)}|\phi|^{\Theta(1)}\bigr)\,.\qedhere
\]
\end{enumerate}
\end{proof}

\begin{proof}[Proof of \expref{Theorem}{the:worst_case_bound_simple}]
The very first step of splitting at any node of $F^*_{h+2,r}$ will
result in a $type_1$ tree, the running time on which is lower bounded
by the running time on $\mathcal{T}_{1,h}$. By
\expref{Lemma}{lemma:t1t2}, that is
\[
\Omega\bigl(3^{\frac{1}{-\log{(1-\alpha)}}{(1-\eps)\tw(\phi)\log N}}
|\phi|^{\Theta(1)}\bigr)\,,
\]
where
\[
N=\Theta\left(\left({\frac{1+\sqrt{5}}{2}}\right)^{h}\right)\,,\quad\text{and}\quad
\alpha=\frac{3-\sqrt{5}}{2}
\]
(which matches the parameter chosen in the tradeoff algorithm). By simplifying this expression we obtain the theorem.
\end{proof}

%
%
%
%


\section{Generalized two-parameter tradeoff algorithms} \label{sec:alg2}
%
%

In this section
we establish \expref{Theorem}{the:algorithm_complexity} below, by
exhibiting a family of algorithms that achieve time-space tradeoffs generalizing the algorithms in the 
previous section.
Each algorithm in this family is identified by the parameters $(\eps, c)$.
Moreover, we show that both of these parameters are necessary to
achieve different time-space tradeoffs. Intuitively, parameter $0<\eps<1$
corresponds to the granularity of the discretization of the
assignment space, whereas the integer parameter $c\geq 2$ has to do
with the ``complexity'' of the rule applied recursively during the truth assignment search.
\begin{theorem}\label{the:algorithm_complexity}
For every integer $c\ge 2$ and $\eps$, where $0<\eps<1$, a $\sat$
instance $\phi$ with a tree decomposition of width $\tw(\phi)$ and
$N$ nodes, can be decided in time-space
\[
\left(3^{\left(\lambda_{c}(\log N - c) +
c\right)(1-\eps)\tw(\phi)}|\phi|^{O(1)},\;\;
2^{c\eps\tw(\phi)}|\phi|^{O(1)}\right)
\]
for a constant $\lambda_c$.
\end{theorem}

$\lambda_c$ is a constant depending on $c$. To be more specific,
$\lambda_c$ is defined as $-\log{x_c}$, where $x_c$ is the root with
largest absolute value of the polynomial equation:
$X^c-X^{c-1}-X^{c-2}-\dots-1=0$.  The first few values of $\lambda_c$ for small $c$'s are listed in \expref{Table}{fig:lambda_c}.

\begin{table}[h]
\centering
\begin{tabular}{cccccc}
\toprule
$c$&2&3&4&5&6\\
\midrule
$\lambda_c$&1.441&1.138&1.057&1.026&1.013\\
\bottomrule
\end{tabular}
\caption{Values of $\lambda_c$ for small $c$'s.}
\label{fig:lambda_c}
\end{table}


\subsection{Generalized tradeoff algorithms}
We have already seen a tradeoff algorithm which avoids $type_i$ trees for $i\geq 3$. 
It is natural to ask if the algorithm can be generalized to allow up
to $type_c$ trees for any fixed $c\ge 2$, and more importantly if by doing so there is any gain
in the running time (clearly, there will be a loss in the space). 
Indeed, this is possible and as $c$ increases the running time decreases 
while the space requirement increases.

First, we generalize the splitting algorithm to allow
$type_i$ trees for $i$ up to $c$. For arbitrary $1\leq i\leq c$,
consider splitting a $type_{i}$ tree: suppose the splitting node is
$p$. If $p$ is on the path between some pair of previous splitting
nodes, splitting at this node results in several $type_{j}\; (j\leq i)$
trees; otherwise, splitting results in several $type_{1}$ trees
and one $type_{i+1}$ tree. Formally, we devise an algorithm $\mathcal{H}_c$, 
such that when splitting a $type_{i}$ tree, we invoke $\mathcal{H}_c$ to determine the splitting
node. This is an implementation of \textsc{Splitting Alg} in \expref{Algorithm}{alg:hybrid}.


\begin{algorithm}
\caption{$\mathcal{H}_c(\mathcal{T},\mathcal{S})$}
\begin{algorithmic}[1]
\If {$\mathcal{T}$ with $\mathcal{S}$ is a $type_{0}$ tree}
    \State \Return the $1/2$-splitting node
\Else
    \State suppose $\mathcal{T}$ with $\mathcal{S}$ is a $type_{i}$ tree
    \If {$|\mathcal{T}|\le 2^{c - i}$}
        \State \Return the $1/2$-splitting node
    \Else
        \State pick an arbitrary node from $\mathcal{S}$ as root and compute the $\alpha_{c,i}$-splitting node $q_1$
        \If {$q_1$ is \emph{not} on the path between any pair in $\mathcal{S}$}
            \State \Return $q_1$ \Comment{\expref{Figure}{subfig:case1}}
        \Else
            \State compute a $1/2$-splitting node $q_2$.
            \If {$q_2$ is on the path between any pair in $\mathcal{S}$}
                \State \Return $q_2$ \Comment{\expref{Figure}{subfig:case2}}
            \Else
                \State \Return the least common ancestor of $q_2$ and all nodes in $\mathcal{S}$ \Comment{\expref{Figure}{subfig:case3}}
            \EndIf
        \EndIf
    \EndIf
\EndIf
\end{algorithmic}
\end{algorithm}

\begin{figure}[ht]                                                        
\begin{center}                                                            
{\subfloat[]{\includegraphics[height=130pt]{algorithm_case1.pdf}\label{subfig:case1}}
\hspace{20pt}\subfloat[]{\includegraphics[height=130pt]{algorithm_case3.pdf}\label{subfig:case2}}
\hspace{20pt}\subfloat[]{\includegraphics[height=130pt]{algorithm_case2.pdf}\label{subfig:case3}}}
\end{center}                                                              
\caption{Choosing splitting node for a $type_i$ tree ($i=2$ here) in three different cases. Rounding errors are ignored for simplicity.}\label{fig:algorithm_des3}
\end{figure}     

Each $\alpha_{c, i}$ for any $1\leq i< c$ is a parameter satisfying
$0\le\alpha_{c,i}\le 1 / 2$. To prevent $type_{c + 1}$ trees,
splitting node of a $type_{c}$ tree must be on the path between some
pair of previous splitting nodes, this is assured by setting
$\alpha_{c, c} = 0$. For a fixed $c$, the running time and space of
the algorithm solving $\sat$ of bounded tree-width utilizing the
splitting algorithm $\mathcal{A}$ are summarized in
\expref{Theorem}{the:algorithm_complexity} (see page~\pageref{the:algorithm_complexity}).

We introduce the following notation in order to discuss the splitting depth. 

\begin{definition}\label{def:cutting_depth}
The \emph{$c$-splitting depth} $\mathsf{SD}_{c}(\mathcal{A},
\mathcal{T}, S)$ of a \emph{splitting algorithm} $\mathcal{A}$ on
tree $\mathcal{T}$ with previous splitting nodes $S$ is inductively defined as
follows (where the case for $|S|>c$ is arbitrary):
\begin{eqnarray*}
\mathsf{SD}_c(\mathcal{A}, \mathcal{T}, S)=
\begin{cases}
  \max_{(\mathcal{T}_{0}, S_{0})\in C_{\mathcal{T}, S, p}}\mathsf{SD}_c(\mathcal{A}, \mathcal{T}_{0}, S_{0}) + 1 	& |S|\le c, |S|<|\mathcal{T}|\,,\\
0 &|S|\le c, |S|=|\mathcal{T}|\,,\\
\infty &|S|>c\,,
\end{cases}
\end{eqnarray*}
where $p$ is the output of $\mathcal{A}$ on $\mathcal{T}$ and $S$, $C_{\mathcal{T}, S, p}$ is
the set of subtrees by splitting at $p$ in tree $\mathcal{T}$ with
previous splitting nodes $S$.

We define the \emph{$c$-minimum splitting depth}
$\mathsf{minSD}_c(\mathcal{T}, S)$ to be the minimum value of
$\mathsf{SD}_c(\mathcal{A}, \mathcal{T}, S)$, over all splitting
algorithms.
\end{definition}

Under this notation, given a tree $\mathcal{T}$, any algorithm $\mathcal{A}$ avoiding
$type_{c+1}$ trees requires time
\[
d^{(1-\eps)\mathsf{SD}_{c}(\mathcal{A}, \mathcal{T},
\emptyset)\tw(\phi)}|\phi|^{O(1)}
\]
and space
\[
2^{c\eps\tw(\phi)}|\phi|^{O(1)}\,.
\]
In fact, bounding the running time is a non-trivial issue (the derived recurrences are in a ``perplexed'' form).
The proof of \expref{Theorem}{the:algorithm_complexity} follows by two technical lemmas: 
\expref{Lemma}{lem:algorithm_complexity} establishes the recurrences according to the recursive algorithm, 
and \expref{Lemma}{lem:algorithm_complexity2} deals with choice of parameters. 
For simplicity of presentation we ignore issues regarding the divisibility of $N$ by $2$. 

\begin{lemma}\label{lem:algorithm_complexity}
For every $c\geq 2$, any tree $\mathcal{T}$ with $N$ nodes and splitting
node set $S$ of size $i$, let 
\[
D_{c, i}(N) = \max_{\mathcal{T}, S}
\mathsf{SD}_{c}(\mathcal{H}_c,\mathcal{T}, S)\,.
\]
Then,
\[
\begin{cases}
D_{c, i}(N) \leq \max\{D_{c,1}\left((1 - \alpha_{c, i})N\right), D_{c,i + 1}\left(\alpha_{c, i}N\right), D_{c,i}\left(N / 2\right)\}+ 1&\forall i:1 \leq i < c\,,\\[1ex]
D_{c, c}(N) \leq \max\{D_{c,1}(N) , D_{c,c}(N / 2)\} + 1\,.&
\end{cases}
\]
\end{lemma}

\begin{proof}
Without loss of generality, suppose $N\geq 2^{c}$. Consider
splitting a $type_{i}$ tree with splitting nodes $S$, $1\leq i<c$.
If the $\alpha_{c, i}$-splitting-node $m$ is not on the path between
any pair of previous splitting nodes, splitting at $m$ will result
in multiple $type_1$ trees of size at most
$\lceil(1-\alpha_{c,i})N\rceil$ and one $type_{i+1}$ tree of size at
most $\lceil{\alpha_{c,i}N}\rceil$. Otherwise, since
$1-\alpha_{c,i}\geq 1/2$, the maximal possible size of a $type_1$ tree
created by any splitting node will not exceed
$\lceil{(1-\alpha_{c,i})N}\rceil$. Splitting at the
$1/2$-splitting-node $c$ will result in multiple $type_{j}(j\leq i)$
trees of size at most $\lceil{N/2}\rceil$, otherwise, splitting at
the least common ancestor of $c$ and all previous splitting nodes as
$p$, will result in multiple $type_{1}$ tree of size at most
$\lceil{(1 - \alpha_{c, i})N}\rceil$ and many $type_{j}(j\leq i)$
trees with size at most $\lceil{N/2}\rceil$. In summary,
$$D_{c,i}(N) \leq \max\{D_{c,1}\left((1 - \alpha_{c, i})N\right), D_{c,i
+ 1}\left(\alpha_{c, i}N\right), D_{c,i}\left(N / 2\right) \} + 1\,.$$

Now, consider splitting a $type_{c}$ tree with splitting nodes $S$.
Since $\alpha_{c, c} = 0$, we always ignore the $(1 - \alpha_{c,
i})$-splitting-node $m$. Splitting at the $1/2$-splitting-node $c$
will result in multiple $type_{j}(j\leq i)$ trees of size at most
$\lceil{N/2}\rceil$. Splitting at the least common ancestor of $c$
and all previous splitting nodes will result in multiple $type_{1}$
tree with size at most $N$ and multiple $type_{j}(j\leq i)$ trees
with size at most $\lceil{N/2}\rceil$, namely: 
\[
D_{c, c}(N) \leq \max\{D_{c, 1}(N) , D_{c, c}(N / 2)\} + 1\,.\qedhere
\]
\end{proof}

\begin{lemma}\label{lem:algorithm_complexity2}
$\mathsf{SD}_c(\mathcal{H}_2,\mathcal{T},\emptyset)$ for a tree $\mathcal{T}$ of $N$ nodes is at most $\lambda_{c}(\log N - c) + c + O(1)$, with properly chosen parameters $\alpha_{c,i}$'s.
\end{lemma}

\begin{proof}

For ease of computation, we define a function $D'$ independent of $D$, as a recurrence that satisfies the recursion that, by \expref{Lemma}{lem:algorithm_complexity}, holds for the running time.
\[
\begin{cases}
D'_{c,i}(N)=D'_{c,1}((1 - \alpha_{c,i}) N) + 1 = D'_{c,i + 1}(\alpha_{c,i}N) + 1&\forall i: 1\le i<c\,,\\[1ex]
D'_{c,c}(N)=D'_{c,1}(N) + 1\,.
\end{cases}
\]
By manipulating the first equation, we can derive that
\begin{align*}
&D'_{c,1}((1-\alpha_{c,i})N)=D'_{c,i+1}(\alpha_{c,i}N)&&\forall i:1\le i<c\\
\Rightarrow\quad&D'_{c,1}((1-\alpha_{c,i})/\alpha_{c,i} N)=D'_{c,i+1}(N)&&\forall i:1\le i<c\\
\Rightarrow\quad&D'_{c,1}((1-\alpha_{c,i-1}/\alpha_{c,i-1} N)=D'_{c,i}(N)&&\forall i:1<i\le c\,.
\end{align*}
Again, by the first equation, for each $1\leq i< c$,
\[
D'_{c,i}(N) = D'_{c,i+1}(\alpha_{c,
i}N) + 1 = D'_{c,1}(\alpha_{c, i}(1 - \alpha_{c, i + 1})N) + 2\,,
\]
thus
\begin{align*}
D'_{c,1}(N) = D'_{c,1}(\alpha_{c, i}(1 - \alpha_{c, i + 1}) / (1 - \alpha_{c, i})N)+2&&&\forall i:1\le i<c\,.
\end{align*}
Consider minimizing the values of $D'_{c,1}$. Since $D'_{c,1}(N) =
D'_{c,1}((1 - \alpha_{c, 1})N) + 1$, we let 
\[
1 - \alpha_{c, 1} = \alpha_{c, i}\frac{1 - \alpha_{c, i + 1}}{1 -
\alpha_{c, i}}\,.
\]
By rearranging, 
\[
\alpha_{c, i + 1} = 1 - \frac{(1 - \alpha_{c,
1})(1 - \alpha_{c, i})}{\alpha_{c, i}}
\]
holds. Inductively, the following can be proved
\begin{align*}
&\alpha_{c, i} = 1 - \frac{\alpha_{c, 1}(1-\alpha_{c, 1})^{i}}{2\alpha_{c, 1} -
1 + (1 - \alpha_{c, 1})^{i}}&&\forall i:1\le i\le c\,.
\end{align*}
Now look at the boundary conditions, since
\[
D'_{c,c}(N) = D'_{c,1}(N) + 1 = D'_{c,1}\cdot\frac{(1 -
\alpha_{c, c-1})N}{\alpha_{c, c-1}}\,.
\]
Again, to minimize the values of $D'_{c,1}$, let 
\[
\frac{\alpha_{c, c-1}}{1
- \alpha_{c, c}} = 1 - \alpha_{c, 1}\,, \qquad\text{and therefore}\qquad \alpha_{c, c-1} = \frac{1 -
\alpha_{c, 1}}{2 - \alpha_{c, 1}}\,.
\]
By what is shown above, 
\[
\frac{1 - \alpha_{c,
1}}{2 - \alpha_{c, 1}} = 1 - \frac{\alpha_{c, 1}(1-\alpha_{c,
1})^{c - 1}}{2\alpha_{c, 1}- 1 + (1 - \alpha_{c, 1})^{c - 1}}\,,
\]
which implies
\[
\sum_{i=1}^{c}(1 - \alpha_{c, 1})^{i} = 1\,.
\]
We choose $\alpha_{c,1}= \alpha^*_{c,1}$ to be a solution of the equation above, and then all the other $\alpha_{c,i}$'s can be fixed. By setting $\lambda_{c} = {1}/{\log (1 - \alpha^*_{c, 1})}$, for
each $1\leq i\leq c$, $D'_{c,i}(N) \geq D'_{c,i}(N / 2) + 1$. We get
\[
\begin{cases}
D'_{c,i}(N)=\max\{D'_{c,1}((1-\alpha_{c, i}) N), D'_{c,i+1}(\alpha_{c, i}N), D'_{c,i}(N/2)\} + 1&\forall i: 1\le i<c\,,\\[1ex]
D'_{c,c}(N)=\max\{D'_{c,1}(N), D'_{c,c}(N/2)\} + 1\,.
\end{cases}
\]
Note that $D'$ is defined in a way that it satisfies the recursion in \expref{Lemma}{lem:algorithm_complexity}, and it can be proved by induction that
$D'_{c,i}(N)$ upper bounds $D_{c,i}(N)$ for all $c,i$. By the choice of the parameters, the recurrence can be solved using standard tools. Specifically,
\[
D_{c,1}(N) \leq D'_{c,1}(N) \leq \lambda_{c}(\log N - c) +
D_{c,1}(2^{c})+ O(1)\,.
\]
Since $D_{c,1}(2^c) = c$, $\mathsf{SD}_c(\mathcal{H}_c, \mathcal{T}, S)$ is
upper bounded by $\lambda_{c}(\log N - c) + c + O(1)$, where
$\lambda_{c}$ satisfies 
\[
\sum_{\ell=1}^{c}2^{-\frac{\ell}{\lambda_{c}}} =
1\,.\qedhere
\]
\end{proof}

\begin{proof}[Proof of \expref{Theorem}{the:algorithm_complexity}]
For every $c \geq 2$, we solve the above recurrences: when $N <2^{c}$, the running time is
\[
d^{\log N (1-\eps)\tw(\phi)}|\phi|^{O(1)}\,;
\]
when $N \ge 2^{c}$, the running time is
\[
d^{\left(\lambda_{c}(\log N - c) + c\right)
  (1-\eps)\tw(\phi)}|\phi|^{O(1)}\,.
\]
Space required by the algorithm is upper bounded by $2^{c\eps\tw(\phi)}|\phi|^{O(1)}$ since only $type_i$ trees are allowed, for $i\le c$.
\end{proof}

The value $\lambda_c$ depending on the choice of parameter $c$ seems quite artificial in the analysis of our algorithms, but later we will see that this constant is actually tight. Here is an upper bound on $\lambda_c$.
\begin{lemma}\label{lem:bound_of_lambda}
$\displaystyle \lambda_c<1+\frac{2}{2^{c/2}}$\,.
\end{lemma}
\begin{proof}
Let $f(X)=X^{c}-\sum_{i=0}^{c-1}{X^{i}}$, and let $\gamma_{c}$ be the
root of $f(X)=0$ with largest absolute value. We know $f(2)=1>0$, so
if we can prove $f(2-{1}/{2^{c/2}})<0$ then there must be a
root between 2 and $2-{1}/{2^{c/2}}$. Denote
$y=2-{1}/{2^{c/2}}$,
\begin{eqnarray*}
f(y)<0\iff y^{c}<\sum_{i=0}^{c-1}{y^{i}}=\frac{y^{c}-1}{y-1}\iff y<2-\frac{1}{y^c}\,.
\end{eqnarray*}
The last inequality is true because
$y=2-{1}/{2^{c/2}}>\sqrt{2}$ when $c\ge2$ and
$2-{1}/{y^c}>2-{1}/{\sqrt{2}^{c}}=y$. By
definition of $\lambda_c= {1}/{\log_{2}{\gamma_{c}}}$, it follows that
$\lambda_c<1+{2}/{2^{c/2}}$.
\end{proof}

Given the above upper bound, we can furthermore prove an interesting feature of our family of algorithms. 
Namely, the space resource can be fully exploited to minimize the running time, which potentially is of 
practical importance.

\begin{corollary}[of \expref{Theorem}{the:algorithm_complexity}]\label{cor:hybrid_opt_space}
For any $\eps'>0$ there exists an algorithm which runs in space
$2^{\eps'\tw(\phi)}|\phi|^{O(1)}$ and time
$d^{\delta\tw(\phi)\log_{2}{|\phi|}}|\phi|^{O(1)}$ for a constant
$\delta<1$.
\end{corollary}

\begin{proof}
For any fixed $\eps$ and $c$, there is an
algorithm with running time
\[
O\bigl(d^{\lambda_{c}(1-\eps)\tw(\phi)\log{|\phi|}}|\phi|^{O(1)}\bigr)
\]
and space
$O(2^{c\eps\tw(\phi)}|\phi|^{O(1)})$ by \expref{Theorem}{the:algorithm_complexity}. Set
$\eps={\eps'}/{c}$, then the space is
$O(2^{\eps'\tw(\phi)}|\phi|^{O(1)})$ and the running time is
\[
O\bigl(d^{\lambda_{c}(1-\frac{\eps'}{c})\tw(\phi)\log{|\phi|}}|\phi|^{O(1)}\bigr)\,.
\]
By \expref{Lemma}{lem:bound_of_lambda},
\[
\lambda_{c}\left(1-\frac{\eps'}{c}\right)<\left(1+\frac{2}{2^{c/2}}\right)\left(1-\frac{\eps'}{c}\right)<1
\]
for sufficiently large $c$.
\end{proof}

\subsection{Optimality of the generalized tradeoff algorithm}
Similarly to the last part of \expref{Section}{sec:alg}, we also prove the optimality of the generalized tradeoff algorithm. 
However, in this case the matching lower bound is more involved (since the upper bound involved a lot of guessing).
We construct the hard instance using extended generalized Fibonacci trees.

\begin{definition}
For any integer $c\ge 2$, and positive integer $h$, a \emph{$(c,
h)$-Fibonacci tree}(denoted as $F_{c,h}$) is a rooted tree defined by one of
the rules,
\begin{enumerate}[(1)]
\item if $h\le c$, $F_{c,h}$ is a chain of $2^c$ nodes;
\item if $h>c$, $F_{c,h}$ is constructed by starting from a chain of $c$ nodes (one end as the root), then replacing the $i$th node (starting from the root) by a subtree $F_{c,h-i}$.
\end{enumerate}
An \emph{extended $(c,h,r)$-Fibonacci tree} (denote as $F^{*}_{c, h,
r}$) is constructed by connecting one root node $r$ to a subtree
$F_{c, h}$.
\end{definition}

See \expref{Figure}{fig:optimality_of_the_hybrid} for an illustration of a $(c,h)$-Fibonacci tree. $F_{c,h+c}$ is indeed the hard instance for splitting algorithms in $\mathfrak{A}_c$ for $c\ge 2$. As discussed previously, it suffices to lower bound $\mathsf{minSD}$ on this tree.

\begin{figure}[ht]                                                        
\begin{center}                                                            
\subfloat[$F_{c,h}$]{\includegraphics[width=150pt]{fib_tree_new.pdf}\label{fig:optimality_of_the_hybrid}}
\hspace{40pt}\subfloat[$F^*_{c,h,r}$]{\hspace{4pt}\includegraphics[width=31pt]{fib_tree_new_extended.pdf}\hspace{4pt}} \hspace{40pt}\subfloat[$G_{c, h, w}$]{\includegraphics[width=150pt]{worst_case_proof.pdf}\label{fig:worst_case_proof}}

\end{center}                                                              
\caption{Fibonacci tree in a more general form and the hard instance based on it.}
\end{figure}     

Similar to the proof of \expref{Theorem}{the:worst_case_bound_simple}, we need a definition of trees which may appear in intermediate phases and contain previous splitting nodes.
$\forall c\geq 2$, $\forall h > c$ and $\forall w:1 \leq w \leq c$, $G_{c, h,
w}$ is such a tree: first construct a chain of length $w$, then connect $c - w + 1$ previous splitting nodes to the first node of the chain, and $\forall i:1\le i\le w$, connect a subtree $F_{c, h - c + w - i}$ to the $i$-th node of the chain. Denote $S_{\ell}$ as the set of the $\ell$ previous splitting nodes connected to the first node of the chain. The following bound holds for these intermediate trees.
\begin{lemma}\label{lemma:minsd_bound}
$\forall h\ge 1, \forall w:1\le w\le c$, $\mathsf{minSD}(G_{c, h, w}, S_{c - w + 1})\geq h - c + w$.
\end{lemma}
\begin{proof}
We prove the lemma by induction on $h$. The base case is
trivial. Suppose $\forall h:h < h_0$,
\[
\mathsf{minSD}_c(G_{c, h, w},S_{c
- w + 1})\geq h - c + w
\]
holds for any valid $w$. For the induction step, we prove 
\begin{eqnarray}
\mathsf{minSD}_c(G_{c, h_0,w},S_{c-w+1})\geq h_0 - c + w\label{formula:double_induction}
\end{eqnarray}
holds for any $w$ by induction on $w$. When $w = 1$, to
prevent $type_i$ trees for $i > c$, we must split at the first node
of the chain. By induction hypothesis (on $h$),
\[
\mathsf{minSD}_{c}(G_{c, h_0, 1}, S_{c}) \ge 1
+ \mathsf{minSD}_{c}(G_{c, h_0 - c, c}, S_{1}) \geq h_0 - c + 1\,.
\]
Suppose \eqref{formula:double_induction} holds $\forall w: w<w_0$, for
the induction step, consider lower bounding 
\[
\mathsf{minSD}_c(G_{c, h_0,w_0},S_{c-w_0+1})\,.
\]

As in the proof of \expref{Lemma}{lemma:t1t2}, in order to apply the
induction hypothesis, some size-reducing procedure which will not
increase the running time will be applied to the tree after
splitting. If the splitting node is inside the subtree $F_{c, h_0 - c
  + w_0 - 1}$,  prune the nodes in the subtree $F_{c,h_0-c+w_0-1}$
outside the path between the first node on the chain and the splitting
node, then shrink the path to an edge, and finally shrink the first
edge on the chain to obtain a $G_{c,h_0,w_0-1}$, by induction
hypothesis,
\[
\mathsf{minSD}_{c}(G_{c, h_0, w_0 - 1}, S_{c - (w_0 -1) + 1})\ge h_0 -
c + w_0-1\,;
\]
otherwise consider an additional free splitting at the first node on
the chain, this produces a $G_{c,h_0-c+w_0-1,c}$, again by induction
hypothesis ($h_0-c+w_0-1<h_0$), 
\[
\mathsf{minSD}_{c}(G_{c, h_0 - c + w_0 - 1, c}, S_{1}) = h_0 - c +
w_0-1 -c + c=h_0-c+w_0-1\,.
\]
Therefore, 
\[
\mathsf{minSD}_{c}(G_{c, h_0, w_0}, S_{c - w_0 + 1}) \ge
1+h_0-c+w_0-1=h_0-c+w_0\,.
\]
This completes both inductions and also the proof.
\end{proof}

\begin{corollary}\label{cor:worst_case_bound}
For each $h\geq 1$, $\mathsf{minSD}(F^{*}_{c, h, r}, \{r\}) \ge h$.
\end{corollary}

\begin{proof}
By \expref{Lemma}{lemma:minsd_bound}, $\mathsf{minSD}_{c}(F^{*}_{c, h, r},\{r\}) = \mathsf{minSD}_{c}(G_{c, h, c},S_{1})\geq h - c + c \geq h$.
\end{proof}

Now we are ready to state the theorem for optimality.
\begin{theorem}\label{the:worst_case_bound}
For every $c\geq 2$ and $N > 2^c$, there exists a tree $\mathcal{T}$
with $N$ nodes, such that 
\[
\mathsf{minSD}_c(\mathcal{T}, \emptyset)\ge \lambda_{c} (\log N - c) +
c - O(1)\,.
\]
\end{theorem}

\begin{proof}
Let $|F_{c, h}|$ be the number of nodes in the tree $F_{c,
h}$. For any $h\leq c$, we have $|F_{c, h}|\leq 2^{c}$, when $h
> c$, we have $|F_{c, h}| = \sum_{i = 1}^{c}|F_{c, h - i}| + c$. By the recursion,
the generating function of $|F_{c, h}|$ can be written as $f(X) = X^{c}
- \sum_{i=0}^{c}{X^{i}}$. Therefore 
\[
|F_{c, h}| = \sum_{i =
1}^{c}{\delta_{c, i}\gamma_{c, i}^{h - c}}\,,
\]
where $\delta_{c,i}$ is
upper bounded by a constant times $2^{c}$ and $\gamma_{c, i}$ is the $i$-th
root of the equation $f(X) = 0$.

Let $\gamma_{c} = \arg\max_i\{|\gamma_{c,i}|\}$. When $h$ tends to
infinity, $|F_{c, h}| = \Theta(2^{c}\gamma_{c}^{h - c})$. So, 
\[
h
\geq \log_{\gamma_{c}}{\left({|F_{c, h}| / 2^{c}}\right)} + c - O(1)
= \lambda_{c}(\log{|F_{c, h}|} - c) + c - O(1)\,.
\]
Therefore, for any
$c\geq 2$ and large enough $N$, consider the tree $\mathcal{T}=F_{c,h+c}$ with $\ge N$
nodes. Splitting it at any node will result in a tree, whose minimum splitting depth is lower bounded by $\mathsf{minSD}(F^{*}_{c, h, r}, \{r\})$: if the splitting node is on the chain, then let $r$ be the splitting node; otherwise let $r$ be any node on the chain other than the one which is connected to the root of the subtree where the splitting node lay. (One can think of as splitting at $r$ for free.) This, when combining with \expref{Corollary}{cor:worst_case_bound}, completes the proof.
\end{proof}

Similarly to \expref{Theorem}{the:worst_case_bound_simple}, here we conclude
the optimality of our tradeoff algorithm. 
That is, for fixed $c\ge 2$, $\forall\eps: 0<\eps<1$, and every
sufficiently large input length and every algorithm $\mathfrak{A}_c$
(whose description may depend on the length) there is an instance
$\phi$, for which the running time is \[
\Omega\bigl(3^{\lambda_{c} (\log |\phi| - c) + c -
  O(1)}|\phi|^{\Theta(1)}\bigr)\,.
\]

\iffalse
\subsection{An algorithm optimal in our framework}
As mentioned in \expref{Remark}{rem:time_and_depth}, for fixed $c\ge 2$,
an optimal splitting algorithm, \ie, with smallest splitting depth
implies an optimal algorithm in $\mathfrak{A}_c$. Indeed, the
following lemma assures that such an optimal splitting algorithm can
be computed in quasi-polynomial time.

\begin{lemma}\label{lem:search_splitting_depth}
For a tree T with N nodes, $\mathsf{minSD}_{c}(T,\emptyset)$ can be
computed in time $O\left(N^{\mathsf{minSD}_{c}(T,
\emptyset)+O(1)}\right)$ and polynomial space.
\end{lemma}
\begin{proof}
For any $h$, whether $\mathsf{minSD}_{c}(T, \emptyset)\leq h$ in
$N^{d}$ can be tested by a branch-and-bound algorithm. For any tree $T$ and
previous splitting nodes $S$, enumerate all nodes and check
whether the minimal splitting depth of each subtree is at most $h-1$
recursively. The maximal depth of the recursion is set to $h$, thus the
running time is $O\left(N^{h}\right)$. Therefore, the overall
time is at most $O\left(N^{\mathsf{minSD}_{c}(T, \emptyset)+O(1)}\right)$. The
required space is polynomial.
\qed
\end{proof}

By applying the splitting algorithm in the previous lemma we obtain the following tradeoff algorithm.

\begin{theorem}\label{the:optimal_hybrid}
For any $c\geq 2$, any $\eps$ satisfying $0<\eps<0$, the
hybrid algorithm can be done in time
$d^{(1-\eps)\mathsf{minSD}_{c}(T, \emptyset)\tw(\phi)}|\phi|^{O(1)}$ and
space $2^{c\eps\tw(\phi)}|\phi|^{O(1)}$.
\end{theorem}
\fi


\section{Future work}\label{sec:conclusion}
%
A very exciting research direction is to unconditionally verify our conjecture in 
restricted models of computation---propositional proof complexity lower bounds can be 
understood as such results. The work of Beame-Beck-Impagliazzo~\cite{BBI} took the 
first step towards this direction. Such results can be also understood as partial progress 
towards $\SC\neq\nc$.

A rather intriguing direction regarding positive results, is to use randomness in order to 
improve the multiplicative constants in the exponents of time or space, or to provide
improved tradeoffs. More generally, we would like to understand the role of randomness
in width-parameterized $\sat$-solving, a topic which is fundamentally unexplored.

\section*{Acknowledgments}
We would like to thank Hubie Chen, Kevin Matulef and Alexander Razborov for useful
remarks and suggestions. 

\bibliographystyle{tocplain}   %
%
%
%
%
\bibliography{v010a012}

%
%
%
%
\begin{tocauthors}
\begin{tocinfo}[allender]
Eric Allender\\
 Distinguished professor\\
 Rutgers University, New Brunswick, NJ\\
 allender\tocat{}cs\tocdot{}rutgers\tocdot{}edu \\
 \url{http://www.cs.rutgers.edu/~allender}
\end{tocinfo}
\begin{tocinfo}[chen]
  Shiteng Chen\\
  \phd\ student\\
  Institute for Interdisciplinary Information Sciences\\
  Tsinghua University\\
  shitengchen\tocat{}gmail\tocdot{}com\\
  \url{http://iiis.tsinghua.edu.cn/shitengchen}
\end{tocinfo}
\begin{tocinfo}[lou]
  Tiancheng Lou\\
  Software engineer\\
  Google Mountain View\\
  tiancheng\tocdot{}lou\tocat{}gmail\tocdot{}com\\
  \url{http://iiis.tsinghua.edu.cn/tianchenglou}
\end{tocinfo}
\begin{tocinfo}[papakonstantinou]
  Periklis A. Papakonstantinou\\
  Assistant professor\\
  Institute for Interdisciplinary Information Sciences\\
  Tsinghua University\\
  papakons\tocat{}tsinghua\tocdot{}edu\tocdot{}cn\\
  \url{http://iiis.tsinghua.edu.cn/~papakons}
\end{tocinfo}
\begin{tocinfo}[tang]  %
  Bangsheng Tang\\
  Associate researcher \\
  Hulu, Beijing Office \\
  bangsheng\tocdot{}tang\tocat{}gmail\tocdot{}com\\
%
  \url{http://tang.bangsheng.info}
\end{tocinfo}
\end{tocauthors}

%
%
%
%
%
%
%
%
%
%
%
%
%
%
\begin{tocaboutauthors}
\begin{tocabout}[allender]
\textsc{Eric Allender} 
is a professor at \href{http://www.cs.rutgers.edu}{Rutgers University}.  He 
has been at Rutgers since receiving his \phd\ in 1985 at 
\href{http://gatech.edu}{Georgia Tech}, under the supervision of 
\href{http://www2.gsu.edu/~matknk}{Kim N. King}.  While at Georgia Tech, he 
was the Backbone of the 
\href{http://seedandfeed.org}{Seed and Feed Marching Abominable} and he still 
plays trombone from time to time.  He did his undergraduate work at the 
\href{http://www.uiowa.edu}{University of Iowa}.  He is a 
\href{http://fellows.acm.org}{Fellow of the ACM}, and currently serves as 
Editor-in-Chief of 
\href{http://toct.acm.org}{ACM Transactions on Computation Theory}.  
Circuit complexity, Kolmogorov complexity, and complexity classes are his 
main research interests.  He and his wife find happiness on the dance floor 
and toiling in their garden.
\end{tocabout}
\begin{tocabout}[chen]
\textsc{Shiteng Chen} is currently a \phd\ student at the
  \href{http://iiis.tsinghua.edu.cn}{Institute for Interdisciplinary 
Information Sciences}, 
\href{http://www.tsinghua.edu.cn}{Tsinghua University},
advised by Periklis Papakonstantinou. %
He did his undergraduate studies in the pilot computer
science
%
program at Tsinghua University, 
the ``Yao class.''  
\end{tocabout}
\begin{tocabout}[lou]
\textsc{Tiancheng Lou} is currently with Google.
%
%
He received his \phd\ in 2012
from the \href{http://iiis.tsinghua.edu.cn}{Institute for 
Interdisciplinary Information Sciences}, 
\href{http://www.tsinghua.edu.cn}{Tsinghua
    University} under the supervision of Professor
\href{http://iiis.tsinghua.edu.cn/yao/}{Andrew C. Yao}. 
He holds numerous programming contest awards. 
\end{tocabout}

\begin{tocabout}[papakonstantinou]
\textsc{Periklis A. Papakonstantinou} is an assistant professor at the
\href{http://iiis.tsinghua.edu.cn}{Institute for Interdisciplinary
Information Sciences},
\href{http://www.tsinghua.edu.cn}{Tsinghua University}.
He took up this appointment (in 2010) immediately after some wonderful
years
at the \href{http://www.cs.toronto.edu}{University of Toronto}, where he
had the privilege of being part of a
great \href{http://www.cs.toronto.edu/theory/}{theory group}. During his
\phd\ at the University of Toronto he read
theory of computing and cryptography with his advisor
\href{http://www.cs.toronto.edu/dcs/people-faculty-rackoff.html}{Charlie
Rackoff}, whose teachings
contributed to %
his deep appreciation for concepts in Computer Science.
Significant influence on his research identity and taste comes from his
teachers
\href{http://www.math.bme.hu/~gabor/}{G\'abor Pete} and
\href{http://www.renyi.hu/~szegedyb/}{Bal\'azs Szegedy}
(from studies in mathematics at the University of Toronto),
and Stavros Cosmadakis (from his engineering studies at the
\href{https://www.ceid.upatras.gr/en}{University of Patras} in Greece).
His current research interests are in the foundations of computer science
(at large),
and he has a more than occasional interest in Cryptography and Machine
Learning.
In his early youth he enjoyed riding motorbikes %
and collecting graduate degrees.
\end{tocabout}

\begin{tocabout}[tang]
  \textsc{Bangsheng Tang} is currently an Associate Researcher at 
\href{http://en.wikipedia.org/wiki/Hulu}{Hulu}, 
Beijing Office.  %
He received his \phd\ in 2013 from the
  \href{http://iiis.tsinghua.edu.cn}{Institute for Interdisciplinary
Information Sciences},
\href{http://www.tsinghua.edu.cn}{Tsinghua University}, 
under the supervision of
  \href{http://iiis.tsinghua.edu.cn/~papakons/}{Periklis
    A. Papakonstantinou}. This work was done during his \phd\ studies.
He did his undergraduate studies in the
  first-ever Tsinghua University Special Pilot CS Class, founded by
  \href{http://iiis.tsinghua.edu.cn/yao/}{Andrew C. Yao}.
  His research interests
  include algorithm design, computational complexity and
  computational group theory.
\end{tocabout}
\end{tocaboutauthors}

\end{document}

