Incorporated @atri 031421 suggestions.

hardness-app.tex

@@ -664,11 +664,11 @@ and we obtain the desired result.
 
 
 \paragraph{Run-time Analysis}
-It is easy to check that except for~\Cref{alg:sample-times-union}, all lines take $O(1)$ time.  Now consider all executions of~\Cref{alg:sample-times-union} together. We note that at each level we will be adding a given set of variables to some set at most once: since the sum of the sizes of the sets at a given level is at most $\degree(\circuit)$, each level involves $O(\degree(\circuit)\cdot\log{\degree(\circuit)})$ time. Thus, overall all executions of~\Cref{alg:sample-times-union} take $O(\degree(\circuit)\cdot\log{\degree(\circuit)}\cdot \depth(\circuit))$ time.  Thus, for $n$ gates visited \sampmon has runtime of $O\left(n + \degree(\circuit) log{\degree(\circuit)}\cdot\depth(\circuit)\right).$
+It is easy to check that except for~\Cref{alg:sample-times-union}, all lines take $O(1)$ time.  Now consider an execution of~\Cref{alg:sample-times-union}. We note that we will be adding a given set of variables to some set at most once: since the sum of the sizes of the sets at a given level is at most $\degree(\circuit)$, each gate visited takes $O(\log{\degree(\circuit)})$.  Deote \cost(\circuit) (\Cref{eq:cost-sampmon}) to be an upper bound of the number of nodes visited by \sampmon.  Then the runtime is $O\left(\cost(\circuit)\cdot \log{\degree(\circuit)}\right)$.
 
-We now bound the number of recursive calls $n$ in $\sampmon$ by $O\left((\degree(\circuit) + 1)\cdot \depth(\circuit)\right)$.  
+We now bound the number of recursive calls in $\sampmon$ by $O\left((\degree(\circuit) + 1)\right.$$\left.\cdot\right.$ $\left.\depth(\circuit)\right)$.  
 
-Let \cost be a function that models an upper bound on the number of gates that can be visited in the run of \sampmon.  We define \cost recursively as follows.
+Let \cost$(\cdot)$ be a function that models an upper bound on the number of gates that can be visited in the run of \sampmon.  We define \cost$(\cdot)$ recursively as follows.
 
 \begin{equation}
 	\cost(\circuit) =
@@ -679,7 +679,7 @@ Let \cost be a function that models an upper bound on the number of gates that c
 		\end{cases}\label{eq:cost-sampmon}
 \end{equation}
 
-First note that the number of gates visited in \sampmon is $O\left(\cost(\circuit)\right)$.  To show that \Cref{eq:cost-sampmon} upper bounds the number of nodes visited by \sampmon, note that when \sampmon visits a gate such that \circuit.\type $ =\circmult$, line ~\ref{alg:sample-times-for-loop} visits each input of \circuit.  For the case when \circuit.\type $= \circplus$, line ~\ref{alg:sample-plus-bsamp} visits exactly one of the input gates.  Finally, it is trivial to see that when \circuit.\type $\in \{\var, \tnum\}$, i.e., a source gate, that only one gate is visited.
+First note that the number of gates visited in \sampmon is $\leq\cost(\circuit)$.  To show that \Cref{eq:cost-sampmon} upper bounds the number of nodes visited by \sampmon, note that when \sampmon visits a gate such that \circuit.\type $ =\circmult$, line ~\ref{alg:sample-times-for-loop} visits each input of \circuit, as defined in (\ref{eq:cost-sampmon}).  For the case when \circuit.\type $= \circplus$, line ~\ref{alg:sample-plus-bsamp} visits exactly one of the input gates, which may or may not be the subcircuit with the maximum number of gates traversed, which makes \cost$(\cdot)$ an upperbound.  Finally, it is trivial to see that when \circuit.\type $\in \{\var, \tnum\}$, i.e., a source gate, that only one gate is visited.
 
 We prove the following inequality holds.
 \begin{equation}
@@ -690,8 +690,8 @@ Note that \Cref{eq:strict-upper-bound} implies the claimed runtime.  We prove \C
 
 For the base case $\degree(\circuit) = \depth(\circuit) = 0$, $\cost(\circuit) = 1$, and it is trivial to see that the inequality $2\degree(\circuit) \cdot \depth(\circuit) + 1 \geq \cost(\circuit)$ holds.
 
