corollaryroutineunresolved_ref

Superlinear circuit lower bound for E^NP

Corollary·cor:quantitative-circuits·§1 Introduction

Statement (paper)

Let CL(n)C_L(n) be the minimum number of noninput gates in a circuit computing LL on {0,1}n\{0,1\}^n, allowing arbitrary Boolean gates of fan-in at most two and unrestricted fan-out. There exist a language L∈ENPL\in\mathrm E^{\mathrm{NP}} and a constant c>0c>0 such that CL(n)>c nlog⁡nfor infinitely many n. C_L(n)>c\,n\sqrt{\log n}\qquad\text{for infinitely many }n.

In plain English

There is a language L∈ENPL\in\mathrm E^{\mathrm{NP}} and a constant c>0c>0 such that, for infinitely many nn, every fan-in-two circuit (arbitrary binary gates, unrestricted fan-out) computing LL on {0,1}n\{0,1\}^n needs more than c nlog⁡nc\,n\sqrt{\log n} noninput gates.

Why it's here

This is the paper's quantitative circuit-lower-bound application of the fast 3-SAT algorithm from Theorem 1.1 at linear clause density. The proof takes the witness language of a succinct 3-CNF built from a hard nondeterministic-time unary language and shows that small circuits for it would give a nondeterministic algorithm for that language running within time 2n/22^{n/2}, contradicting the time hierarchy theorem.
Classified routine:
Follows from the paper's fast SAT/counting algorithm (thm-main) via the standard Williams-style algorithms-to-lower-bounds connection: succinct 3-SAT reduction plus the nondeterministic time hierarchy theorem.

Uses

thmSubexponential deterministic k-CNF model counting

Used by

Nothing in the paper

Inside the proof

claimHard unary language yields succinct 3-CNFclaimClause decoder has linear-size circuitclaimWitness language lies in E^NPclaimFast 3-SAT at linear clause densityclaimSmall witness circuits give nondeterministic algorithm for HclaimTest-circuit runtime contradicts time hierarchy

Sources

PaperOpen
Section
§1 Introduction
Page
—
Label
cor:quantitative-circuits
Line
main_full_version.tex:183
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • warn
    unresolved_ref
    Proof rests essentially on external results: Williams's witness-circuit argument [Wil13], the JMV13 local reduction, and Zak's nondeterministic time hierarchy.