Global rebuilding of OBDDs avoiding memory requirement maxima
Identifieur interne : 001234 ( Istex/Corpus ); précédent : 001233; suivant : 001235Global rebuilding of OBDDs avoiding memory requirement maxima
Auteurs : Jochen Bern ; Christoph Meinel ; Anna SlobodováSource :
- Lecture Notes in Computer Science [ 0302-9743 ] ; 1995.
Abstract
Abstract: It is well-known that the size of an ordered binary decision diagram (OBDD) may depend crucially on the order in which the variables occur. In the paper, we describe an implementation of an outputefficient algorithm that transforms an OBDD P representing a Boolean function f with respect to one variable ordering π into an OBDD Q that represents f with respect to another variable ordering σ. The algorithm runs in average time O(¦P∥Q¦) and requires O(¦P¦+n¦Q¦) space. The importance of the algorithm is demonstrated by means of experimental results on basically two different applications. In one of them, the algorithm is used merely once. Such transformations are needed to test equivalence or to perform synthesis on OBDDs in which variables appear in different orders. The other application shows a way how to decrease the size of intermediate representations in the course of the construction of OBDDs from a given circuit. Here the algorithm is used dynamically, whenever the size of the manipulated OBDDs becomes too large.
Url:
DOI: 10.1007/3-540-60045-0_36
Links to Exploration step
ISTEX:5D5A86C8E465CA1550E5C48D995BD6ED6645839ALe document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Global rebuilding of OBDDs avoiding memory requirement maxima</title><author><name sortKey="Bern, Jochen" sort="Bern, Jochen" uniqKey="Bern J" first="Jochen" last="Bern">Jochen Bern</name><affiliation><mods:affiliation>University of Trier, D-54286, Trier, Germany</mods:affiliation></affiliation></author><author><name sortKey="Meinel, Christoph" sort="Meinel, Christoph" uniqKey="Meinel C" first="Christoph" last="Meinel">Christoph Meinel</name><affiliation><mods:affiliation>University of Trier, D-54286, Trier, Germany</mods:affiliation></affiliation></author><author><name sortKey="Slobodova, Anna" sort="Slobodova, Anna" uniqKey="Slobodova A" first="Anna" last="Slobodová">Anna Slobodová</name><affiliation><mods:affiliation>University of Trier, D-54286, Trier, Germany</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:5D5A86C8E465CA1550E5C48D995BD6ED6645839A</idno><date when="1995" year="1995">1995</date><idno type="doi">10.1007/3-540-60045-0_36</idno><idno type="url">https://api.istex.fr/document/5D5A86C8E465CA1550E5C48D995BD6ED6645839A/fulltext/pdf</idno><idno type="wicri:Area/Istex/Corpus">001234</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001234</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Global rebuilding of OBDDs avoiding memory requirement maxima</title><author><name sortKey="Bern, Jochen" sort="Bern, Jochen" uniqKey="Bern J" first="Jochen" last="Bern">Jochen Bern</name><affiliation><mods:affiliation>University of Trier, D-54286, Trier, Germany</mods:affiliation></affiliation></author><author><name sortKey="Meinel, Christoph" sort="Meinel, Christoph" uniqKey="Meinel C" first="Christoph" last="Meinel">Christoph Meinel</name><affiliation><mods:affiliation>University of Trier, D-54286, Trier, Germany</mods:affiliation></affiliation></author><author><name sortKey="Slobodova, Anna" sort="Slobodova, Anna" uniqKey="Slobodova A" first="Anna" last="Slobodová">Anna Slobodová</name><affiliation><mods:affiliation>University of Trier, D-54286, Trier, Germany</mods:affiliation></affiliation></author></analytic><monogr></monogr><series><title level="s">Lecture Notes in Computer Science</title><imprint><date>1995</date></imprint><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series><idno type="istex">5D5A86C8E465CA1550E5C48D995BD6ED6645839A</idno><idno type="DOI">10.1007/3-540-60045-0_36</idno><idno type="ChapterID">2</idno><idno type="ChapterID">Chap2</idno></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: It is well-known that the size of an ordered binary decision diagram (OBDD) may depend crucially on the order in which the variables occur. In the paper, we describe an implementation of an outputefficient algorithm that transforms an OBDD P representing a Boolean function f with respect to one variable ordering π into an OBDD Q that represents f with respect to another variable ordering σ. The algorithm runs in average time O(¦P∥Q¦) and requires O(¦P¦+n¦Q¦) space. The importance of the algorithm is demonstrated by means of experimental results on basically two different applications. In one of them, the algorithm is used merely once. Such transformations are needed to test equivalence or to perform synthesis on OBDDs in which variables appear in different orders. The other application shows a way how to decrease the size of intermediate representations in the course of the construction of OBDDs from a given circuit. Here the algorithm is used dynamically, whenever the size of the manipulated OBDDs becomes too large.</div></front></TEI><istex><corpusName>springer</corpusName><author><json:item><name>Jochen Bern</name><affiliations><json:string>University of Trier, D-54286, Trier, Germany</json:string></affiliations></json:item><json:item><name>Christoph Meinel</name><affiliations><json:string>University of Trier, D-54286, Trier, Germany</json:string></affiliations></json:item><json:item><name>Anna Slobodová</name><affiliations><json:string>University of Trier, D-54286, Trier, Germany</json:string></affiliations></json:item></author><language><json:string>eng</json:string></language><originalGenre><json:string>ReviewPaper</json:string></originalGenre><abstract>Abstract: It is well-known that the size of an ordered binary decision diagram (OBDD) may depend crucially on the order in which the variables occur. In the paper, we describe an implementation of an outputefficient algorithm that transforms an OBDD P representing a Boolean function f with respect to one variable ordering π into an OBDD Q that represents f with respect to another variable ordering σ. The algorithm runs in average time O(¦P∥Q¦) and requires O(¦P¦+n¦Q¦) space. The importance of the algorithm is demonstrated by means of experimental results on basically two different applications. In one of them, the algorithm is used merely once. Such transformations are needed to test equivalence or to perform synthesis on OBDDs in which variables appear in different orders. The other application shows a way how to decrease the size of intermediate representations in the course of the construction of OBDDs from a given circuit. Here the algorithm is used dynamically, whenever the size of the manipulated OBDDs becomes too large.</abstract><qualityIndicators><score>6.263</score><pdfVersion>1.3</pdfVersion><pdfPageSize>439.208 x 662.424 pts</pdfPageSize><refBibsNative>false</refBibsNative><keywordCount>0</keywordCount><abstractCharCount>1042</abstractCharCount><pdfWordCount>4259</pdfWordCount><pdfCharCount>24706</pdfCharCount><pdfPageCount>12</pdfPageCount><abstractWordCount>167</abstractWordCount></qualityIndicators><title>Global rebuilding of OBDDs avoiding memory requirement maxima</title><chapterId><json:string>2</json:string><json:string>Chap2</json:string></chapterId><refBibs><json:item><author><json:item><name>M Blum</name></json:item><json:item><name>A,K Chandra</name></json:item><json:item><name>M,N Wegman</name></json:item></author><host><volume>0</volume><pages><last>82</last><first>80</first></pages><issue>2</issue><author></author><title>Inf. Process . Lett</title><publicationDate>1980-03</publicationDate></host><title>Equivalence of Free Boolean Graphs Can Be Decided ProbabilisticaUy in Polynomial Time</title><publicationDate>1980-03</publicationDate></json:item><json:item><host><author><json:item><name>J Bern</name></json:item><json:item><name> Ch</name></json:item><json:item><name>A Meinel</name></json:item></author><title>Slobodov~: T~-U---sT -a Programming Environment for the FBDD-package, in print</title><publicationDate>1994</publicationDate></host></json:item><json:item><author><json:item><name>K,S Brace</name></json:item><json:item><name>R,L Rudeu</name></json:item><json:item><name>R,E K M Bryant</name></json:item><json:item><name>D,E Butler</name></json:item><json:item><name>R Ross</name></json:item><json:item><name>M,R Kaput</name></json:item><json:item><name> Mercer</name></json:item></author><host><pages><last>45</last><first>40</first></pages><author></author><title>Efficient Implementation of a BDD Package Proc. of 27th ACM/IEEE Design Automation Conference Proc. 28th ACM</title><publicationDate>1990-06</publicationDate></host><title>Heuristics to Compute Variable Orderings for Efficient Manipulation of Ordered Binary Decision Diagrams</title><publicationDate>1990-06</publicationDate></json:item><json:item><author><json:item><name>R,E Bryant</name></json:item></author><host><volume>6</volume><pages><last>691</last><first>677</first></pages><issue>542</issue><author></author><title>IEEE Trans. Comput. C-35</title><publicationDate>1986-08</publicationDate></host><title>Graph-Based Algorithms for Boolean Function Manipulation B. Bollig, I. Wegener: Improving the Variable Ordering of OBDDs is NP- Complete, Forschungsbericht Nr</title><publicationDate>1986-08</publicationDate></json:item><json:item><author><json:item><name>M Fujita</name></json:item><json:item><name>H Fujisawa</name></json:item><json:item><name>N Kawato</name></json:item></author><host><pages><last>5</last><first>2</first></pages><author></author><title>Proc. of IEEE ICCAD</title><publicationDate>1988</publicationDate></host><title>Evaluation and Improvements of Boolean Comparison Method Based on Binary Decision Diagrams</title><publicationDate>1988</publicationDate></json:item><json:item><author><json:item><name>M Fujita</name></json:item><json:item><name>Y Matsunaga</name></json:item><json:item><name>T Kakuda</name></json:item></author><host><pages><last>53</last><first>50</first></pages><author></author><title>Proc. of EDAC</title><publicationDate>1991</publicationDate></host><title>On Variable Ordering of Binary Decision Diagrams for the Appfication of Multi-Valued Logic Synthesis</title><publicationDate>1991</publicationDate></json:item><json:item><author><json:item><name>S,J Friedman</name></json:item><json:item><name>K,J S Supowit</name></json:item><json:item><name>N Minato</name></json:item><json:item><name>S,M R Ishiura</name></json:item><json:item><name>R Mercer</name></json:item><json:item><name>D,E Kaput</name></json:item><json:item><name>Ross Malik</name></json:item><json:item><name>A Wang</name></json:item><json:item><name>R,K Brayton</name></json:item><json:item><name>A Sangiovanni-Vincenteui</name></json:item></author><host><pages><last>713</last><first>710</first></pages><author></author><title>Proc. of the 27th ACM/1EEE Design Automation Conference Functional Approaches to Generating Orderings for Efficient Symbolic Representation. Proc. of 29th ACM/IEEE DAC Proc. of the IEEE International Conference on Computer-Aided Design</title><publicationDate>1988</publicationDate></host><title>Finding the Optimal Variable Ordering for binary Decision Diagrams Yajima: Shared Binary Decision Diagrams with Attributed edges for Efficient Boolean Function Manipulation</title><publicationDate>1988</publicationDate></json:item><json:item><author><json:item><name> Ch</name></json:item><json:item><name>A Meinel</name></json:item><json:item><name> Slobodov~i</name></json:item></author><host><pages><last>524</last><first>515</first></pages><author></author><title>Proc. of MFCS'94 Proc. of IEEE ICCAD</title><publicationDate>1993</publicationDate></host><title>On the Complexity of Constructing optimal Ordered Binary Decision Diagrams R. Rudell: Dynamic Variable Ordering for Ordered Binary Decision Diagrams</title><publicationDate>1993</publicationDate></json:item><json:item><author><json:item><name>P Savick~</name></json:item><json:item><name>I,S Wegener</name></json:item><json:item><name>K Tan_I</name></json:item><json:item><name>S,S Hamaguchi</name></json:item><json:item><name>H Tani</name></json:item><json:item><name> Imai</name></json:item></author><host><pages><last>398</last><first>389</first></pages><author></author><title>Proc. FST&TCS Proc. 4th ISAAC Proc. of 5th ISAAC</title><publicationDate>1993</publicationDate></host><title>Efficient Algorithms for the Transformation Between Different Types of Binary Decision Diagrams Yajima: The Complexity of the Optimal Variable Ordering of a Shared Binary Decision Diagram A Reordering for an Ordered Binary Decision Diagram and an Extended Framework for Combinatorics of Graphs</title><publicationDate>1993</publicationDate></json:item></refBibs><genre><json:string>conference</json:string></genre><serie><editor><json:item><name>Gerhard Goos</name></json:item><json:item><name>Juris Hartmanis</name></json:item><json:item><name>Jan van Leeuwen</name></json:item></editor><issn><json:string>0302-9743</json:string></issn><language><json:string>unknown</json:string></language><eissn><json:string>1611-3349</json:string></eissn><title>Lecture Notes in Computer Science</title><copyrightDate>1995</copyrightDate></serie><host><editor><json:item><name>Pierre Wolper</name></json:item></editor><subject><json:item><value>Computer Science</value></json:item><json:item><value>Computer Science</value></json:item><json:item><value>Logics and Meanings of Programs</value></json:item><json:item><value>Software Engineering</value></json:item><json:item><value>Mathematical Logic and Formal Languages</value></json:item><json:item><value>Electronics and Microelectronics, Instrumentation</value></json:item><json:item><value>Special Purpose and Application-Based Systems</value></json:item><json:item><value>Artificial Intelligence (incl. Robotics)</value></json:item></subject><isbn><json:string>978-3-540-60045-9</json:string></isbn><language><json:string>unknown</json:string></language><eissn><json:string>1611-3349</json:string></eissn><title>Computer Aided Verification</title><bookId><json:string>3540600450</json:string></bookId><volume>939</volume><pages><last>15</last><first>4</first></pages><issn><json:string>0302-9743</json:string></issn><genre><json:string>book-series</json:string></genre><eisbn><json:string>978-3-540-49413-3</json:string></eisbn><copyrightDate>1995</copyrightDate><doi><json:string>10.1007/3-540-60045-0</json:string></doi></host><publicationDate>2005</publicationDate><copyrightDate>1995</copyrightDate><doi><json:string>10.1007/3-540-60045-0_36</json:string></doi><id>5D5A86C8E465CA1550E5C48D995BD6ED6645839A</id><score>1.7069787</score><fulltext><json:item><extension>pdf</extension><original>true</original><mimetype>application/pdf</mimetype><uri>https://api.istex.fr/document/5D5A86C8E465CA1550E5C48D995BD6ED6645839A/fulltext/pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/document/5D5A86C8E465CA1550E5C48D995BD6ED6645839A/fulltext/zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/document/5D5A86C8E465CA1550E5C48D995BD6ED6645839A/fulltext/tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Global rebuilding of OBDDs avoiding memory requirement maxima</title><respStmt><resp>Références bibliographiques récupérées via GROBID</resp><name resp="ISTEX-API">ISTEX-API (INIST-CNRS)</name></respStmt><respStmt><resp>Références bibliographiques récupérées via GROBID</resp><name resp="ISTEX-API">ISTEX-API (INIST-CNRS)</name></respStmt></titleStmt><publicationStmt><authority>ISTEX</authority><publisher>Springer Berlin Heidelberg</publisher><pubPlace>Berlin, Heidelberg</pubPlace><availability><p>Springer-Verlag, 1995</p></availability><date>1995</date></publicationStmt><sourceDesc><biblStruct type="inbook"><analytic><title level="a" type="main" xml:lang="en">Global rebuilding of OBDDs avoiding memory requirement maxima</title><author xml:id="author-1"><persName><forename type="first">Jochen</forename><surname>Bern</surname></persName><affiliation>University of Trier, D-54286, Trier, Germany</affiliation></author><author xml:id="author-2"><persName><forename type="first">Christoph</forename><surname>Meinel</surname></persName><affiliation>University of Trier, D-54286, Trier, Germany</affiliation></author><author xml:id="author-3"><persName><forename type="first">Anna</forename><surname>Slobodová</surname></persName><affiliation>University of Trier, D-54286, Trier, Germany</affiliation></author></analytic><monogr><title level="m">Computer Aided Verification</title><title level="m" type="sub">7th International Conference, CAV '95 Liège, Belgium, July 3–5, 1995 Proceedings</title><idno type="pISBN">978-3-540-60045-9</idno><idno type="eISBN">978-3-540-49413-3</idno><idno type="pISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="DOI">10.1007/3-540-60045-0</idno><idno type="book-ID">3540600450</idno><idno type="book-title-ID">42727</idno><idno type="book-volume-number">939</idno><idno type="book-chapter-count">34</idno><editor><persName><forename type="first">Pierre</forename><surname>Wolper</surname></persName></editor><imprint><publisher>Springer Berlin Heidelberg</publisher><pubPlace>Berlin, Heidelberg</pubPlace><date type="published" when="2005-05-31"></date><biblScope unit="volume">939</biblScope><biblScope unit="page" from="4">4</biblScope><biblScope unit="page" to="15">15</biblScope></imprint></monogr><series><title level="s">Lecture Notes in Computer Science</title><editor><persName><forename type="first">Gerhard</forename><surname>Goos</surname></persName></editor><editor><persName><forename type="first">Juris</forename><surname>Hartmanis</surname></persName></editor><editor><persName><forename type="first">Jan</forename><surname>van Leeuwen</surname></persName></editor><biblScope><date>1995</date></biblScope><idno type="pISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="series-Id">558</idno></series><idno type="istex">5D5A86C8E465CA1550E5C48D995BD6ED6645839A</idno><idno type="DOI">10.1007/3-540-60045-0_36</idno><idno type="ChapterID">2</idno><idno type="ChapterID">Chap2</idno></biblStruct></sourceDesc></fileDesc><profileDesc><creation><date>1995</date></creation><langUsage><language ident="en">en</language></langUsage><abstract xml:lang="en"><p>Abstract: It is well-known that the size of an ordered binary decision diagram (OBDD) may depend crucially on the order in which the variables occur. In the paper, we describe an implementation of an outputefficient algorithm that transforms an OBDD P representing a Boolean function f with respect to one variable ordering π into an OBDD Q that represents f with respect to another variable ordering σ. The algorithm runs in average time O(¦P∥Q¦) and requires O(¦P¦+n¦Q¦) space. The importance of the algorithm is demonstrated by means of experimental results on basically two different applications. In one of them, the algorithm is used merely once. Such transformations are needed to test equivalence or to perform synthesis on OBDDs in which variables appear in different orders. The other application shows a way how to decrease the size of intermediate representations in the course of the construction of OBDDs from a given circuit. Here the algorithm is used dynamically, whenever the size of the manipulated OBDDs becomes too large.</p></abstract><textClass><keywords scheme="Book-Subject-Collection"><list><label>SUCO11645</label><item><term>Computer Science</term></item></list></keywords></textClass><textClass><keywords scheme="Book-Subject-Group"><list><label>I</label><label>I1603X</label><label>I14029</label><label>I16048</label><label>T24027</label><label>I13030</label><label>I21017</label><item><term>Computer Science</term></item><item><term>Logics and Meanings of Programs</term></item><item><term>Software Engineering</term></item><item><term>Mathematical Logic and Formal Languages</term></item><item><term>Electronics and Microelectronics, Instrumentation</term></item><item><term>Special Purpose and Application-Based Systems</term></item><item><term>Artificial Intelligence (incl. Robotics)</term></item></list></keywords></textClass></profileDesc><revisionDesc><change when="2005-05-31">Published</change><change xml:id="refBibs-istex" who="#ISTEX-API" when="2016-11-22">References added</change><change xml:id="refBibs-istex" who="#ISTEX-API" when="2017-01-20">References added</change></revisionDesc></teiHeader></istex:fulltextTEI><json:item><extension>txt</extension><original>false</original><mimetype>text/plain</mimetype><uri>https://api.istex.fr/document/5D5A86C8E465CA1550E5C48D995BD6ED6645839A/fulltext/txt</uri></json:item></fulltext><metadata><istex:metadataXml wicri:clean="Springer, Publisher found" wicri:toSee="no header"><istex:xmlDeclaration>version="1.0" encoding="UTF-8"</istex:xmlDeclaration><istex:docType PUBLIC="-//Springer-Verlag//DTD A++ V2.4//EN" URI="http://devel.springer.de/A++/V2.4/DTD/A++V2.4.dtd" name="istex:docType"></istex:docType><istex:document><Publisher><PublisherInfo><PublisherName>Springer Berlin Heidelberg</PublisherName><PublisherLocation>Berlin, Heidelberg</PublisherLocation></PublisherInfo><Series><SeriesInfo TocLevels="0"><SeriesID>558</SeriesID><SeriesPrintISSN>0302-9743</SeriesPrintISSN><SeriesElectronicISSN>1611-3349</SeriesElectronicISSN><SeriesTitle Language="En">Lecture Notes in Computer Science</SeriesTitle><SeriesAbbreviatedTitle>Lect Notes Comput Sci</SeriesAbbreviatedTitle></SeriesInfo><SeriesHeader><EditorGroup><Editor><EditorName DisplayOrder="Western"><GivenName>Gerhard</GivenName><FamilyName>Goos</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>Juris</GivenName><FamilyName>Hartmanis</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>Jan</GivenName><Particle>van</Particle><FamilyName>Leeuwen</FamilyName></EditorName></Editor></EditorGroup></SeriesHeader><Book Language="En"><BookInfo MediaType="eBook" Language="En" BookProductType="Proceedings" TocLevels="0" NumberingStyle="Unnumbered"><BookID>3540600450</BookID><BookTitle>Computer Aided Verification</BookTitle><BookSubTitle>7th International Conference, CAV '95 Liège, Belgium, July 3–5, 1995 Proceedings</BookSubTitle><BookVolumeNumber>939</BookVolumeNumber><BookDOI>10.1007/3-540-60045-0</BookDOI><BookTitleID>42727</BookTitleID><BookPrintISBN>978-3-540-60045-9</BookPrintISBN><BookElectronicISBN>978-3-540-49413-3</BookElectronicISBN><BookChapterCount>34</BookChapterCount><BookCopyright><CopyrightHolderName>Springer-Verlag</CopyrightHolderName><CopyrightYear>1995</CopyrightYear></BookCopyright><BookSubjectGroup><BookSubject Code="I" Type="Primary">Computer Science</BookSubject><BookSubject Code="I1603X" Priority="1" Type="Secondary">Logics and Meanings of Programs</BookSubject><BookSubject Code="I14029" Priority="2" Type="Secondary">Software Engineering</BookSubject><BookSubject Code="I16048" Priority="3" Type="Secondary">Mathematical Logic and Formal Languages</BookSubject><BookSubject Code="T24027" Priority="4" Type="Secondary">Electronics and Microelectronics, Instrumentation</BookSubject><BookSubject Code="I13030" Priority="5" Type="Secondary">Special Purpose and Application-Based Systems</BookSubject><BookSubject Code="I21017" Priority="6" Type="Secondary">Artificial Intelligence (incl. Robotics)</BookSubject><SubjectCollection Code="SUCO11645">Computer Science</SubjectCollection></BookSubjectGroup></BookInfo><BookHeader><EditorGroup><Editor><EditorName DisplayOrder="Western"><GivenName>Pierre</GivenName><FamilyName>Wolper</FamilyName></EditorName></Editor></EditorGroup></BookHeader><Chapter ID="Chap2" Language="En"><ChapterInfo ChapterType="ReviewPaper" NumberingStyle="Unnumbered" TocLevels="0" ContainsESM="No"><ChapterID>2</ChapterID><ChapterDOI>10.1007/3-540-60045-0_36</ChapterDOI><ChapterSequenceNumber>2</ChapterSequenceNumber><ChapterTitle Language="En">Global rebuilding of OBDDs avoiding memory requirement maxima</ChapterTitle><ChapterCategory>Session 2: Invited Talk</ChapterCategory><ChapterFirstPage>4</ChapterFirstPage><ChapterLastPage>15</ChapterLastPage><ChapterCopyright><CopyrightHolderName>Springer-Verlag</CopyrightHolderName><CopyrightYear>1995</CopyrightYear></ChapterCopyright><ChapterHistory><OnlineDate><Year>2005</Year><Month>5</Month><Day>31</Day></OnlineDate></ChapterHistory><ChapterGrants Type="Regular"><MetadataGrant Grant="OpenAccess"></MetadataGrant><AbstractGrant Grant="OpenAccess"></AbstractGrant><BodyPDFGrant Grant="Restricted"></BodyPDFGrant><BodyHTMLGrant Grant="Restricted"></BodyHTMLGrant><BibliographyGrant Grant="Restricted"></BibliographyGrant><ESMGrant Grant="Restricted"></ESMGrant></ChapterGrants><ChapterContext><SeriesID>558</SeriesID><BookID>3540600450</BookID><BookTitle>Computer Aided Verification</BookTitle></ChapterContext></ChapterInfo><ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff1"><AuthorName DisplayOrder="Western"><GivenName>Jochen</GivenName><FamilyName>Bern</FamilyName></AuthorName></Author><Author AffiliationIDS="Aff1"><AuthorName DisplayOrder="Western"><GivenName>Christoph</GivenName><FamilyName>Meinel</FamilyName></AuthorName></Author><Author AffiliationIDS="Aff1"><AuthorName DisplayOrder="Western"><GivenName>Anna</GivenName><FamilyName>Slobodová</FamilyName></AuthorName></Author><Affiliation ID="Aff1"><OrgName>University of Trier</OrgName><OrgAddress><Postcode>D-54286</Postcode><City>Trier</City><Country>Germany</Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>It is well-known that the size of an ordered binary decision diagram (OBDD) may depend crucially on the order in which the variables occur. In the paper, we describe an implementation of an outputefficient algorithm that transforms an OBDD <Emphasis Type="Italic">P</Emphasis> representing a Boolean function <Emphasis Type="Italic">f</Emphasis> with respect to one variable ordering <Emphasis Type="Italic">π</Emphasis> into an OBDD <Emphasis Type="Italic">Q</Emphasis> that represents <Emphasis Type="Italic">f</Emphasis> with respect to another variable ordering <Emphasis Type="Italic">σ</Emphasis>. The algorithm runs in average time <Emphasis Type="Italic">O(¦P∥Q¦)</Emphasis> and requires <Emphasis Type="Italic">O(¦P¦+n¦Q¦)</Emphasis> space.</Para><Para>The importance of the algorithm is demonstrated by means of experimental results on basically two different applications. In one of them, the algorithm is used merely once. Such transformations are needed to test equivalence or to perform synthesis on OBDDs in which variables appear in different orders. The other application shows a way how to decrease the size of intermediate representations in the course of the construction of OBDDs from a given circuit. Here the algorithm is used dynamically, whenever the size of the manipulated OBDDs becomes too large.</Para></Abstract><ArticleNote Type="Misc"><SimplePara>Granted by DFG Me 1077/2-1</SimplePara></ArticleNote></ChapterHeader><NoBody></NoBody></Chapter></Book></Series></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Global rebuilding of OBDDs avoiding memory requirement maxima</title></titleInfo><titleInfo type="alternative" contentType="CDATA" lang="en"><title>Global rebuilding of OBDDs avoiding memory requirement maxima</title></titleInfo><name type="personal"><namePart type="given">Jochen</namePart><namePart type="family">Bern</namePart><affiliation>University of Trier, D-54286, Trier, Germany</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Christoph</namePart><namePart type="family">Meinel</namePart><affiliation>University of Trier, D-54286, Trier, Germany</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Anna</namePart><namePart type="family">Slobodová</namePart><affiliation>University of Trier, D-54286, Trier, Germany</affiliation><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre type="conference" displayLabel="ReviewPaper"></genre><originInfo><publisher>Springer Berlin Heidelberg</publisher><place><placeTerm type="text">Berlin, Heidelberg</placeTerm></place><dateIssued encoding="w3cdtf">2005-05-31</dateIssued><copyrightDate encoding="w3cdtf">1995</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><physicalDescription><internetMediaType>text/html</internetMediaType></physicalDescription><abstract lang="en">Abstract: It is well-known that the size of an ordered binary decision diagram (OBDD) may depend crucially on the order in which the variables occur. In the paper, we describe an implementation of an outputefficient algorithm that transforms an OBDD P representing a Boolean function f with respect to one variable ordering π into an OBDD Q that represents f with respect to another variable ordering σ. The algorithm runs in average time O(¦P∥Q¦) and requires O(¦P¦+n¦Q¦) space. The importance of the algorithm is demonstrated by means of experimental results on basically two different applications. In one of them, the algorithm is used merely once. Such transformations are needed to test equivalence or to perform synthesis on OBDDs in which variables appear in different orders. The other application shows a way how to decrease the size of intermediate representations in the course of the construction of OBDDs from a given circuit. Here the algorithm is used dynamically, whenever the size of the manipulated OBDDs becomes too large.</abstract><relatedItem type="host"><titleInfo><title>Computer Aided Verification</title><subTitle>7th International Conference, CAV '95 Liège, Belgium, July 3–5, 1995 Proceedings</subTitle></titleInfo><name type="personal"><namePart type="given">Pierre</namePart><namePart type="family">Wolper</namePart><role><roleTerm type="text">editor</roleTerm></role></name><genre type="book-series" displayLabel="Proceedings"></genre><originInfo><copyrightDate encoding="w3cdtf">1995</copyrightDate><issuance>monographic</issuance></originInfo><subject><genre>Book-Subject-Collection</genre><topic authority="SpringerSubjectCodes" authorityURI="SUCO11645">Computer Science</topic></subject><subject><genre>Book-Subject-Group</genre><topic authority="SpringerSubjectCodes" authorityURI="I">Computer Science</topic><topic authority="SpringerSubjectCodes" authorityURI="I1603X">Logics and Meanings of Programs</topic><topic authority="SpringerSubjectCodes" authorityURI="I14029">Software Engineering</topic><topic authority="SpringerSubjectCodes" authorityURI="I16048">Mathematical Logic and Formal Languages</topic><topic authority="SpringerSubjectCodes" authorityURI="T24027">Electronics and Microelectronics, Instrumentation</topic><topic authority="SpringerSubjectCodes" authorityURI="I13030">Special Purpose and Application-Based Systems</topic><topic authority="SpringerSubjectCodes" authorityURI="I21017">Artificial Intelligence (incl. Robotics)</topic></subject><identifier type="DOI">10.1007/3-540-60045-0</identifier><identifier type="ISBN">978-3-540-60045-9</identifier><identifier type="eISBN">978-3-540-49413-3</identifier><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="BookTitleID">42727</identifier><identifier type="BookID">3540600450</identifier><identifier type="BookChapterCount">34</identifier><identifier type="BookVolumeNumber">939</identifier><part><date>1995</date><detail type="volume"><number>939</number><caption>vol.</caption></detail><extent unit="pages"><start>4</start><end>15</end></extent></part><recordInfo><recordOrigin>Springer-Verlag, 1995</recordOrigin></recordInfo></relatedItem><relatedItem type="series"><titleInfo><title>Lecture Notes in Computer Science</title></titleInfo><name type="personal"><namePart type="given">Gerhard</namePart><namePart type="family">Goos</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Juris</namePart><namePart type="family">Hartmanis</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jan</namePart><namePart type="family">van Leeuwen</namePart><role><roleTerm type="text">editor</roleTerm></role></name><originInfo><copyrightDate encoding="w3cdtf">1995</copyrightDate><issuance>serial</issuance></originInfo><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="SeriesID">558</identifier><recordInfo><recordOrigin>Springer-Verlag, 1995</recordOrigin></recordInfo></relatedItem><identifier type="istex">5D5A86C8E465CA1550E5C48D995BD6ED6645839A</identifier><identifier type="DOI">10.1007/3-540-60045-0_36</identifier><identifier type="ChapterID">2</identifier><identifier type="ChapterID">Chap2</identifier><accessCondition type="use and reproduction" contentType="copyright">Springer-Verlag, 1995</accessCondition><recordInfo><recordContentSource>SPRINGER</recordContentSource><recordOrigin>Springer-Verlag, 1995</recordOrigin></recordInfo></mods></metadata></istex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Rhénanie/explor/UnivTrevesV1/Data/Istex/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001234 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 001234 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Rhénanie
|area= UnivTrevesV1
|flux= Istex
|étape= Corpus
|type= RBID
|clé= ISTEX:5D5A86C8E465CA1550E5C48D995BD6ED6645839A
|texte= Global rebuilding of OBDDs avoiding memory requirement maxima
}}
| This area was generated with Dilib version V0.6.31. |  |