  Satisfiability is considered the canonical NP-complete problem and is used as
a starting point for hardness reductions in theory, while in practice heuristic
SAT solving algorithms can solve large-scale industrial SAT instances very
efficiently. This disparity between theory and practice is believed to be a
result of inherent properties of industrial SAT instances that make them
tractable. Two characteristic properties seem to be prevalent in the majority
of real-world SAT instances, heterogeneous degree distribution and locality. To
understand the impact of these two properties on SAT, we study the proof
complexity of random k-SAT models that allow to control heterogeneity and
locality. Our findings show that heterogeneity alone does not make SAT easy as
heterogeneous random k-SAT instances have superpolynomial resolution size. This
implies intractability of these instances for modern SAT-solvers. On the other
hand, modeling locality with an underlying geometry leads to small
unsatisfiable subformulas, which can be found within polynomial time.
  A key ingredient for the result on geometric random k-SAT can be found in the
complexity of higher-order Voronoi diagrams. As an additional technical
contribution, we show a linear upper bound on the number of non-empty Voronoi
regions, that holds for points with random positions in a very general setting.
In particular, it covers arbitrary p-norms, higher dimensions, and weights
affecting the area of influence of each point multiplicatively. This is in
stark contrast to quadratic lower bounds for the worst case.