-For the inductive hypothesis, we assume the bound holds for a circuit where $\ell \geq \depth(\circuit) \geq 0$.
-Now consider the case when \sampmon has an arbitrary circuit \circuit input with $\depth(\circuit) = \ell + 1$.  By the hypothesis, we know all inputs $\circuit_i$ of the sink gate \circuit uphold the bound
+For the inductive hypothesis, we assume the bound holds for a circuit where $\ell \geq \depth(\circuit) \geq 1$.
+Now consider the case when \sampmon has an arbitrary circuit \circuit input with $\depth(\circuit) = \ell + 1$.  By definition \circuit.\type $\in \{\circplus, \circmult\}$. Note that since $\depth(\circuit) \geq 2$, \circuit must have inputs.  Further we know that by the inductive hypothesis the inputs $\circuit_i$ for $i \in \{\linput, \rinput\}$ of the sink gate \circuit uphold the bound
 \begin{equation}
 2\degree(\circuit_i)\cdot \depth(\circuit_i) + 1 \geq \cost(\circuit_i).\label{eq:ih-bound-cost}
 \end{equation}
@@ -704,7 +704,7 @@ substituing values, the following should hold,
 \begin{align}
 &2\left(\degree(\circuit_\linput) + \degree(\circuit_\rinput)\right) \cdot \left(\max(\depth(\circuit_\linput), \depth(\circuit_\rinput)) + 1\right) + 1 \label{eq:times-lhs}\\
 &\qquad\geq 2\degree(\circuit_\linput) \cdot \depth(\circuit_\linput) + 2 \degree(\circuit_\rinput) \cdot \depth(\circuit_\rinput) + 3\label{eq:times-middle} \\
-&\qquad\geq 1 + \cost(\circuit_\linput) + \cost(\circuit_\rinput) = \cost(\circuit)\label{eq:times-rhs}.
+&\qquad\geq 1 + \cost(\circuit_\linput) + \cost(\circuit_\rinput) = \cost(\circuit) (\ref{eq:cost-sampmon})\label{eq:times-rhs}.
 \end{align}
 
 To prove the inequality $\Cref{eq:times-lhs} \geq \Cref{eq:times-middle}$, first, let us expand \Cref{eq:times-lhs},  
