View in EDS

Design Automation With Mixtures of Proof Strategies for Propositional Logic.

Saved in:
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
FullText Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 10489135
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Design Automation With Mixtures of Proof Strategies for Propositional Logic.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Andersson%2C+Gunnar%22">Andersson, Gunnar</searchLink><br /><searchLink fieldCode="AR" term="%22Bjesse%2C+Per%22">Bjesse, Per</searchLink><br /><searchLink fieldCode="AR" term="%22Cook%2C+Byron%22">Cook, Byron</searchLink><br /><searchLink fieldCode="AR" term="%22Hanna%2C+Ziyad%22">Hanna, Ziyad</searchLink>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22IEEE+Transactions+on+Computer-Aided+Design+of+Integrated+Circuits+%26+Systems%22">IEEE Transactions on Computer-Aided Design of Integrated Circuits & Systems</searchLink>. Aug2003, Vol. 22 Issue 8, p1042. 7p. 3 Diagrams, 4 Charts.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Proof+theory%22">Proof theory</searchLink><br /><searchLink fieldCode="DE" term="%22Electronic+circuit+design%22">Electronic circuit design</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: 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]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>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.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=10489135
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1109/TCAD.2003.814959
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 7
        StartPage: 1042
    Subjects:
      – SubjectFull: Proof theory
        Type: general
      – SubjectFull: Electronic circuit design
        Type: general
    Titles:
      – TitleFull: Design Automation With Mixtures of Proof Strategies for Propositional Logic.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Andersson, Gunnar
      – PersonEntity:
          Name:
            NameFull: Bjesse, Per
      – PersonEntity:
          Name:
            NameFull: Cook, Byron
      – PersonEntity:
          Name:
            NameFull: Hanna, Ziyad
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 08
              Text: Aug2003
              Type: published
              Y: 2003
          Identifiers:
            – Type: issn-print
              Value: 02780070
          Numbering:
            – Type: volume
              Value: 22
            – Type: issue
              Value: 8
          Titles:
            – TitleFull: IEEE Transactions on Computer-Aided Design of Integrated Circuits & Systems
              Type: main
ResultId 1