Boolean Satisfiability (SAT) is often used as the model for a significant and increasing number of applications in Electronics Design Automation (EDA) and many other fields of computer science and engineering. Although the SAT problem belongs to the class NP-complete - problems that do not have a polynomial run time algorithm but answers for which can be checked for correctness, by an algorithm with run time is polynomial in the size of the input - typical SAT instances are easy to solve. Both theoretical and empirical studies have been conducted on various SAT models to investigate when SAT instances become hard to solve. For more than a decade, crossover point has been the only parameter considered for hardness. Existing results state that for random SAT, the problems becomes relatively harder when the clause to variable ratio is 4.3. This thesis work is motivated by the observation that not all benchmarks at the crossover point are hard. We conjecture that the structure of the solution space is also related to the hardness. We provide an empirical framework for the validation of this conjecture. Firstly, we show by experiments that (1) the crossover point is not the only metric to characterize hardness and (2) existing benchmarks are inefficient in providing solution space information We present a novel approach to generate the SAT instances with known solution space structure. Another related issue on how to obtain the solution space information is also discussed, where we propose two probabilistic techniques for quick estimation of the solution space with high accuracy.