Is "Experimental Complexity Theory" being used to solve open problems? Scott Aaronson proposed an interesting challange: can we use supercomputers today to help solve CS problems in the same way that physicists use large particle colliders?


  More concretely, my proposal is to
  devote some of the world’s computing
  power to an all-out attempt to answer
  questions like the following: does
  computing the permanent of a 4-by-4
  matrix require more arithmetic
  operations than computing its
  determinant?


He concludes that this would require ~$10^{123}$ floating point operations, which is beyond our current means.  The slides are available and are also worth reading.  

Is there any precedence for solving open TCS problems through brute force experimentation?
In "Finding Efficient Circuits Using SAT-solvers", Kojevnikov, Kulikov, and Yaroslavtsev have used SAT solvers to find better circuits for computing $MOD_k$ function. 

I have used computers to find proofs of time-space lower bounds, as described here. But that was only feasible because I was working with an extremely restrictive proof system.

Maverick Woo and I have been working for some time to find the "right" domain for proving circuit upper/lower bounds using computers. We had hoped that we may resolve $CC^0$ vs $ACC^0$ (or a very weak version of it) using SAT solvers, but this is looking more and more unlikely. (I hope Maverick doesn't mind me saying this...)

The first generic problem with using brute-force search to prove nontrivial lower bounds is that it just takes too damn long, even on a very fast computer. The alternative is to try to use SAT solvers, QBF solvers, or other sophisticated optimization tools, but they do not seem to be enough to offset the enormity of the search space. Circuit synthesis problems are among the hardest practical instances one can come by.

The second generic problem is that the "proof" of the resulting lower bound (obtained by running brute-force search and finding nothing) would be insanely long and apparently yield no insight (other than the fact that the lower bound holds). So a big challenge to "experimental complexity theory" is to find interesting lower bound questions for which the eventual "proof" of the lower bound is short enough to be verifiable, and interesting enough to lead to further insights.