Polynomial Fault Detection Without Bounded Width: Exact Reachable Sets in Priority Controllers

Circuit-width restrictions give several polynomial cases of automatic test pattern generation. We study a generalized c432 priority controller whose first-stage bridge-fault detection problem is polynomial even on a subfamily with linear treewidth and net cut-width in its specified native layout. No fixed bounds on block inputs and block-graph treewidth cover this subfamily. The tractability mechanism is a constructive description of the qualifier sets that the fault can produce, valid for every controller size. The controller has n channels and b request buses; the c432 selector is the case n=9, b=3. We determine the exact eligible sets reachable under the specified bridge fault and construct a primary input for every admitted set. For guarded decoders, supporting paths and classical dual-Horn reasoning decide detection and construct a detecting eligible set in O((n+q)G) time, where q is the number of observed outputs and G counts channel inputs, decoder nodes, and child, guard and output incidences. With no shared internal gates, the decoder work is O(G). Writing a primary-input test or full native model adds O(N), where N is the complete native encoding size. The same image supports P-completeness of detection, NP-hardness of minimum detecting eligible sets, #P-completeness of counting distinct detecting eligible sets, and an exponential DNNF representation lower bound. Unbounded conjunctions of two computed children make detection NP-complete. For the original guarded class, the specified complete encoding admits ordinary resolution refutations with O(N^3) inferences. The worst-case cost of recovering circuit roles from an arbitrary CNF remains open. Standard SAT solvers are faster than the family implementation on the generated decision panels. The extensions characterize stage-local bridge images and exact healthy/faulty pairs for a fault confined to one final-qualifier request occurrence. Detection for the latter fault is NP-complete on supplied guarded DAGs, while unshared formula forests admit an O(G^2) algorithm. Supporting-path and positive-clause parameters give further algorithmic bounds. The source archive contains the manuscript, four figures, and portable finite checks for the fault-model extensions. It does not contain the full native compiler or Lean development. The new extensions are proved in the manuscript but are not included in the earlier Lean formalization. OpenAI Codex assisted with mathematical exploration, Lean formalization, and manuscript preparation. The author reviewed the AI-assisted material and takes full responsibility for the manuscript.