# Does coNP-complete problem have subexponential size certificate?

Assuming NP != coNP, then there is no polynomial size certificate for coNP-complete problem. But what about subexponential size certificate? Particularly for coSAT, is there subexponential size proof to prove a formula is unsatisfiable? If not, what is the negative evidence? Thanks

This is the topic of proof complexity, i.e. the size of certificates for the $\mathbf{co\text{-}NP}\text{-}complete$ problem $TAUT$ ($= coSAT$).

The short answer is: it is open.

On the negative side, we cannot even show that there are not polysize $Frege$ refutations for unsatisfiable formulas (let alone the general question of showing this for an arbitrary proof system, a propositional proof system can be thought as a nondeterministic algorithm for $TAUT$).

The question is also equivalent to $\mathbf{coNP} \subseteq NTime(2^{o(n)})$.

• Thanks. Then what is the general belief to this problem? I guess the community has made some "guess" about the result. – Xi Wu Mar 1 '11 at 10:11
• I don't have a good answer and I don't remember hearing conjectures/guesses about this, the only related thing that comes to my mind right now is that some experts find it plausible that EF (Extended-Frege) is an optimal proof system, but EF being an optimal proof system would make sense even if some theorems don't have subexponential EF proofs (i.e. $\mathbf{coNP} \not \subseteq NTime(2^{o(n)})$). There are researchers who find even $\mathbf{coNP}=\mathbf{NP}$ plausible, and there are others who think $\mathbf{coNP} \not \subseteq NTime(2^{o(n)})$). – Kaveh Mar 2 '11 at 1:00

One possible implication of this would be that $NEXP \nsubseteq P/poly$ from Ryan William's result (since you would then have an co-nondeterministic algorithm for CircuitSAT running in time faster than exponential). Not really negative evidence, but still...

• Thanks. I incline to interpret your answer as the difficulty to show coNP-complete problem has subexponential size proof, because then we have a nice separation. – Xi Wu Mar 1 '11 at 9:47