# Circuits and formulas for Clique

Is it correct to say that the Clique Problem is in $$P$$ iff there exists a family of Boolean circuits $$C$$ to decide Clique whose sizes are bounded by a polynomial? And based on this question, does that imply that there exists an equivalent set of Boolean formulas $$F$$ to decide Clique whose sizes are bounded by a polynomial? And if there is such an $$F$$, would there be correct derivations based on propositional logic axioms from any member of $$F$$ to the corresponding large naive formula for Clique?

• It is conjectured that $$\mathsf{NC^1} \neq \mathsf{P}$$.
• It is conjectured that $$\mathsf{NP} \neq \mathsf{coNP}$$.