Boolean Satisfiability solvers are widely used in many VLSI Computer Aided Design applications. Their popularity is due to recent developments such as effective search space pruning, decision making, and learning from previous mistakes. Most SAT algorithms and performance improvement techniques focus on the core engine and do not exploit circuit specific properties. Historically, properties such as don't care conditions have played an important role in problems such as test pattern generation and circuit synthesis. This thesis presents a number of techniques that increase SAT solver performance by taking advantage of circuit don't care conditions. General strategies and specific heuristics are developed that utilize a circuit's observability don't cares; controllability don't cares, and don't care states to improve SAT solver efficiency for formal verification problems. Extensive experiments demonstrate the benefits of don't care conditions on benchmark suites as well as industrial circuits.