Lower bounds for the size of nondeterministic circuits It is known that the minimum size of $U_2$-circuits computing the parity function exactly equals $3(n-1)$. The lower bound proof is based on the gate elimination method.

Recently, I noticed that the gate elimination method works well also for nondeterministic $U_2$-circuits, and we can prove a $3(n-1)$ lower bound for the size of nondeterministic $U_2$-circuits computing the parity function.

(It means that nondeterministic computation is useless to compute parity by $U_2$-circuits and cannot reduce the size from $3(n-1)$. Thus, the minimum circuits don't change from the deterministic case.)

My questions are the following two:

(1) Is this a new result or a known result?

(2) More generally, are there some known results of lower bounds for the size of nondeterministic circuits (including formulas, constant depth circuits, and so on) with unlimited nondeterministic input bits (or, in other words, unlimited nondeterminism) for an explicit function?

Additional explanation (Nov 27, 2014)

In the second question, I intended that I would like to know especially whether
this is the first nontrivial lower bound for the size of nondeterministic circuits
(including formulas, constant depth circuits, and so on) with unlimited nondeterminism
for an explicit function or not.
I know there are some results if nondeterminism is limited, as follows.

[1] Hartmut Klauck: Lower Bounds for Computation with Limited Nondeterminism.
    IEEE Conference on Computational Complexity 1998: 141-

[2] Vikraman Arvind, K. V. Subrahmanyam, N. V. Vinodchandran:
    The Query Complexity of Program Checking by Constant-Depth Circuits.
    ISAAC 1999: 123-132
A partial answer to the second question:


exponential lower bounds for explicit functions for any class that contains 3-CNF do not translate into exponential lower bounds for unlimited nondeterminism, because one can transform any circuit of size $S$ into a nondeterministic 3-CNF of size $O(S)$ with non-determinism $S$,
even if you want non-determinism less than S, this is still doable if the function is computed by a $B_2$ formula (for example, parity), because one can split this formula of size $S$ into, say, $S/100$ pieces introducing $S/100$ new variables, and the resulting formula will be $O(S)$ size (though the constant in the $O()$ will be large),
for limited (but growing) nondeterminism one can, of course, use good old bounds (for example, Hastad's exponential lower bound $2^{n^{1/d}}$ for parity remains exponential if the nondeterminism is much less than $n^{1/d}$: just enumerate all possible bits for the nondeterminism and take a big OR of the resulting formulas).


A partial answer to the first question:


not known to me :) it would be interesting to see the proof (in particular, how can you substitute values for the existential variables).