SFR–FLP–AFS: A Structural–Fidelity Framework for Capturing the Hardness of NP Problems
The Cook–Levin theorem establishes the NP-completeness of SAT by encoding an exponentially branching nondeterministic computation into a single polynomial-size Boolean formula. While this compression proves completeness, it obscures the structural source of SAT’s hardness: the exponential search inherent in nondeterministic computation. Standard explanations, such as claiming that SAT is hard because all NP problems reduce to it, therefore provide little insight into what actually makes NP problems difficult. This paper introduces the Formula Location Problem (FLP) as the primitive structure underlying NP-hardness. Instead of collapsing all computation paths into a single formula, our Structural Fidelity Reduction (SFR) applies the same reduction technique used in Cook’s original 1971 construction, but preserves the structure of the computation tree by generating a separate Boolean formula for each nondeterministic path. This produces a family {Fπ} that explicitly mirrors the branching behavior of the machine and exposes the underlying location problem: identifying an accepting path among exponentially many rejecting ones. Within this framework, every NP problem can be viewed as an instance of FLP, with SAT, TSP, 3-coloring, and other classical NP-complete problems appearing only as surface-level encodings of the same underlying structure. This perspective yields a natural decomposition of NP computation into polynomial-time generation, exponentialtime location, and polynomial-time verification. We further show that a polynomial-time Accepting Formula Selector (AFS), an algorithm capable of solving FLP, exists if and only if P equals NP. By isolating FLP as the structural source of NP-hardness, this framework clarifies why modern SAT solvers perform effectively in practice: their heuristics exploit geometric regularities in the rejection space of FLP instances rather than solving the general location problem outright.
Institutions
- 's Heeren Loo (NL)
- Michigan State University (US)
Publication Details
- Journal
- Zenodo (CERN European Organization for Nuclear Research)
- Published
- 2025-11-27
- DOI
- https://doi.org/10.5281/zenodo.17733578
- Primary Topic
- Formal Methods in Verification
- Type
- article
- Field-Weighted Citation Impact
- 0.00