It is widely believed that NP does not equal coNP. This means that there are coNP sets for which some elements require superpolynomial length proofs of membership. Are there coNP sets for which the average element requires superpolynomial length proofs of membership? Exponential length? One goal of this research is to find evidence that such sets exist. For example, what is a plausible complexity theoretic assumption under which these average case hard coNP sets exist? Such a result would generalize the study of average case complexity to work against nondeterministic algorithms. Furthermore, arguing for the existence of these sets is part of an approach to proving the independence of P not equal NP. It has already been argued that the existence of doubly exponentially -hard one way functions rules out P/poly-natural proofs that SATISFIABILITY requires superpolynomial circuits. Furthermore, this implies that propositional proof systems with the interpolation property do not have polynomially bounded proofs that SAT is not in P/poly. It might be possible to generalize the `natural proof/interpolation' approach in order to prove an important independence result for SAT not in P/poly. If average case hard coNP sets of the right type do exist, then there are no NP/poly-natural proofs of SAT not in P/poly. This would imply that propositional systems with the existential interpolation property do not have polynomially-bounded proofs of SAT not in P/poly. Hard coNP sets would have two important consequences. 1) Generalize the known limits of P/poly natural proofs to NP/poly-natural proofs. 2) Extend independence results from systems with the interpolation property to systems with the existential interpolation property. The more powerful independence tools might be extensible to a proof system such as Extended Frege.
