Circuit-SAT 解空间的几何：刚性、连通阈值与拓扑结构

We study the geometry of circuit-SAT solution spaces over the complete binary basis B₂. For each of the 222 NPN-equivalence classes of 4-input Boolean functions, we encode minimum-size circuits as satisfiability instances, enumerate structurally distinct solutions, and construct the local-move graph, a reconfiguration graph where edges connect circuits differing by a single-gate edit.

The local-move graph at minimum circuit size C(f) exhibits a three-phase connectivity structure: connected at C ≤ 1, totally isolated at C = 2, and fragmented into multiple components at C ≥ 3. At C = 2, every minimum-size circuit is an isolated vertex (18/18 circuits across 5 NPN classes); all 218 classes with C ≥ 2 are disconnected (zero violations). We prove that total isolation at C = 2 is a mathematical necessity for all n ≥ 3: every minimum-size 2-gate circuit is fully exercised. A single gate of slack (δ = 1) produces giant connected components in 220 of 222 classes (99.1%).

We also identify a distance/count asymmetry: counting metrics (solution count, component count) are uncorrelated with C(f), while the minimax linkage distance correlates with C(f) (rₛ = 0.867 raw, rₛ = 0.338 after normalising for encoding dimension). Persistent homology detects nontrivial H₁ loops in 96.8% of solution spaces; normalising H₁ persistence by the H₀ max-persistence reveals that loops close at shorter relative distances as complexity increases (rₛ = −0.837).

The full dataset comprises 665 instance–size pairs across three slack levels, totalling over 200,000 enumerated circuits. Partial verification at n = 5 (all 25 NPN classes with C(f) ∈ {2,3}) exhibits the same three-phase structure.