claimroutineinferred_dep

Small witness circuits give nondeterministic algorithm for H

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

Statement (paper)

Let η<1/(12A)\eta<1/(12A) be a positive rational and sn=⌊ηn⌊a(n)⌋⌋s_n=\lfloor\eta n\lfloor a(n)\rfloor\rfloor. If CW(dn)⩽snC_W(dn)\le s_n for all sufficiently large nn, then HH is decided by a nondeterministic procedure that rejects nonunary inputs and, on 1n1^n, guesses a circuit on dndn index bits with at most sns_n gates, feeds the decoder's three variable labels to three copies of it, and accepts if the resulting test circuit (testing whether the indexed clause is violated) is unsatisfiable; this procedure accepts 1n1^n if and only if 1n∈H1^n\in H.

In plain English

Let η<1/(12A)\eta<1/(12A) be a positive rational and sn=⌊ηn⌊a(n)⌋⌋s_n=\lfloor\eta n\lfloor a(n)\rfloor\rfloor. If CW(dn)⩽snC_W(dn)\le s_n for all large nn, then HH is decided by a nondeterministic procedure that, on 1n1^n, guesses a circuit with at most sns_n gates on dndn index bits, plugs it into the decoder's three variable labels, and accepts exactly when the resulting test circuit is unsatisfiable.

Why it's here

This turns the hypothetical small circuits for the witness language WW into a nondeterministic algorithm for HH. Guessing a witness circuit and combining three copies with the linear-size clause decoder gives a test circuit that is unsatisfiable exactly when the guessed assignment satisfies every clause. The next claim analyzes this procedure's running time to contradict the time hierarchy theorem.
Classified routine:
This is the standard easy-witness / succinct-SAT argument in the style of Williams' 'nontrivial SAT algorithms imply circuit lower bounds': guess a small circuit for the witness and verify it with a SAT check on the composed test circuit. It follows directly from the earlier decoder and witness claims.

Uses

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

Used by

claimTest-circuit runtime contradicts time hierarchy

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Small witness circuits give nondeterministic algorithm for H" rests on claim-cor-quantitative-circuits-2
  • info
    inferred_dep
    outline: "Small witness circuits give nondeterministic algorithm for H" rests on claim-cor-quantitative-circuits-3