A proof engine approach to solving combinational design automation problems

There are many approaches available for solving combinational design automation problems encoded as tautology or satisfiability checks. Unfortunately there exists no single analysis that gives adequate performance for all problems of interest, and it is therefore critical to be able to combine approaches. In this paper, we present a proof engine framework where individual analyses are viewed as strategies-functions between different proof states. By defining our proof engine in such a way that we can compose strategies to form new, more powerful, strategies we achieve synergistic effects between the individual methods. The resulting framework has enabled us to develop a small set of powerful composite default strategies. We describe several strategies and their interplay; one of the strategies, variable instantiation, is new. The strength of our approach is demonstrated with experimental results showing that our default strategies can achieve up to several magnitudes of speed-up compared to BDD-based techniques and search-based satisfiability solvers such as ZCHAFF.