
We study the computational complexity of satisfiability through a structural analysis of clause interactions in conjunctive normal form (CNF) formulas. We introduce a geometric and algebraic framework in which clauses are represented as sets over the space of primary clauses, making clause intersections explicit and enabling an exact characterization of satisfiability via the inclusion–exclusion principle. Within this framework, we define families of CNF languages characterized by their numerical capacity and by quantitative bounds on clause intersections. We show that these structural parameters induce a strict hierarchy of satisfiability problems. For the language V , defined by formulas of exact numerical capacity, satisfiability is decidable in polynomial time, while linear-time decision is provably insufficient. For the language A, obtained by adjoining a single clause to formulas in V, we show that satisfiability remains polynomial-time decidable when the intersection width is bounded by a fixed constant. In contrast, for the subclass A*, in which the clause–intersection degree grows unboundedly but remains o(log r), we prove that satisfiability is not polynomial-time decidable. Our results establish explicit connections between clause–intersection geometry, algebraic representations of SAT via inclusion–exclusion, and fundamental limits on stepwise information acquisition by deterministic machines. Within this framework, we establish a separation between P and NP. Furthermore, we show that this approach operates outside the scope of known barriers such as relativization, natural proofs and algebrization. This version supersedes two earlier versions of the manuscript previously deposited on TechRxiv: DOI: https://doi.org/10.36227/techrxiv.172767346.60561665/v1 DOI: https://doi.org/10.36227/techrxiv.172767346.60561665/v2 These earlier versions contain preliminary and intermediate results. The present version introduces substantial revisions, including structural changes and updated results.
