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
2 Answers
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 WuMar 1, 2011 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$– KavehMar 2, 2011 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 WuMar 1, 2011 at 9:47