# Solving 0/1 integer programming and solving ACC-of-SYM circuits

I am referring to the proof of Theorem 1.4 in this STOC 2014 paper, https://arxiv.org/abs/1401.2444. In particular my question is about the argument that begins in the 8th line of page 9 where the author says the following,

"Following the strategy of Theorem 1.2 (and the author's ACC SAT algorithm https://www.cs.cmu.edu/~ryanw/acc-lbs.pdf), the satisfiability question of (a $AC^0[2]\circ SYM$) C with $n$ inputs and size $poly(s)$ can be efficiently converted into a problem of evaluating a larger $AC^0[2]\circ SYM$ circuit C' where C' has $(n-k)$ inputs, $2^k\times poly(s,M)$ size and $k < \frac{n}{2}$ is a parameter and the $AC^0$ part has depth $6$. More precisely C' is an OR of $2^k$ copies of the depth $5$ circuit $C$ and each copy has its first $k$ inputs assigned to a distinct string from $\{0,1\}^k$."

Now given how C' is defined given a circuit C it seems obvious to me that the circuit C' is satisfiable if and only if C is satisfiable.

(...EXCEPT that I dont see why $C$ is a depth $5$ circuit given that from whats on the top of page $9$ it follows that its a $AND \circ OR \circ AND \circ XOR \circ AND \circ OR \circ SYM$. Then the $AC^0[2]$ part of $C'$ should be depth $6$ and that matches with the first part of the paragraph. I guess this "depth 5" part of the quoted paragraph is a typo!...)

Then to make this argument where is the need for the deeper theorems like Theorem 1.2 of this paper (which is about a fast algorithm to evaluate $ACC \circ THR$ circuits) and the big breakthrough paper thats cited? (At no later stage in this proof do I see these two big results being referred to either.) Am I missing something in this argument?