Last week I attended the Army Research Office sponsored Workshop on Reasoning in Adversarial and Noncooperative Environments related to Topic #22 of the 2011 MURI. Most of the attendees were AI types many of whom look at games with incomplete information against opponents you can't trust. A group at USC talked about their work using game theory to deploy federal air marshals on planes and road-side checking at LAX. Game theory that might save lives.
I talked in a panel on the complexity of computing equilibrium on why we should turn the question around and use computational complexity to redefine equilibrium. Bart Selman, also on the panel, talked about his limited success in using SAT solving heuristics for QBF. During the Q&A we got into an interesting debate on the importance of computational complexity in real-world scenarios. The word "irrelevant" came up to note that NP-completeness is too blunt a tool to capture hardness in practice. Bart didn't think average-case was quite the right approach either, some other structural property of problems was needed.
Though we both care deeply about satisfiability, Bart and I don't hang out much in the same circles and this workshop was the first time we really had to a chance to chat. Despite the panel, Bart later showed quite an interest in computational complexity. I found myself explaining Ryan's new result to him, which get complexity results from betters circuit SAT algorithms.
The PCP theorem says it is as hard to approximate max-SAT as it is to solve it exactly. In practice, according to Bart, this separation makes SAT easier to solve heuristically. So Bart suggested one might use the PCP theorem as a method to preprocess a formula to improve current heuristics. The PCP theorem still has large constants in the size of the reduction making a direct application impractical. But perhaps parts of the theorem, for example using good error-correcting codes, can help. That would take the PCP theorem, normally used for showing problems hard, to help make SAT easier. Cool if it could be made to work.