Design automation with mixtures of proof strategies for propositional logic

Design automation problems can often be encoded in propositional logic, and solved by applying propositional logic proof methods. Unfortunately, there exists no single proof method with adequate performance for all problems of interest. It is, therefore, critical to be able to combine different approaches, and to quickly be able to test how different compositions affect overall performance. In this paper, we present a proof engine framework where individual methods 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. Unlike previous approaches, our framework is flexible enough to allow users to quickly come up with specially tailored composite analyses for problems from any of the different subdomains of design automation. We show how several known analyses for solving design automation problems encoded in propositional logic can be integrated as base strategies in our framework. As a proof-of-concept, and to demonstrate the power inherent in the framework, we also present experimental results that show the performance of two default composite strategies that we have developed using the framework over a period of several years. These strategies are often one to two magnitudes faster when compared with binary decision diagram-based techniques and search-based satisfiability solvers such as ZCHAFF. The introduction of the framework was the key facilitator in the development of these default strategies.