On Cook's Reduction and the Structure of NP Computation

Cook’s 1971 theorem is usually remembered for showing that a nondeterministic polynomial-time computation can be represented by a polynomial-size propositional formula. Cook’s original definition of polynomial reducibility, however, is stated in terms of a deterministic polynomial-time query machine with oracle access to the target set. The polynomial construction and the target-membership query are therefore distinct operations within the reduction Cook actually defines. This paper returns to that original formulation and separates those two operations. The tableau construction transforms the nondeterministic computation into a polynomial-size propositional instance. In our analysis, the construction by itself is an encoding rather than the complete reduction: the underlying recognition structure remains the same. The existence of an accepting computation has been represented as the existence of a satisfying assignment. Cook’s reduction is completed by the oracle he explicitly supplies, because the oracle returns the target-membership value and allows the deterministic query machine to determine membership in the source set. Later many-one formulations place the polynomial membership-preserving transformation itself under the name reduction, making this two-stage structure less visible. Cook’s original formulation leaves the distinction explicit: first represent the recognition problem inside the target language, then obtain the target-membership value. The paper uses that separation to examine what the propositional construction preserves before the oracle answers the resulting membership question. Cook’s tableau then provides a direct lens on the structure of NP computation. Fixing the nondeterministic choices path by path allows each bounded computation history to be represented by its own polynomial-size Cook-style formula. Taken together, these formulas expose the computation space as a potentially exponential family of polynomially bounded candidate histories. Cook’s single polynomial-size tableau represents that same family implicitly through its assignment space. The tableau compresses the family, but the recognition condition remains the same: the problem is still whether the represented family contains at least one accepting member. That preserved recognition condition reappears under further Cook encodings. Treat the resulting SAT instance as another NP recognition problem, construct its nondeterministic computation family, and encode that family with another Cook tableau. The representation can continue from computation histories to assignments, back to computation histories, and again to propositional assignments. At every stage the same form of existential condition survives: some accepting or satisfying member must exist. Without target-membership access, the process can continue producing new representations of that condition without supplying its truth value. We argue that Cook’s hypothetical oracle breaks this cascade by returning the membership answer and thus completing the reduction. This family structure also provides a way to understand modern SAT solving. Propagation, conflict analysis, clause learning, backtracking, and related methods do not need to test every complete assignment independently. They can derive consequences that eliminate or constrain entire regions of the assignment space at once. Through Cook’s tableau, those regions correspond to subfamilies of possible computations. Deterministic SAT reasoning can therefore resolve large portions of the encoded computation space collectively, while the final recognition problem remains whether the accepting portion of that space is empty or nonempty. SAT self-reducibility closes the connection in the opposite direction. If SAT membership can be determined in polynomial time, polynomially many further membership queries can recover a satisfying assignment, and Cook’s tableau then recovers the corresponding accepting computation. In the Cook–SAT setting, efficient membership determination is therefore sufficient not only to establish that an accepting computation exists, but also to recover one. The paper’s contribution is to recover the full computational structure of Cook’s original reduction and use it to trace the same recognition burden across nondeterministic computation, path-specific formulas, Cook’s compressed tableau, repeated re-encoding, modern SAT reasoning, and self-reducibility. The tableau shows how a potentially exponential computation family can be represented in polynomial size. Re-encoding shows that representation alone can continue carrying the same existential condition into new forms. Cook’s oracle marks the point at which representation becomes determination: it supplies the membership value that the encodings themselves preserve but do not compute. Cook’s original formulation therefore gives a direct lens on the P versus NP boundary. A deterministic polynomial-time algorithm does not need to reproduce any particular internal mechanism of the oracle; it must reproduce its membership answer uniformly in polynomial time. For an NP-complete target such as SAT, if deterministic polynomial time can supply that determination without oracle access, then P equals NP. If it cannot, then P does not equal NP.