Is "Experimental Complexity Theory" being used to solve open problems?

Question

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?

Answer 1

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.

Answer 2

Many of the best bounds in Ramsey Theory are done by brute forcing through sets of cleverly generated (non-isomorphic) graphs. Progress in Ramsey Theory generally fluxuates between mathematical and computational advances to the problem.

In general, computer brute force is often used to get some evidence for conjectures when no proofs are known to exist. For example, the Goldbach Conjecture and Riemann Hypothesis have been verified by computer search up to very large numbers.