A “teoria da complexidade experimental” está sendo usada para resolver problemas em aberto?

Scott Aaronson propôs um desafio interessante : podemos usar os supercomputadores hoje para ajudar a resolver problemas de CS da mesma maneira que os físicos usam grandes coletores de partículas?

Mais concretamente, minha proposta é dedicar parte do poder computacional do mundo a uma tentativa total de responder a perguntas como as seguintes: calcular a permanente de uma matriz 4 por 4 exige operações aritméticas mais do que calcular seu determinante?

Ele conclui que isso exigiria aproximadamente operações de ponto flutuante, que estão além dos nossos meios atuais. Os slides estão disponíveis e também valem a pena ler. $10^{123}$

Existe alguma precedência para resolver problemas abertos do TCS através da experimentação de força bruta?

Em "Localizando circuitos eficientes usando solucionadores SAT", Kojevnikov, Kulikov e Yaroslavtsev usaram os solucionadores SAT para encontrar melhores circuitos para calcular a função .$MOD_k$

Eu usei computadores para encontrar provas dos limites inferiores do espaço-tempo, conforme descrito aqui . Mas isso só foi possível porque eu estava trabalhando com um sistema de provas extremamente restritivo.

Maverick Woo e eu trabalhamos há algum tempo para encontrar o domínio "certo" para provar os limites superior / inferior do circuito usando computadores. Esperávamos resolver vs A C C 0 (ou uma versão muito fraca) usando solucionadores SAT, mas isso parece cada vez mais improvável. (Espero que Maverick não se importe que eu diga isso ...)$CC^0$$ACC^0$

O primeiro problema genérico com o uso da pesquisa de força bruta para provar limites inferiores não triviais é que leva muito tempo, mesmo em um computador muito rápido. A alternativa é tentar usar os solucionadores SAT, QBF ou outras sofisticadas ferramentas de otimização, mas elas não parecem ser suficientes para compensar a enormidade do espaço de pesquisa. Os problemas de síntese de circuitos estão entre os casos práticos mais difíceis que podemos encontrar.

O segundo problema genérico é que a "prova" do limite inferior resultante (obtida executando a pesquisa de força bruta e não encontrando nada) seria insanamente longa e aparentemente não produziria nenhuma percepção (além do fato de que o limite inferior é válido). Portanto, um grande desafio para a "teoria da complexidade experimental" é encontrar questões interessantes do limite inferior para as quais a eventual "prova" do limite inferior seja curta o suficiente para ser verificável e interessante o suficiente para levar a novas idéias.

Muitos dos melhores limites da Teoria de Ramsey são feitos por força bruta através de conjuntos de gráficos inteligentemente gerados (não isomórficos). O progresso na teoria de Ramsey geralmente flui entre os avanços matemáticos e computacionais do problema.

Em geral, a força bruta do computador é frequentemente usada para obter evidências de conjecturas quando não há provas de que exista. Por exemplo, a Conjectura de Goldbach e a Hipótese de Riemann foram verificadas por pesquisa de computador com números muito grandes.