Exploration Barriers for SAT: Structural Lower Bounds Preserved from Search to Decision

Description This repository contains a research manuscript investigating a structural barrier to algorithmic compression for the Boolean satisfiability problem (SAT). Rather than attempting an immediate resolution of the P versus NP problem, the paper identifies and formalizes a precise obstruction that any efficient algorithm for SAT must overcome. The core result establishes that exploration—access to local constraints—cannot be compressed beyond linear bounds, even under strong coordination and parallelism. The analysis is conducted within a layered SAT framework, where constraints are organized into independently structured local blocks. Within this setting, we introduce the notion of Exposure Time, measuring how much of the input structure must be revealed before global conclusions about satisfiability become possible. The main contributions are: A linear Exposure Time lower bound for SAT search, showing that any algorithm producing a satisfying assignment must access a linear number of local blocks. A preservation principle demonstrating that lower bounds for search automatically transfer to decision, ruling out compressed decision procedures without corresponding exploration. A local flip-gadget construction establishing that, unless a block is accessed, the global satisfiability status remains information-theoretically ambiguous. Explicit equivalences connecting the framework to query complexity, communication protocols, and branching programs, yielding a unified structural interpretation. The results are unconditional, rely on exact counting arguments, and do not invoke cryptographic assumptions. While the paper does not claim a separation of P and NP, it identifies a structural barrier that any potential proof of P = NP would necessarily need to overcome. This release is intended to enable open verification, scrutiny, and discussion within the theoretical computer science community. Future versions may refine exposition or expand comparisons with related work, while preserving the core results. Abstract We investigate a structural barrier to algorithmic compression for the Boolean satisfiability problem (SAT), focusing on the inherent limitations of exploration under partial information.Rather than pursuing an immediate separation between P and NP, we identify a precise obstruction that any efficient algorithm for SAT must overcome. We introduce a layered SAT framework in which local constraints are organized into independently structured blocks, and analyze algorithms operating under bounded local access. Within this setting, we establish an Exposure Time lower bound showing that any algorithm—whether for search or decision—must access a linear number of local blocks to reliably determine satisfiability. This yields a structural non-compressibility result: exploration cannot be parallelized or shortcut beyond linear bounds, even under strong coordination. A key contribution is a preservation principle showing that lower bounds for search automatically transfer to decision. We further strengthen the result by constructing local flip gadgets demonstrating that, unless a block is accessed, the global satisfiability status remains information-theoretically ambiguous. As a consequence, decision procedures are subject to the same linear access barrier as search. Our framework unifies lower bounds across search, decision, query complexity, communication protocols, and branching programs, via explicit model equivalences. The results identify a structural barrier that any potential proof of P = NP would necessarily need to overcome, while remaining unconditional and independent of cryptographic assumptions. Keywords P vs NP SAT computational complexity structural lower bounds exploration complexity search vs decisionexposure time query complexity communication complexity branching programs non-compressibilitytheoretical computer science License CC BY 4.0