claimstandard

Hard unary language yields succinct 3-CNF

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

Statement (paper)

For all sufficiently large nn, applying the local reduction of [JMV13] with locality parameter r=2r=2 to the fixed machine for the unary language H∈NTIME⁡(2n)∖NTIME⁡(2n/2)H\in\operatorname{NTIME}(2^n)\setminus\operatorname{NTIME}(2^{n/2}) on input 1n1^n, with time allowance T=2nnO(1)T=2^n n^{O(1)}, yields in polynomial time a decoder with q=n+O(log⁡n)q=n+O(\log n) clause-index bits that outputs, on each index, three variable labels and their signs. The 3-CNF formula φn\varphi_n consisting of the clauses decoded on all 2q2^q indices is satisfiable if and only if 1n∈H1^n\in H.

In plain English

For large nn, the local reduction of [JMV13] with r=2r=2, applied to the machine for a unary language H∈NTIME(2n)∖NTIME(2n/2)H\in\mathrm{NTIME}(2^n)\setminus\mathrm{NTIME}(2^{n/2}) on input 1n1^n with T=2nnO(1)T=2^n n^{O(1)}, gives in polynomial time a decoder mapping each qq-bit clause index, with q=n+O(log⁡n)q=n+O(\log n), to three variable labels and signs. The 3-CNF φn\varphi_n formed by all 2q2^q decoded clauses is satisfiable exactly when 1n∈H1^n\in H.

Why it's here

This turns membership of 1n1^n in a hard nondeterministic-time language into satisfiability of an exponentially large 3-CNF given succinctly by a decoder with only about nn index bits. Later claims build on this: they implement the decoder as a linear-size circuit and define a witness language from the first satisfying assignment of φn\varphi_n, which is what the circuit lower bound argument uses.
Classified standard:
This is a direct application of the local (succinct) reduction from nondeterministic time to succinct 3-SAT by Jahanjou, Miles and Viola (JMV13), combined with the nondeterministic time hierarchy theorem to obtain the hard unary language HH. It is the standard first step of Williams-style circuit lower bound arguments.

Uses

Nothing else in the paper

Used by

claimClause decoder has linear-size circuitclaimWitness language lies in E^NP

Sources

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

Phase 2 aligns this node to a Lean declaration.