corollaryroutine

Fast inversion of local Boolean maps

Corollary·cor:consequence-local-inversion·§C.2 Inverting Boolean maps with constant output locality

Statement (paper)

For every fixed dd and n⩾20n\ge20, the number ∣G−1(b⃗)∣|G^{-1}(\vec{b})| can be computed exactly, and a preimage can be found whenever one exists, in deterministic time (n+m)Od(1)2Od(ρ(n)) (n+m)^{O_d(1)}2^{O_d(\rho(n))} and space (n+m)Od(1)(n+m)^{O_d(1)}.

In plain English

For a Boolean map GG with output locality bounded by a fixed dd and a target b⃗\vec{b}, one can count the preimages ∣G−1(b⃗)∣|G^{-1}(\vec{b})| exactly and find a preimage if one exists, in time (n+m)Od(1)2Od(ρ(n))(n+m)^{O_d(1)}2^{O_d(\rho(n))} and polynomial space (n+m)Od(1)(n+m)^{O_d(1)}, for n⩾20n\ge20.

Why it's here

Each output bit of GG depends on at most dd input bits, so the equation G(x)=b⃗G(x)=\vec{b} is a dd-CNF constraint system, and the main counting theorem applies with ρ(n)\rho(n) as its savings term. This turns the subexponential model-counting algorithm into a subexponential inversion algorithm for local maps, including search via the count.
Classified routine:
Direct consequence of the paper's main k-CNF model-counting theorem (thm-main): each local output constraint G_i(x)=b_i is written as a d-CNF of at most 2^d clauses, and search reduces to counting by the standard self-reducibility argument of fixing variables one at a time.

Uses

thmSubexponential deterministic k-CNF model counting

Used by

Nothing in the paper

Sources

PaperOpen
Section
§C.2 Inverting Boolean maps with constant output locality
Page
—
Label
cor:consequence-local-inversion
Line
main_full_version.tex:4284
Leannot aligned

Phase 2 aligns this node to a Lean declaration.