Does MiniSAT need exponential time?
When pure CDCL solvers (such as MiniSAT, I believe) are run on unsatisfiable instances, their transcript can be converted to a Resolution refutation of the instance. In particular, the running time of the solver is lower bounded by the length of the smallest Resolution refutation of the instance. There are instances which are known to take exponential length to refute in Resolution, for example the Pigeonhole Principle on $n+1$ pigeons and $n$ holes. Such instances will take exponential time to refute on any pure CDCL solver.