claimroutineinferred_dep

Witness language lies in E^NP

Claim·§1 Introduction·inside corSuperlinear circuit lower bound for E^NP

Statement (paper)

The language WW defined by padding each variable label to dndn bits, with W(i)W(i) equal to bit ii of the lexicographically first satisfying assignment of φn\varphi_n (ordering variables by their labels) when ∣i∣=dn|i|=dn and φn\varphi_n is satisfiable, and W(i)=0W(i)=0 otherwise, lies in ENP\mathrm E^{\mathrm{NP}}.

In plain English

The witness language WW, where W(i)W(i) is bit ii of the lexicographically first satisfying assignment of φn\varphi_n (with variable labels padded to dndn bits, and W(i)=0W(i)=0 if φn\varphi_n is unsatisfiable), is decidable in ENP\mathrm E^{\mathrm{NP}}.

Why it's here

This places the hard witness language in the class ENP\mathrm E^{\mathrm{NP}} required by the corollary. Since the decoder from the earlier claim produces φn\varphi_n succinctly, the first satisfying assignment can be found bit by bit with NP-oracle queries in time exponential in the input length dndn, and the circuit-size argument then applies to WW.
Classified routine:
Standard self-reduction argument: the lexicographically first satisfying assignment of a succinctly described exponential-size formula is computed bit by bit with NP-oracle queries in exponential time. This is the familiar step in Williams-style circuit lower bounds, e.g. Jahanjou–Miles–Viola 2013.

Uses

claimHard unary language yields succinct 3-CNF

Used by

claimSmall witness circuits give nondeterministic algorithm for H

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Witness language W lies in E^NP" rests on claim-cor-quantitative-circuits-1