Conflict-driven clause-learning (CDCL) SAT solvers routinely solve formulas with thousands to millions of variables and clauses, despite the satisfiability problem being NP-complete. At the same time, small randomly generated formulas are difficult for the same solvers. The goal of this work is to understand which aspects or measures of SAT formulas relate best to SAT solver performance, and further to relate these measures to SAT solver heuristic behavior.