Exploring variable elimination as a preprocessing technique to speed up SAT

The use of SAT solvers in EDA applications has grown enormously in the last decade. This has only been possible due to the fact that state-of-the-art SAT solvers have achieved breakthrough performance in handling problem sizes and reducing run time. As the applications and usability of SAT solvers increase, it is more important to improve performance in addition to maintaining correctness.;Preprocessing as an optimization method for SAT Solvers has been explored in many ways. Several algorithms apply different methods to simplify the input problem before it is passed on to the SAT engine. NiVER [18] explored variable elimination resolution, Hypre [2] used hyper binary resolution to simplify the input problem, SatELite [8] explored the combination of variable elimination and subsumption to reduce the size of the input problem and Alembic [10] presented a unique distillation process to increase the deductive power of the SAT engine which is enabled by using self-subsumption, subsumption and variable elimination hand in hand.;This thesis tries to explore the capability and limitations of variable elimination resolution as a preprocessing technique for Propositional Satisfiability problems expressed in the Conjunctive Normal Form (CNF). The concept of eliminating variables in the SAT problem and hence, simplifying the SAT problem will in effect make solving the problem an easier task has been assumed. And with this assumption, various levels of variable elimination have been implemented, experimented and tested in collaboration with CirCUs 2.0 Satisfiability Solver developed at University of Colorado at Boulder.