Managing don´t cares in Boolean satisfiability

Advances in Boolean satisfiability solvers have popularized their use in many of today´s CAD VLSI challenges. Existing satisfiability solvers operate on a circuit representation that does not capture all of the structural circuit characteristics and properties. This work proposes algorithms that take into account the circuit don´t care conditions thus enhancing the performance of these tools. Don´t care sets are addressed in this work both statically and dynamically to reduce the search space and guide the decision making process. Experiments demonstrate performance gains.