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)})$.

  • 1
    $\begingroup$ Thanks. Then what is the general belief to this problem? I guess the community has made some "guess" about the result. $\endgroup$ – Xi Wu Mar 1 '11 at 10:11
  • $\begingroup$ 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)})$). $\endgroup$ – 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...

  • $\begingroup$ 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. $\endgroup$ – Xi Wu Mar 1 '11 at 9:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.