<p>Many of the best bounds in <a href="http://en.wikipedia.org/wiki/Ramsey_theory">Ramsey Theory</a> 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.</p>

<p>In general, computer brute force is often used to get some evidence for conjectures when no proofs are known to exist. For example, the <a href="http://en.wikipedia.org/wiki/Goldbach%27s_conjecture">Goldbach Conjecture</a> and <a href="http://en.wikipedia.org/wiki/Riemann_hypothesis">Riemann Hypothesis</a> have been verified by computer search up to very large numbers.</p>

CC BY-SA 2.5
2010-08-24T23:21:27.370Z
I think the question is about solving major open problems in *computer science*.
Jukka Suomela
CC BY-SA 2.5
2010-08-24T23:36:46.680Z
True. I missed that. Should I delete this answer?
Ross Snider
CC BY-SA 2.5
2010-08-25T13:56:44.297Z
Sorry that my question wasn't clear.  I would suggest that you leave your answer.
Shane
CC BY-SA 2.5
2010-08-24T21:32:04.437Z
2010-08-24T21:32:04.437Z
Ross Snider
<p>In "Finding Efficient Circuits Using SAT-solvers", Kojevnikov, Kulikov, and Yaroslavtsev have used SAT solvers to find better circuits for computing $MOD_k$ function. </p>

<p>I have used computers to find proofs of time-space lower bounds, as described <a href="https://cstheory.stackexchange.com/questions/93/what-are-the-best-current-lower-bounds-on-3sat/120#120">here</a>. But that was only feasible because I was working with an extremely restrictive proof system.</p>

<p>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...)</p>

<p>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.</p>

<p>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.</p>

CC BY-SA 2.5
2010-08-24T21:30:49.117Z
2010-08-24T21:30:49.117Z
2017-04-13T12:32:28.077Z
Ryan Williams
<p>Scott Aaronson proposed <a href="http://www.scottaaronson.com/blog/?p=252">an interesting challange</a>: can we use supercomputers today to help solve CS problems in the same way that physicists use large particle colliders?</p>

<blockquote>
  <p>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?</p>
</blockquote>

<p>He concludes that this would require ~$10^{123}$ floating point operations, which is beyond our current means.  The <a href="http://www.scottaaronson.com/talks/wildidea.ppt">slides are available</a> and are also worth reading.  </p>

<p>Is there any precedence for solving open TCS problems through brute force experimentation?  </p>

CC BY-SA 2.5
2010-08-24T21:12:02.623Z
Related (but much broader) question: http://cstheory.stackexchange.com/questions/82/where-and-how-did-computers-help-prove-a-theorem
Shane
<cc.complexity-theory>
Is "Experimental Complexity Theory" being used to solve open problems?
Shane
# Is "Experimental Complexity Theory" being used to solve open problems?

(Asked by: username_0 on 2010-08-24)

Scott Aaronson proposed [an interesting challange](http://www.scottaaronson.com/blog/?p=252): 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](http://www.scottaaronson.com/talks/wildidea.ppt) and are also worth reading.

Is there any precedence for solving open TCS problems through brute force experimentation?

**Tags:** cc.complexity-theory
> **Comments:**
> **username_0**: Related (but much broader) question: http://cstheory.stackexchange.com/questions/82/where-and-how-did-computers-help-prove-a-theorem  

---

## 2 answers

### Answer by username_3 on 2010-08-24. Score: 24 | Accepted answer

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](https://cstheory.stackexchange.com/questions/93/what-are-the-best-current-lower-bounds-on-3sat/120#120). 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 by username_1 on 2010-08-24. Score: 8

Many of the best bounds in [Ramsey Theory](http://en.wikipedia.org/wiki/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](http://en.wikipedia.org/wiki/Goldbach%27s_conjecture) and [Riemann Hypothesis](http://en.wikipedia.org/wiki/Riemann_hypothesis) have been verified by computer search up to very large numbers.

> **Comments:**
> **username_2**: I think the question is about solving major open problems in *computer science*.  
> **username_1**: True. I missed that. Should I delete this answer?  
> **username_0**: Sorry that my question wasn't clear.  I would suggest that you leave your answer.  

---

