To show that NP=coNP implies P=NP seems far, far beyond our current abilities — indeed, almost as hard as NP vs. coNP itself! You would need to show that any efficient proof system for coNP is “automatizable” — i.e. that the proofs can actually be found in polynomial time. Certainly any proof of this would have to be non-relativizing, and I think non-algebrizing as well (will have to check though). It’s not, repeat **not**, some simple observation that everyone’s overlooked.

I apologize for the hijacking. ]]>

Since electrons, photons, and fingers all travel with finite velocity, even seeing the characters being typed out is significantly delayed from the events as they occur. In fact, even if you are in the vicinity of the events there is some brief but quantifiable delay in your perceiving them. I suggest that there is not only no such thing as live-blogging, but that there is no live-anything at all!

]]>We say a problem has polynomial-size certificates if there’s a polynomial-time algorithm V such that for every problem instance φ,

(i) if the answer is “yes” then there’s at least one polynomial-size string w such that V(φ,w) accepts, and

(ii) if the answer is “no” then there’s no w such that V(φ,w) accepts.

(This is also the definition for a problem being in NP. Thus, coNP-complete problems have polynomial-size certificates if and only if NP=coNP — which is considered extremely unlikely, almost as unlikely as P=NP.)

Notice that the definition of a certificate is just *anything that causes V to accept!* The reason this definition is reasonable is that we stipulated that if the answer is “no” then nothing can cause V to accept. The two requirements — that some certificate should cause V to accept a “yes” instance, and that no certificate should cause it to accept a “no” instance — are called *completeness* and *soundness* respectively.

I’m guessing what you really want to know is this: in practice, how do people go about proving that a Boolean formula is unsatisfiable? Well, one way is just to list all 2^{n} possible satisfying assignments and show that none of them work! But there are entire fields — called *proof complexity* and *automated reasoning* — devoted to coming up with better ways. One example of a better way is what’s called a resolution proof, which basically involves smashing together clauses (“resolving” them) until you reach a contradiction. You can then conclude that the original formula must have been unsatisfiable.

In practice, many unsatisfiable formulas have short resolution proofs — but alas, Haken proved in the 80’s that *some* unsatisfiable formulas require exponentially-long resolution proofs.

If you come up with a proof system where the proofs of unsatisfiability always have polynomial size, you’ll have shown NP=coNP. And if you show furthermore that the proofs can always be *found* efficiently, you’ll have shown P=NP.