Последствия субэкспоненциальных доказательств / алгоритмов для SAT

Были бы какие-нибудь серьезные последствия, если бы у SAT было самое большее субэкспоненциальное несогласованное доказательство или даже более сильно, у SAT были алгоритмы субэкспоненциального времени?

cc.complexity-theory sat proof-complexity выбирать
источник

Это опровергнет гипотезу об экспоненциальном времени, которая имеет различные последствия (описано в статье в Википедии).

Артем Казнатчеев

@ArtemKaznatcheev комментарий -> ответ?

Суреш Венкат

@SureshVenkat чувствует себя немного неловко, когда дает ответ, когда Райан Уильямс может дать гораздо лучший ответ. Я дал один на данный момент, но я надеюсь, что Райан и другие предложат что-нибудь более крутое.

Артем Казнатчеев

Если ответ правильный, не имеет значения, кто его дает :)

Суреш Венкат

Извините, Артем, мой ответ был бы не намного круче, чем ваш ... Думаю, нужно добавить, что ETH неверно, подразумевает нижние границы новой суперлинейной цепи (та же статья).

Райан Уильямс

Ответы:

Если бы у SAT был алгоритм субэкспоненциального времени, вы бы опровергли гипотезу экспоненциального времени .

$n$ $poly(n)$ $2^n poly(n)$ $NEXP \not\subseteq P/poly$

Артем Казнатчеев
источник

Я думаю, что первый абзац вашего ответа - это просто определение гипотезы об экспоненциальном времени.

Цуёси Ито