Sample Method for Minimization of OBDDs
Identifieur interne : 000F95 ( Istex/Corpus ); précédent : 000F94; suivant : 000F96Sample Method for Minimization of OBDDs
Auteurs : Anna Slobodova ; Christoph MeinelSource :
- Lecture Notes in Computer Science [ 0302-9743 ] ; 1998.
Abstract
Abstract: The exact minimization of the size of Ordered Binary Decision Diagrams (OBDD) is known to be an NP-complete problem. The available heuristical solutions of the problem still do not satisfy requirements of the practical applications. Development of the efficient algorithms that find acceptable variable orders within a short time and with a modest memory overhead is hence higly desired. In this paper we contribute to the solution of the minimization problem by a new variable reordering heuristic that is based on sampling. A small OBDD sample is chosen from the OBDDs that are considered for minimization. Solving the problem for this small sample, we obtain a variable order that is extrapolated and applied to the entire OBDDs. We present the first experimental results with the Sample Reordering targeted at combinatorial verification. The suggested heuristic is substantially faster than Sifting.
Url:
DOI: 10.1007/3-540-49477-4_34
Links to Exploration step
ISTEX:44B0942DEB039718FDCA9D4A16B46A1CA0BB36F8Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Sample Method for Minimization of OBDDs</title><author><name sortKey="Slobodova, Anna" sort="Slobodova, Anna" uniqKey="Slobodova A" first="Anna" last="Slobodova">Anna Slobodova</name><affiliation><mods:affiliation>Compaq, Shrewsbury, Massachusets, USA</mods:affiliation></affiliation><affiliation><mods:affiliation>Comenius University, Bratislava, Slovakia</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: slobodov@cadunx.hlo.dec.com</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>Institute of Telematics, Bahnhofstr 30-32, 54292, Trier, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>FB IV - Informatik, University of Trier, 54286, Trier, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: meinel@ti.fhg.de</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:44B0942DEB039718FDCA9D4A16B46A1CA0BB36F8</idno><date when="1998" year="1998">1998</date><idno type="doi">10.1007/3-540-49477-4_34</idno><idno type="url">https://api.istex.fr/document/44B0942DEB039718FDCA9D4A16B46A1CA0BB36F8/fulltext/pdf</idno><idno type="wicri:Area/Istex/Corpus">000F95</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000F95</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Sample Method for Minimization of OBDDs</title><author><name sortKey="Slobodova, Anna" sort="Slobodova, Anna" uniqKey="Slobodova A" first="Anna" last="Slobodova">Anna Slobodova</name><affiliation><mods:affiliation>Compaq, Shrewsbury, Massachusets, USA</mods:affiliation></affiliation><affiliation><mods:affiliation>Comenius University, Bratislava, Slovakia</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: slobodov@cadunx.hlo.dec.com</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>Institute of Telematics, Bahnhofstr 30-32, 54292, Trier, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>FB IV - Informatik, University of Trier, 54286, Trier, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: meinel@ti.fhg.de</mods:affiliation></affiliation></author></analytic><monogr></monogr><series><title level="s">Lecture Notes in Computer Science</title><imprint><date>1998</date></imprint><idno type="ISSN">0302-9743</idno><idno type="ISSN">0302-9743</idno></series><idno type="istex">44B0942DEB039718FDCA9D4A16B46A1CA0BB36F8</idno><idno type="DOI">10.1007/3-540-49477-4_34</idno><idno type="ChapterID">34</idno><idno type="ChapterID">Chap34</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: The exact minimization of the size of Ordered Binary Decision Diagrams (OBDD) is known to be an NP-complete problem. The available heuristical solutions of the problem still do not satisfy requirements of the practical applications. Development of the efficient algorithms that find acceptable variable orders within a short time and with a modest memory overhead is hence higly desired. In this paper we contribute to the solution of the minimization problem by a new variable reordering heuristic that is based on sampling. A small OBDD sample is chosen from the OBDDs that are considered for minimization. Solving the problem for this small sample, we obtain a variable order that is extrapolated and applied to the entire OBDDs. We present the first experimental results with the Sample Reordering targeted at combinatorial verification. The suggested heuristic is substantially faster than Sifting.</div></front></TEI><istex><corpusName>springer</corpusName><author><json:item><name>Anna Slobodova</name><affiliations><json:string>Compaq, Shrewsbury, Massachusets, USA</json:string><json:string>Comenius University, Bratislava, Slovakia</json:string><json:string>E-mail: slobodov@cadunx.hlo.dec.com</json:string></affiliations></json:item><json:item><name>Christoph Meinel</name><affiliations><json:string>Institute of Telematics, Bahnhofstr 30-32, 54292, Trier, Germany</json:string><json:string>FB IV - Informatik, University of Trier, 54286, Trier, Germany</json:string><json:string>E-mail: meinel@ti.fhg.de</json:string></affiliations></json:item></author><language><json:string>eng</json:string></language><originalGenre><json:string>OriginalPaper</json:string></originalGenre><abstract>Abstract: The exact minimization of the size of Ordered Binary Decision Diagrams (OBDD) is known to be an NP-complete problem. The available heuristical solutions of the problem still do not satisfy requirements of the practical applications. Development of the efficient algorithms that find acceptable variable orders within a short time and with a modest memory overhead is hence higly desired. In this paper we contribute to the solution of the minimization problem by a new variable reordering heuristic that is based on sampling. A small OBDD sample is chosen from the OBDDs that are considered for minimization. Solving the problem for this small sample, we obtain a variable order that is extrapolated and applied to the entire OBDDs. We present the first experimental results with the Sample Reordering targeted at combinatorial verification. The suggested heuristic is substantially faster than Sifting.</abstract><qualityIndicators><score>5.657</score><pdfVersion>1.3</pdfVersion><pdfPageSize>431 x 666 pts</pdfPageSize><refBibsNative>false</refBibsNative><keywordCount>0</keywordCount><abstractCharCount>913</abstractCharCount><pdfWordCount>3977</pdfWordCount><pdfCharCount>22973</pdfCharCount><pdfPageCount>10</pdfPageCount><abstractWordCount>140</abstractWordCount></qualityIndicators><title>Sample Method for Minimization of OBDDs</title><chapterId><json:string>34</json:string><json:string>Chap34</json:string></chapterId><refBibs><json:item><author><json:item><name>B Bollig</name></json:item><json:item><name>M Löbbig</name></json:item><json:item><name>I Wegener</name></json:item></author><host><pages><last>1</last><first>5</first></pages><author></author><title>Proc. IWLS</title><publicationDate>1995</publicationDate></host><title>Simulated Annealing to Improve Variable Orderings for OBDDs</title><publicationDate>1995</publicationDate></json:item><json:item><author><json:item><name>J Bern</name></json:item><json:item><name> Ch</name></json:item><json:item><name>A Meinel</name></json:item><json:item><name> Slobodová</name></json:item></author><host><pages><last>308</last><first>299</first></pages><author></author><title>Proc. CAV, (LNCS 939</title><publicationDate>1995</publicationDate></host><title>Global Rebuilding of OBDDs – Avoiding Memory Requirement Maxima</title><publicationDate>1995</publicationDate></json:item><json:item><author><json:item><name>R,E Bryant</name></json:item></author><host><pages><last>691</last><first>677</first></pages><issue>35</issue><author></author><title>IEEE Transactions on Computers</title><publicationDate>1986</publicationDate></host><title>Graph Based Algorithms for Boolean Function Manipulation</title><publicationDate>1986</publicationDate></json:item><json:item><author><json:item><name>B Bollig</name></json:item><json:item><name>I Wegener</name></json:item></author><host><volume>45</volume><pages><last>1002</last><first>993</first></pages><issue>9</issue><author></author><title>IEEE Transactions on Computers</title><publicationDate>1996</publicationDate></host><title>Improving the Variable Ordering of OBDDs is NP– complete</title><publicationDate>1996</publicationDate></json:item><json:item><author><json:item><name>R Drechsler</name></json:item><json:item><name>B Becker</name></json:item><json:item><name>N Göckel</name></json:item></author><host><pages><last>368</last><first>364</first></pages><author></author><title>IEEE Proc. Computers and Digital Techniques</title><publicationDate>1996</publicationDate></host><title>A Genetic Algorithm for Variable Ordering of OBDDs</title><publicationDate>1996</publicationDate></json:item><json:item><author><json:item><name>R Drechsler</name></json:item><json:item><name>N Drechsler</name></json:item><json:item><name>W Günther</name></json:item></author><host><author></author><title>ACM Proc. Design Automation Conference</title><publicationDate>1998</publicationDate></host><title>Fast Exact Minimization of BDDs</title><publicationDate>1998</publicationDate></json:item><json:item><author><json:item><name>S,J Friedman</name></json:item><json:item><name>K,J Supowit</name></json:item></author><host><pages><last>356</last><first>348</first></pages><author></author><title>IEEE/ACM Proc. DAC</title><publicationDate>1987</publicationDate></host><title>Finding the Optimal Variable Ordering for Binary Decision Diagrams</title><publicationDate>1987</publicationDate></json:item><json:item><author><json:item><name>S,J Friedman</name></json:item><json:item><name>K,J Supowit</name></json:item></author><host><volume>39</volume><pages><last>713</last><first>710</first></pages><issue>5</issue><author></author><title>IEEE Transactions on Computers</title><publicationDate>1990</publicationDate></host><title>Finding the Optimal Variable Ordering for Binary Decision Diagrams</title><publicationDate>1990</publicationDate></json:item><json:item><author><json:item><name>N Ishiura</name></json:item><json:item><name>H Sawada</name></json:item><json:item><name>S Yajima</name></json:item></author><host><pages><last>475</last><first>472</first></pages><author></author><title>Minimization of Binary Decision Diagrams Based on Exchanges of Variables IEEE Proc. of ICCAD</title><publicationDate>1991</publicationDate></host><publicationDate>1991</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á</name></json:item></author><host><pages><last>525</last><first>515</first></pages><author></author><title>Proc. MFCS, (LNCS 841</title><publicationDate>1994</publicationDate></host><title>On the Complexity of Constructing Optimal Ordered Binary Decision Diagrams</title><publicationDate>1994</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á</name></json:item></author><host><pages><last>343</last><first>338</first></pages><author></author><title>IEEE Proc. of ICCD</title><publicationDate>1997</publicationDate></host><title>Speeding up Variable Reordering of OBDDs</title><publicationDate>1997</publicationDate></json:item><json:item><author><json:item><name>S Panda</name></json:item><json:item><name>F Somenzi</name></json:item></author><host><pages><last>77</last><first>74</first></pages><author></author><title>Who are the Variables in Your Neighbourhood. Proc. ACM/IEEE ICCAD</title><publicationDate>1995</publicationDate></host><publicationDate>1995</publicationDate></json:item><json:item><author><json:item><name>S Panda</name></json:item><json:item><name>F Somenzi</name></json:item><json:item><name>B,F Plessier</name></json:item></author><host><pages><last>631</last><first>628</first></pages><author></author><title>Proc. ICCAD</title><publicationDate>1994</publicationDate></host><title>Symmetry Detection and Dynamic Variable Ordering of Decision Diagrams</title><publicationDate>1994</publicationDate></json:item><json:item><author><json:item><name>R </name></json:item></author><host><pages><last>47</last><first>42</first></pages><author></author><title>Proc. ACM/IEEE ICCAD</title><publicationDate>1993</publicationDate></host><title>Dynamic Variable Ordering for Ordered Binary Decision Diagrams</title><publicationDate>1993</publicationDate></json:item><json:item><author><json:item><name>F Somenzi</name></json:item></author><host><author></author><title>Boulder</title><publicationDate>1997</publicationDate></host><title>CUDD: CU Decision Diagram Package. Release 2.1.2</title><publicationDate>1997</publicationDate></json:item><json:item><author><json:item><name>D Sieling</name></json:item><json:item><name>I Wegener</name></json:item></author><host><volume>48</volume><pages><last>144</last><first>139</first></pages><issue>3</issue><author></author><title>Information Processing Letters</title><publicationDate>1993</publicationDate></host><title>Reduction of BDDs in Linear Time</title><publicationDate>1993</publicationDate></json:item><json:item><host><pages><last>256</last><first>245</first></pages><author><json:item><name>P Savick´savick´y</name></json:item><json:item><name>I Wegener</name></json:item></author><title>Efficient Algorithms for the Transformation Between Different Types of Binary Decision Diagrams Acta Informatica</title><publicationDate>1997</publicationDate></host></json:item><json:item><author><json:item><name>S Tani</name></json:item><json:item><name>K Hamaguchi</name></json:item><json:item><name>S Yajima</name></json:item></author><host><pages><last>398</last><first>389</first></pages><author></author><title>Proc. ISAAC, (LNCS 762</title><publicationDate>1993</publicationDate></host><title>The Complexity of the Optimal Variable Ordering Problem of Shared Binary Decision Diagrams</title><publicationDate>1993</publicationDate></json:item></refBibs><genre><json:string>conference</json:string></genre><serie><editor><json:item><name>Gerhard Goos</name><affiliations><json:string>Karlsruhe University, Germany</json:string></affiliations></json:item><json:item><name>Juris Hartmanis</name><affiliations><json:string>Cornell University, NY, USA</json:string></affiliations></json:item><json:item><name>Jan van Leeuwen</name><affiliations><json:string>Utrecht University, The Netherlands</json:string></affiliations></json:item></editor><issn><json:string>0302-9743</json:string></issn><language><json:string>unknown</json:string></language><title>Lecture Notes in Computer Science</title><copyrightDate>1998</copyrightDate></serie><host><editor><json:item><name>Branislav Rovan</name><affiliations><json:string>Department of Computer Science, Comenius University, SK-84215, Bratislava, Slovakia</json:string><json:string>E-mail: rovan@fmph.uniba.sk</json:string></affiliations></json:item></editor><subject><json:item><value>Computer Science</value></json:item><json:item><value>Computer Science</value></json:item><json:item><value>Computer Communication Networks</value></json:item><json:item><value>Software Engineering/Programming and Operating Systems</value></json:item><json:item><value>Theory of Computation</value></json:item><json:item><value>Information Systems and Communication Service</value></json:item></subject><isbn><json:string>978-3-540-65260-1</json:string></isbn><language><json:string>unknown</json:string></language><title>SOFSEM’ 98: Theory and Practice of Informatics</title><bookId><json:string>3-540-49477-4</json:string></bookId><volume>1521</volume><pages><last>428</last><first>419</first></pages><issn><json:string>0302-9743</json:string></issn><genre><json:string>book-series</json:string></genre><eisbn><json:string>978-3-540-49477-5</json:string></eisbn><copyrightDate>1998</copyrightDate><doi><json:string>10.1007/3-540-49477-4</json:string></doi></host><publicationDate>2002</publicationDate><copyrightDate>1998</copyrightDate><doi><json:string>10.1007/3-540-49477-4_34</json:string></doi><id>44B0942DEB039718FDCA9D4A16B46A1CA0BB36F8</id><score>1.0265541</score><fulltext><json:item><extension>pdf</extension><original>true</original><mimetype>application/pdf</mimetype><uri>https://api.istex.fr/document/44B0942DEB039718FDCA9D4A16B46A1CA0BB36F8/fulltext/pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/document/44B0942DEB039718FDCA9D4A16B46A1CA0BB36F8/fulltext/zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/document/44B0942DEB039718FDCA9D4A16B46A1CA0BB36F8/fulltext/tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Sample Method for Minimization of OBDDs</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 Berlin Heidelberg, 1998</p></availability><date>1998</date></publicationStmt><sourceDesc><biblStruct type="inbook"><analytic><title level="a" type="main" xml:lang="en">Sample Method for Minimization of OBDDs</title><author xml:id="author-1"><persName><forename type="first">Anna</forename><surname>Slobodova</surname></persName><email>slobodov@cadunx.hlo.dec.com</email><affiliation>Compaq, Shrewsbury, Massachusets, USA</affiliation><affiliation>Comenius University, Bratislava, Slovakia</affiliation></author><author xml:id="author-2"><persName><forename type="first">Christoph</forename><surname>Meinel</surname></persName><email>meinel@ti.fhg.de</email><affiliation>Institute of Telematics, Bahnhofstr 30-32, 54292, Trier, Germany</affiliation><affiliation>FB IV - Informatik, University of Trier, 54286, Trier, Germany</affiliation></author></analytic><monogr><title level="m">SOFSEM’ 98: Theory and Practice of Informatics</title><title level="m" type="sub">25th Conference on Current Trends in Theory and Practice of Informatics Jasná, Slovakia, November 21–27, 1998 Proceedings</title><idno type="pISBN">978-3-540-65260-1</idno><idno type="eISBN">978-3-540-49477-5</idno><idno type="pISSN">0302-9743</idno><idno type="DOI">10.1007/3-540-49477-4</idno><idno type="book-ID">3-540-49477-4</idno><idno type="book-title-ID">59038</idno><idno type="book-sequence-number">1521</idno><idno type="book-volume-number">1521</idno><idno type="book-chapter-count">37</idno><editor><persName><forename type="first">Branislav</forename><surname>Rovan</surname></persName><email>rovan@fmph.uniba.sk</email><affiliation>Department of Computer Science, Comenius University, SK-84215, Bratislava, Slovakia</affiliation></editor><imprint><publisher>Springer Berlin Heidelberg</publisher><pubPlace>Berlin, Heidelberg</pubPlace><date type="published" when="2002-09-24"></date><biblScope unit="volume">1521</biblScope><biblScope unit="page" from="419">419</biblScope><biblScope unit="page" to="428">428</biblScope></imprint></monogr><series><title level="s">Lecture Notes in Computer Science</title><editor><persName><forename type="first">Gerhard</forename><surname>Goos</surname></persName><affiliation>Karlsruhe University, Germany</affiliation></editor><editor><persName><forename type="first">Juris</forename><surname>Hartmanis</surname></persName><affiliation>Cornell University, NY, USA</affiliation></editor><editor><persName><forename type="first">Jan</forename><surname>van Leeuwen</surname></persName><affiliation>Utrecht University, The Netherlands</affiliation></editor><biblScope><date>1998</date></biblScope><idno type="pISSN">0302-9743</idno><idno type="series-Id">558</idno></series><idno type="istex">44B0942DEB039718FDCA9D4A16B46A1CA0BB36F8</idno><idno type="DOI">10.1007/3-540-49477-4_34</idno><idno type="ChapterID">34</idno><idno type="ChapterID">Chap34</idno></biblStruct></sourceDesc></fileDesc><profileDesc><creation><date>1998</date></creation><langUsage><language ident="en">en</language></langUsage><abstract xml:lang="en"><p>Abstract: The exact minimization of the size of Ordered Binary Decision Diagrams (OBDD) is known to be an NP-complete problem. The available heuristical solutions of the problem still do not satisfy requirements of the practical applications. Development of the efficient algorithms that find acceptable variable orders within a short time and with a modest memory overhead is hence higly desired. In this paper we contribute to the solution of the minimization problem by a new variable reordering heuristic that is based on sampling. A small OBDD sample is chosen from the OBDDs that are considered for minimization. Solving the problem for this small sample, we obtain a variable order that is extrapolated and applied to the entire OBDDs. We present the first experimental results with the Sample Reordering targeted at combinatorial verification. The suggested heuristic is substantially faster than Sifting.</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>I13022</label><label>I14002</label><label>I16005</label><label>I18008</label><item><term>Computer Science</term></item><item><term>Computer Communication Networks</term></item><item><term>Software Engineering/Programming and Operating Systems</term></item><item><term>Theory of Computation</term></item><item><term>Information Systems and Communication Service</term></item></list></keywords></textClass></profileDesc><revisionDesc><change when="2002-09-24">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-21">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/44B0942DEB039718FDCA9D4A16B46A1CA0BB36F8/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 SeriesType="Series" TocLevels="0"><SeriesID>558</SeriesID><SeriesPrintISSN>0302-9743</SeriesPrintISSN><SeriesTitle Language="En">Lecture Notes in Computer Science</SeriesTitle></SeriesInfo><SeriesHeader><EditorGroup><Editor AffiliationIDS="Aff1"><EditorName DisplayOrder="Western"><GivenName>Gerhard</GivenName><FamilyName>Goos</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff2"><EditorName DisplayOrder="Western"><GivenName>Juris</GivenName><FamilyName>Hartmanis</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff3"><EditorName DisplayOrder="Western"><GivenName>Jan</GivenName><Particle>van</Particle><FamilyName>Leeuwen</FamilyName></EditorName></Editor><Affiliation ID="Aff1"><OrgName>Karlsruhe University</OrgName><OrgAddress><Country>Germany</Country></OrgAddress></Affiliation><Affiliation ID="Aff2"><OrgName>Cornell University</OrgName><OrgAddress><City>NY</City><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff3"><OrgName>Utrecht University</OrgName><OrgAddress><Country>The Netherlands</Country></OrgAddress></Affiliation></EditorGroup></SeriesHeader><Book Language="En"><BookInfo BookProductType="Proceedings" ContainsESM="No" Language="En" MediaType="eBook" NumberingStyle="Unnumbered" TocLevels="0"><BookID>3-540-49477-4</BookID><BookTitle>SOFSEM’ 98: Theory and Practice of Informatics</BookTitle><BookSubTitle>25th Conference on Current Trends in Theory and Practice of Informatics Jasná, Slovakia, November 21–27, 1998 Proceedings</BookSubTitle><BookVolumeNumber>1521</BookVolumeNumber><BookSequenceNumber>1521</BookSequenceNumber><BookDOI>10.1007/3-540-49477-4</BookDOI><BookTitleID>59038</BookTitleID><BookPrintISBN>978-3-540-65260-1</BookPrintISBN><BookElectronicISBN>978-3-540-49477-5</BookElectronicISBN><BookChapterCount>37</BookChapterCount><BookHistory><OnlineDate><Year>2002</Year><Month>9</Month><Day>24</Day></OnlineDate></BookHistory><BookCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>1998</CopyrightYear></BookCopyright><BookSubjectGroup><BookSubject Code="I" Type="Primary">Computer Science</BookSubject><BookSubject Code="I13022" Priority="1" Type="Secondary">Computer Communication Networks</BookSubject><BookSubject Code="I14002" Priority="2" Type="Secondary">Software Engineering/Programming and Operating Systems</BookSubject><BookSubject Code="I16005" Priority="3" Type="Secondary">Theory of Computation</BookSubject><BookSubject Code="I18008" Priority="4" Type="Secondary">Information Systems and Communication Service</BookSubject><SubjectCollection Code="SUCO11645">Computer Science</SubjectCollection></BookSubjectGroup><BookContext><SeriesID>558</SeriesID></BookContext></BookInfo><BookHeader><EditorGroup><Editor AffiliationIDS="Aff4"><EditorName DisplayOrder="Western"><GivenName>Branislav</GivenName><FamilyName>Rovan</FamilyName></EditorName><Contact><Email>rovan@fmph.uniba.sk</Email></Contact></Editor><Affiliation ID="Aff4"><OrgDivision>Department of Computer Science</OrgDivision><OrgName>Comenius University</OrgName><OrgAddress><Postcode>SK-84215</Postcode><City>Bratislava</City><Country>Slovakia</Country></OrgAddress></Affiliation></EditorGroup></BookHeader><Part ID="Part2"><PartInfo TocLevels="0"><PartID>2</PartID><PartSequenceNumber>2</PartSequenceNumber><PartTitle>Contributed Papers</PartTitle><PartChapterCount>18</PartChapterCount><PartContext><SeriesID>558</SeriesID><BookID>3-540-49477-4</BookID><BookTitle>SOFSEM’ 98: Theory and Practice of Informatics</BookTitle></PartContext></PartInfo><Chapter ID="Chap34" Language="En"><ChapterInfo ChapterType="OriginalPaper" ContainsESM="No" Language="En" NumberingStyle="Unnumbered" TocLevels="0"><ChapterID>34</ChapterID><ChapterDOI>10.1007/3-540-49477-4_34</ChapterDOI><ChapterSequenceNumber>34</ChapterSequenceNumber><ChapterTitle Language="En">Sample Method for Minimization of OBDDs</ChapterTitle><ChapterFirstPage>419</ChapterFirstPage><ChapterLastPage>428</ChapterLastPage><ChapterCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>1998</CopyrightYear></ChapterCopyright><ChapterHistory><RegistrationDate><Year>2002</Year><Month>9</Month><Day>23</Day></RegistrationDate><OnlineDate><Year>2002</Year><Month>9</Month><Day>24</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><PartID>2</PartID><BookID>3-540-49477-4</BookID><BookTitle>SOFSEM’ 98: Theory and Practice of Informatics</BookTitle></ChapterContext></ChapterInfo><ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff5 Aff6"><AuthorName DisplayOrder="Western"><GivenName>Anna</GivenName><FamilyName>Slobodova</FamilyName></AuthorName><Contact><Email>slobodov@cadunx.hlo.dec.com</Email></Contact></Author><Author AffiliationIDS="Aff7 Aff8"><AuthorName DisplayOrder="Western"><GivenName>Christoph</GivenName><FamilyName>Meinel</FamilyName></AuthorName><Contact><Email>meinel@ti.fhg.de</Email></Contact></Author><Affiliation ID="Aff5"><OrgName>Compaq, Shrewsbury</OrgName><OrgAddress><City>Massachusets</City><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff6"><OrgName>Comenius University</OrgName><OrgAddress><City>Bratislava</City><Country>Slovakia</Country></OrgAddress></Affiliation><Affiliation ID="Aff7"><OrgName>Institute of Telematics</OrgName><OrgAddress><Street>Bahnhofstr 30-32</Street><Postcode>54292</Postcode><City>Trier</City><Country>Germany</Country></OrgAddress></Affiliation><Affiliation ID="Aff8"><OrgDivision>FB IV - Informatik</OrgDivision><OrgName>University of Trier</OrgName><OrgAddress><Postcode>54286</Postcode><City>Trier</City><Country>Germany</Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>The exact minimization of the size of Ordered Binary Decision Diagrams (OBDD) is known to be an NP-complete problem. The available heuristical solutions of the problem still do not satisfy requirements of the practical applications. Development of the efficient algorithms that find acceptable variable orders within a short time and with a modest memory overhead is hence higly desired.</Para><Para>In this paper we contribute to the solution of the minimization problem by a new variable reordering heuristic that is based on sampling. A small OBDD sample is chosen from the OBDDs that are considered for minimization. Solving the problem for this small sample, we obtain a variable order that is extrapolated and applied to the entire OBDDs. We present the first experimental results with the Sample Reordering targeted at combinatorial verification. The suggested heuristic is substantially faster than Sifting.</Para></Abstract></ChapterHeader><NoBody></NoBody></Chapter></Part></Book></Series></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Sample Method for Minimization of OBDDs</title></titleInfo><titleInfo type="alternative" contentType="CDATA" lang="en"><title>Sample Method for Minimization of OBDDs</title></titleInfo><name type="personal"><namePart type="given">Anna</namePart><namePart type="family">Slobodova</namePart><affiliation>Compaq, Shrewsbury, Massachusets, USA</affiliation><affiliation>Comenius University, Bratislava, Slovakia</affiliation><affiliation>E-mail: slobodov@cadunx.hlo.dec.com</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Christoph</namePart><namePart type="family">Meinel</namePart><affiliation>Institute of Telematics, Bahnhofstr 30-32, 54292, Trier, Germany</affiliation><affiliation>FB IV - Informatik, University of Trier, 54286, Trier, Germany</affiliation><affiliation>E-mail: meinel@ti.fhg.de</affiliation><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre type="conference" displayLabel="OriginalPaper"></genre><originInfo><publisher>Springer Berlin Heidelberg</publisher><place><placeTerm type="text">Berlin, Heidelberg</placeTerm></place><dateIssued encoding="w3cdtf">2002-09-24</dateIssued><copyrightDate encoding="w3cdtf">1998</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: The exact minimization of the size of Ordered Binary Decision Diagrams (OBDD) is known to be an NP-complete problem. The available heuristical solutions of the problem still do not satisfy requirements of the practical applications. Development of the efficient algorithms that find acceptable variable orders within a short time and with a modest memory overhead is hence higly desired. In this paper we contribute to the solution of the minimization problem by a new variable reordering heuristic that is based on sampling. A small OBDD sample is chosen from the OBDDs that are considered for minimization. Solving the problem for this small sample, we obtain a variable order that is extrapolated and applied to the entire OBDDs. We present the first experimental results with the Sample Reordering targeted at combinatorial verification. The suggested heuristic is substantially faster than Sifting.</abstract><relatedItem type="host"><titleInfo><title>SOFSEM’ 98: Theory and Practice of Informatics</title><subTitle>25th Conference on Current Trends in Theory and Practice of Informatics Jasná, Slovakia, November 21–27, 1998 Proceedings</subTitle></titleInfo><name type="personal"><namePart type="given">Branislav</namePart><namePart type="family">Rovan</namePart><affiliation>Department of Computer Science, Comenius University, SK-84215, Bratislava, Slovakia</affiliation><affiliation>E-mail: rovan@fmph.uniba.sk</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><genre type="book-series" displayLabel="Proceedings"></genre><originInfo><copyrightDate encoding="w3cdtf">1998</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="I13022">Computer Communication Networks</topic><topic authority="SpringerSubjectCodes" authorityURI="I14002">Software Engineering/Programming and Operating Systems</topic><topic authority="SpringerSubjectCodes" authorityURI="I16005">Theory of Computation</topic><topic authority="SpringerSubjectCodes" authorityURI="I18008">Information Systems and Communication Service</topic></subject><identifier type="DOI">10.1007/3-540-49477-4</identifier><identifier type="ISBN">978-3-540-65260-1</identifier><identifier type="eISBN">978-3-540-49477-5</identifier><identifier type="ISSN">0302-9743</identifier><identifier type="BookTitleID">59038</identifier><identifier type="BookID">3-540-49477-4</identifier><identifier type="BookChapterCount">37</identifier><identifier type="BookVolumeNumber">1521</identifier><identifier type="BookSequenceNumber">1521</identifier><identifier type="PartChapterCount">18</identifier><part><date>1998</date><detail type="part"><title>Contributed Papers</title></detail><detail type="volume"><number>1521</number><caption>vol.</caption></detail><extent unit="pages"><start>419</start><end>428</end></extent></part><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 1998</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><affiliation>Karlsruhe University, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Juris</namePart><namePart type="family">Hartmanis</namePart><affiliation>Cornell University, NY, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jan</namePart><namePart type="family">van Leeuwen</namePart><affiliation>Utrecht University, The Netherlands</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><originInfo><copyrightDate encoding="w3cdtf">1998</copyrightDate><issuance>serial</issuance></originInfo><identifier type="ISSN">0302-9743</identifier><identifier type="SeriesID">558</identifier><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 1998</recordOrigin></recordInfo></relatedItem><identifier type="istex">44B0942DEB039718FDCA9D4A16B46A1CA0BB36F8</identifier><identifier type="DOI">10.1007/3-540-49477-4_34</identifier><identifier type="ChapterID">34</identifier><identifier type="ChapterID">Chap34</identifier><accessCondition type="use and reproduction" contentType="copyright">Springer-Verlag Berlin Heidelberg, 1998</accessCondition><recordInfo><recordContentSource>SPRINGER</recordContentSource><recordOrigin>Springer-Verlag Berlin Heidelberg, 1998</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 000F95 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 000F95 | 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:44B0942DEB039718FDCA9D4A16B46A1CA0BB36F8
|texte= Sample Method for Minimization of OBDDs
}}
| This area was generated with Dilib version V0.6.31. |  |