@@ -720,26 +720,26 @@ Let us simplify the inequality $(\ref{eq:times-lhs}) \geq (\ref{eq:times-middle}
 &\qquad \geq 2\degree(\circuit_\linput) \cdot \depth(\circuit_\linput) + 2 \degree(\circuit_\rinput) \cdot \depth(\circuit_\rinput) + 3\nonumber\\
 &\implies 2\degree(\circuit_\linput) + 2\degree(\circuit_\rinput) + 1 \geq 3\label{eq:times-lhs-middle-step1}
 \end{align}
-Note that by the \emph{reduced} invariant of \reduce, a circuit \circuit with $\depth(\circuit) > 1$ will always have at least one input with $\degree(\circuit_i) \geq 1$.  Thus, \Cref{eq:times-lhs-middle-step1} follows, and the inequality is upheld.
+Note that by the \emph{reduced} invariant of \reduce, a circuit \circuit with $\depth(\circuit) \geq 1$ will always have at least one input with $\degree(\circuit_i) \geq 1$.  Thus, \Cref{eq:times-lhs-middle-step1} follows, and the inequality is upheld.
 
-Now to justify the inequality (\ref{eq:times-middle}) $\geq$ (\ref{eq:times-rhs}) which holds for the following reasons.  First, \Cref{eq:times-rhs} is the result of \Cref{eq:cost-sampmon} when $\circuit.\type = \circmult$.  \Cref{eq:times-middle} is then produced by substituting the upperbound of (\ref{eq:ih-bound-cost}) for each $\cost(\circuit_i)$, trivially establishing an upper bound to (\ref{eq:times-rhs}).  This proves \Cref{eq:ih-bound-cost} for the $\circmult$ case.
+Now to justify the inequality (\ref{eq:times-middle}) $\geq$ (\ref{eq:times-rhs}) which holds for the following reasons.  First, \Cref{eq:times-rhs} is the result of \Cref{eq:cost-sampmon} when $\circuit.\type = \circmult$.  \Cref{eq:times-middle} is then produced by substituting the upperbound of (\ref{eq:ih-bound-cost}) for each $\cost(\circuit_i)$, trivially establishing an upper bound to (\ref{eq:times-rhs}).  This proves \Cref{eq:strict-upper-bound} for the $\circmult$ case.
 
 For the case when \circuit.\type $= \circplus$, substituting values yields
 \begin{align}
 &2\max(\degree(\circuit_\linput), \degree(\circuit_\rinput)) \cdot \left(\max(\depth(\circuit_\linput), \depth(\circuit_\rinput)) + 1\right) +1\label{eq:plus-lhs-inequality}\\
-&\qquad \geq \max\left(2\degree(\circuit_\linput) \cdot \depth(\circuit_\linput) + 1, 2\degree(\circuit_\rinput) \cdot \depth(\circuit_\rinput) +1\right)\label{eq:plus-middle}\\
+&\qquad \geq \max\left(2\degree(\circuit_\linput) \cdot \depth(\circuit_\linput) + 1, 2\degree(\circuit_\rinput) \cdot \depth(\circuit_\rinput) +1\right) + 1\label{eq:plus-middle}\\
 &\qquad \geq 1 + \max(\cost(\circuit_\linput), \cost(\circuit_\rinput)) = \cost(\circuit)\label{eq:plus-rhs}
 \end{align}
 
-To prove that $\ref{eq:plus-lhs-inequality}) \geq (\ref{eq:plus-middle})$, we can rewrite (\ref{eq:plus-lhs-inequality}) as
+To prove that $(\ref{eq:plus-lhs-inequality}) \geq (\ref{eq:plus-middle})$, we can rewrite (\ref{eq:plus-lhs-inequality}) as
 \begin{equation}
 2\degree_{\max}\depth_{\max} + 2\degree_{\max} + 1.\label{eq:plus-lhs-expanded}
 \end{equation}
-For \Cref{eq:plus-middle}, since $\degree_{\max} \cdot \depth_{\max} \geq \degree(\circuit_i)\cdot \depth(\circuit_i),$ the following upper bound holds,
+Since $\degree_{\max} \cdot \depth_{\max} \geq \degree(\circuit_i)\cdot \depth(\circuit_i),$ the following upper bound holds for \Cref{eq:plus-middle}:
 \begin{equation}
-2\degree_{\max}\depth_{\max} + 2 \geq  \max\left(2\degree(\circuit_\linput) \cdot \depth(\circuit_\linput) + 1, 2\degree(\circuit_\rinput) \cdot \depth(\circuit_\rinput) +1\right).\label{eq:plus-middle-expanded}
+2\degree_{\max}\depth_{\max} + 2 \geq  \max\left(2\degree(\circuit_\linput) \cdot \depth(\circuit_\linput) + 1, 2\degree(\circuit_\rinput) \cdot \depth(\circuit_\rinput) +1\right) + 1.\label{eq:plus-middle-expanded}
 \end{equation}
-Simplifying the inequality $(\ref{eq:plus-lhs-expanded}) \geq (\ref{eq:plus-middle-expanded})$, we obtain
+Substituting the upperbound of (\ref{eq:plus-middle-expanded}) in for (\ref{eq:plus-middle}) we obtain the following for the inequality (\ref{eq:plus-lhs-inequality}) $\geq$ (\ref{eq:plus-middle}):
 \begin{align}
 &2\degree_{\max}\depth_{\max} + 2\degree_{\max} + 1 \geq 2\degree_{\max}\depth_{\max} + 2\nonumber\\
 &\implies 2\degree_{\max} + 1 \geq 2\label{eq:plus-upper-bound-final}.

main.vtc

@@ -1 +1 @@
-\contitem\title{Standard Operating Procedure in Bag PDBs Queries Considered Harmful}\author{Su Feng, Boris Glavic, Aaron Huber, Oliver Kennedy, and Atri Rudra}\page{23:1--23:50}
+\contitem\title{Standard Operating Procedure in Bag PDBs Queries Considered Harmful}\author{Su Feng, Boris Glavic, Aaron Huber, Oliver Kennedy, and Atri Rudra}\page{23:1--23:51}