claimroutineinferred_dep

Clause decoder has linear-size circuit

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

Statement (paper)

For all sufficiently large nn, a Boolean circuit of O(n)O(n) fan-in-two gates computing the clause decoder of φn\varphi_n, which maps each clause index in {0,1}q\{0,1\}^q to the three variable labels and their signs, can be constructed in time polynomial in nn (that is, polynomial in the input length 2n2^n after unary encoding of 1n1^n is not required).

In plain English

For all large nn, the clause decoder of φn\varphi_n, which maps a clause index in {0,1}q\{0,1\}^q to its three variable labels and signs, is computed by a fan-in-two circuit with O(n)O(n) gates, and this circuit can be built in time polynomial in nn.

Why it's here

The previous claim gives the decoder only as a polynomial-time computable map on q=n+O(log⁡n)q=n+O(\log n) index bits. This claim turns it into an explicit circuit of size O(n)O(n), which is the size bound needed to compare against circuits for the witness language. Later claims use this circuit to get a nondeterministic algorithm for HH from small witness circuits.
Classified routine:
This follows from the local reduction of Jahanjou–Miles–Viola [JMV13], whose clause decoder is computed by quasi-linear (here linear) size circuits. It is a direct consequence of the previous claim plus the standard circuit-size bound for that reduction.

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:18
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Clause decoder as linear-size circuit" rests on claim-cor-quantitative-circuits-1