Random 3-SAT formulas above the satisfiability threshold are a canonical source of hard instances for both SAT algorithms and proof systems. In this work, we propose a unified, instance-level explanation for this hardness based on two unconditional properties: structural explosion and semantic irreducibility. We introduce the Assignment-DAG Partition Complexity (ADPC) and prove that the space of partial assignments fragments into exponentially many locally distinguishable subproblems. We then introduce the Semantic Depth Invariant (SDI) and prove that SDI(F)=Omega(n), establishing that unsatisfiability is a global property invisible to bounded-local verifiers. Finally, we demonstrate that SDI strictly subsumes Resolution width, recovering classical exponential lower bounds as a direct corollary.
Harsha Vardhan Routhu (Wed,) studied this question.