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

<p>The short answer is: it is open.</p>

<p>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$).</p>

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

CC BY-SA 2.5
2011-03-01T10:11:17.813Z
Thanks. Then what is the general belief to this problem? I guess the community has made some "guess" about the result.
Xi Wu
CC BY-SA 2.5
2011-03-02T01:00:43.463Z
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
CC BY-SA 2.5
2011-02-28T19:58:51.040Z
2011-02-28T21:40:59.307Z
2011-02-28T21:40:59.307Z
Kaveh
<p>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...</p>

CC BY-SA 2.5
2011-03-01T09:47:23.530Z
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
CC BY-SA 2.5
2011-02-28T19:21:14.803Z
2011-02-28T19:21:14.803Z
Ramprasad
<p>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</p>

CC BY-SA 3.0
2015-07-31T03:44:03.000Z
http://cstheory.stackexchange.com/questions/22022/overlinesat-in-ntimesubexp
Igor Shinkar
<cc.complexity-theory><proof-complexity>
Does coNP-complete problem have subexponential size certificate?
Xi Wu
# Does coNP-complete problem have subexponential size certificate?

(Asked by: username_0 on 2011-02-28)

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

**Tags:** cc.complexity-theory, proof-complexity
> **Comments:**
> **username_1**: http://cstheory.stackexchange.com/questions/22022/overlinesat-in-ntimesubexp  

---

## 2 answers

### Answer by username_2 on 2011-02-28. Score: 12

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

> **Comments:**
> **username_0**: Thanks. Then what is the general belief to this problem? I guess the community has made some "guess" about the result.  
> **username_2**: 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)})$).  

---

### Answer by username_3 on 2011-02-28. Score: 7

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...

> **Comments:**
> **username_0**: 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.  

---

