Bibliographic Details
| Title: |
Design Automation With Mixtures of Proof Strategies for Propositional Logic. |
| Authors: |
Andersson, Gunnar, Bjesse, Per, Cook, Byron, Hanna, Ziyad |
| Source: |
IEEE Transactions on Computer-Aided Design of Integrated Circuits & Systems. Aug2003, Vol. 22 Issue 8, p1042. 7p. 3 Diagrams, 4 Charts. |
| Subjects: |
Proof theory, Electronic circuit design |
| Abstract: |
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. [ABSTRACT FROM AUTHOR] |
|
Copyright of IEEE Transactions on Computer-Aided Design of Integrated Circuits & Systems is the property of IEEE and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) |
| Database: |
Engineering Source |
