corollaryroutine

Linear-size circuit lower bound for E^NP

Corollary·cor:consequence-circuits·§C.1 Circuit lower bounds for E^NP

Statement (paper)

We have ENP⊈SIZE(O(n)). \mathrm E^{\mathrm{NP}}\not\subseteq\mathrm{SIZE}(O(n)).

In plain English

The class ENP\mathrm E^{\mathrm{NP}} is not contained in SIZE(O(n))\mathrm{SIZE}(O(n)): some language in ENP\mathrm E^{\mathrm{NP}} cannot be decided by Boolean circuits of linear size.

Why it's here

This is a consequence of the main theorem's subexponential kk-CNF counting algorithm, placed in the appendix on circuit lower bounds. The algorithm's 2o(n)2^{o(n)} running time feeds the standard algorithms-to-lower-bounds connection, which yields a linear-size circuit lower bound for ENP\mathrm E^{\mathrm{NP}}.
Classified routine:
Follows by plugging the main theorem's subexponential #k-SAT algorithm into the known algorithms-to-circuit-lower-bounds connection: Jahanjou–Miles–Viola showed that sufficiently fast 3-SAT algorithms yield E^NP lower bounds against linear-size circuits, in the line of Williams' ACC lower bound.

Uses

thmSubexponential deterministic k-CNF model counting

Used by

Nothing in the paper

Sources

PaperOpen
Section
§C.1 Circuit lower bounds for E^NP
Page
—
Label
cor:consequence-circuits
Line
main_full_version.tex:4242
Leannot aligned

Phase 2 aligns this node to a Lean declaration.