Random 2-CNF formulas undergo a satisfiability phase transition at clause density 1 — below this density, almost all formulas are satisfiable; above, almost none are. The treewidth of the formula's variable interaction graph undergoes a transition at density 1/2 — below, the formula is tree-like; above, it has unbounded treewidth.
Lagniez, Monet, and Ganian discover that these two thresholds define a trichotomy for compilability into Ordered Binary Decision Diagrams (OBDDs). Below density 1/2: OBDD compilation succeeds with polynomial size. Between 1/2 and 1: the formula is satisfiable but the smallest OBDD is exponential. Above 1: the formula is unsatisfiable, and the OBDD is trivially small (it represents “false”).
The middle regime is the surprise. The formula is satisfiable, its solution set is simple to describe (it's large — an exponential number of satisfying assignments exist), but compiling it into an OBDD requires exponential space. The bottleneck isn't the solution structure — it's the interaction structure. The treewidth transition at 1/2 creates entanglement between variables that OBDDs cannot efficiently represent, regardless of how the variables are ordered.
Three regimes. Two thresholds. Both from classical combinatorics (random graphs, satisfiability), both exactly aligned with the compilability transition. The compilation difficulty of a formula is not about what it says but about how its variables interact.