Polynomial Fault Detection Without Bounded Width: Exact Reachable Sets in Priority Controllers
A mix of human-written and AI-generated textHuman understanding: all partscs.CC — Computational Complexitycs.DS — Data Structures and Algorithmscs.LO — Logic in Computer Science
Contributed by Idris Ali Shaik ↗
Version 1 / Oct 23, 2026 / CC BY 4.0
Abstract
Circuit-width restrictions explain several polynomial cases of automatic test pattern generation. We give a different explanation for an arbitrary-size extension of the c432 priority controller, including a subfamily with linear treewidth and net cut-width in its native layout. For a specified first-stage bridge fault, we characterize exactly the reachable qualifier sets and construct a primary input realizing each one. On drive-one inputs where the first selector flag changes, the healthy set is the target singleton; the faulty sets are precisely the target-containing sets with one request bus and all nonempty sets with at least two buses. Drive zero is undetectable. This image reduces detection to comparing decoder values on sets. For supplied guarded decoders, built from zero, positive channel leaves, disjunction and conjunction of one computed child with negative channel literals, supporting paths and dual-Horn reasoning find a detecting set in O((n+q)G) time for n channels, q outputs and counted decoder size G, or O(G) for formula forests. Unsatisfiable instances of the complete guarded native CNF encoding have resolution refutations with O(N³) inferences, where N is the encoding size. Detection is P-complete, while minimum-set optimization and counting detecting sets are NP-hard and #P-complete, respectively. A specified final-qualifier stuck-at fault makes detection NP-complete on shared guarded decoders. The exact first-stage bridge-image statements are formalized in Lean and registered as PALOMAR-2026-10-19-000010, version 1.
Provenance statement
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.
Formalizations
References
No bibliography entries.
Version history
- v1Submitted by Idris Ali ShaikInitial depositCurrentOct 23, 2026