Embedding Memoization to the Semantic Tree Search for Deciding QBFs
Identifieur interne : 001570 ( Istex/Corpus ); précédent : 001569; suivant : 001571Embedding Memoization to the Semantic Tree Search for Deciding QBFs
Auteurs : Mohammad Ghasemzadeh ; Volker Klotz ; Christoph MeinelSource :
- Lecture Notes in Computer Science [ 0302-9743 ] ; 2005.
Abstract
Abstract: Quantified Boolean formulas (QBFs) play an important role in artificial intelligence subjects, specially in planning, knowledge representation and reasoning [20]. In this paper we present ZQSAT (sibling of our FZQSAT [15]), which is an algorithm for evaluating quantified Boolean formulas. QBF is a language that extends propositional logic in such a way that many advanced forms of reasoning can be easily formulated and evaluated. ZQSAT is based on ZDD, which is a variant of BDD, and an adopted version of the DPLL algorithm. The program has been implemented in C using the CUDD package. The capability of ZDDs in storing sets of subsets efficiently enabled us to store the clauses of a QBF very compactly and led us to implement the search algorithm in such a way that we could store and reuse the results of all previously solved subformulas with few overheads. This idea along some other techniques, enabled ZQSAT to solve some standard QBF benchmark problems faster than the best existing QSAT solvers.
Url:
DOI: 10.1007/978-3-540-30549-1_59
Links to Exploration step
ISTEX:E74E21DECC13ED4A2B10E61449622E0F569337BCLe document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct:series"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Embedding Memoization to the Semantic Tree Search for Deciding QBFs</title><author><name sortKey="Ghasemzadeh, Mohammad" sort="Ghasemzadeh, Mohammad" uniqKey="Ghasemzadeh M" first="Mohammad" last="Ghasemzadeh">Mohammad Ghasemzadeh</name><affiliation><mods:affiliation>FB-IV Informatik, University of Trier, D-54286, Trier, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: GhasemZadeh@TI.Uni-Trier.DE</mods:affiliation></affiliation></author><author><name sortKey="Klotz, Volker" sort="Klotz, Volker" uniqKey="Klotz V" first="Volker" last="Klotz">Volker Klotz</name><affiliation><mods:affiliation>FB-IV Informatik, University of Trier, D-54286, Trier, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: klotz@TI.Uni-Trier.DE</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>FB-IV Informatik, University of Trier, D-54286, Trier, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: meinel@TI.Uni-Trier.DE</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:E74E21DECC13ED4A2B10E61449622E0F569337BC</idno><date when="2004" year="2004">2004</date><idno type="doi">10.1007/978-3-540-30549-1_59</idno><idno type="url">https://api.istex.fr/document/E74E21DECC13ED4A2B10E61449622E0F569337BC/fulltext/pdf</idno><idno type="wicri:Area/Istex/Corpus">001570</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001570</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Embedding Memoization to the Semantic Tree Search for Deciding QBFs</title><author><name sortKey="Ghasemzadeh, Mohammad" sort="Ghasemzadeh, Mohammad" uniqKey="Ghasemzadeh M" first="Mohammad" last="Ghasemzadeh">Mohammad Ghasemzadeh</name><affiliation><mods:affiliation>FB-IV Informatik, University of Trier, D-54286, Trier, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: GhasemZadeh@TI.Uni-Trier.DE</mods:affiliation></affiliation></author><author><name sortKey="Klotz, Volker" sort="Klotz, Volker" uniqKey="Klotz V" first="Volker" last="Klotz">Volker Klotz</name><affiliation><mods:affiliation>FB-IV Informatik, University of Trier, D-54286, Trier, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: klotz@TI.Uni-Trier.DE</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>FB-IV Informatik, University of Trier, D-54286, Trier, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: meinel@TI.Uni-Trier.DE</mods:affiliation></affiliation></author></analytic><monogr></monogr><series><title level="s">Lecture Notes in Computer Science</title><imprint><date>2005</date></imprint><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series><idno type="istex">E74E21DECC13ED4A2B10E61449622E0F569337BC</idno><idno type="DOI">10.1007/978-3-540-30549-1_59</idno><idno type="ChapterID">59</idno><idno type="ChapterID">Chap59</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: Quantified Boolean formulas (QBFs) play an important role in artificial intelligence subjects, specially in planning, knowledge representation and reasoning [20]. In this paper we present ZQSAT (sibling of our FZQSAT [15]), which is an algorithm for evaluating quantified Boolean formulas. QBF is a language that extends propositional logic in such a way that many advanced forms of reasoning can be easily formulated and evaluated. ZQSAT is based on ZDD, which is a variant of BDD, and an adopted version of the DPLL algorithm. The program has been implemented in C using the CUDD package. The capability of ZDDs in storing sets of subsets efficiently enabled us to store the clauses of a QBF very compactly and led us to implement the search algorithm in such a way that we could store and reuse the results of all previously solved subformulas with few overheads. This idea along some other techniques, enabled ZQSAT to solve some standard QBF benchmark problems faster than the best existing QSAT solvers.</div></front></TEI><istex><corpusName>springer</corpusName><author><json:item><name>Mohammad GhasemZadeh</name><affiliations><json:string>FB-IV Informatik, University of Trier, D-54286, Trier, Germany</json:string><json:string>E-mail: GhasemZadeh@TI.Uni-Trier.DE</json:string></affiliations></json:item><json:item><name>Volker Klotz</name><affiliations><json:string>FB-IV Informatik, University of Trier, D-54286, Trier, Germany</json:string><json:string>E-mail: klotz@TI.Uni-Trier.DE</json:string></affiliations></json:item><json:item><name>Christoph Meinel</name><affiliations><json:string>FB-IV Informatik, University of Trier, D-54286, Trier, Germany</json:string><json:string>E-mail: meinel@TI.Uni-Trier.DE</json:string></affiliations></json:item></author><language><json:string>eng</json:string></language><originalGenre><json:string>proceedings</json:string></originalGenre><abstract>Abstract: Quantified Boolean formulas (QBFs) play an important role in artificial intelligence subjects, specially in planning, knowledge representation and reasoning [20]. In this paper we present ZQSAT (sibling of our FZQSAT [15]), which is an algorithm for evaluating quantified Boolean formulas. QBF is a language that extends propositional logic in such a way that many advanced forms of reasoning can be easily formulated and evaluated. ZQSAT is based on ZDD, which is a variant of BDD, and an adopted version of the DPLL algorithm. The program has been implemented in C using the CUDD package. The capability of ZDDs in storing sets of subsets efficiently enabled us to store the clauses of a QBF very compactly and led us to implement the search algorithm in such a way that we could store and reuse the results of all previously solved subformulas with few overheads. This idea along some other techniques, enabled ZQSAT to solve some standard QBF benchmark problems faster than the best existing QSAT solvers.</abstract><qualityIndicators><score>6.968</score><pdfVersion>1.3</pdfVersion><pdfPageSize>430 x 660 pts</pdfPageSize><refBibsNative>false</refBibsNative><keywordCount>0</keywordCount><abstractCharCount>1019</abstractCharCount><pdfWordCount>5055</pdfWordCount><pdfCharCount>29187</pdfCharCount><pdfPageCount>13</pdfPageCount><abstractWordCount>164</abstractWordCount></qualityIndicators><title>Embedding Memoization to the Semantic Tree Search for Deciding QBFs</title><chapterId><json:string>59</json:string><json:string>Chap59</json:string></chapterId><refBibs><json:item><host><author><json:item><name>Olaf Achröer</name></json:item><json:item><name>Ingo Wegener</name></json:item></author><title>The Theory of Zero-Suppressed BDDs and the Number of Knight's Tours. Formal Methods in System Design</title><publicationDate>1998-11</publicationDate></host></json:item><json:item><author><json:item><name>Fadi,A Aloul</name></json:item><json:item><name>N Maher</name></json:item><json:item><name>Karem,A Mneimneh</name></json:item><json:item><name> Sakallah</name></json:item></author><host><pages><last>136</last><first>131</first></pages><author></author><title>International Workshop on Logic and Synthesis (IWLS)</title><publicationDate>2002</publicationDate></host><title>ZBDD-Based Backtrack Search SAT Solver</title><publicationDate>2002</publicationDate></json:item><json:item><author><json:item><name>Jochen Bern</name></json:item><json:item><name>Christoph Meinel</name></json:item><json:item><name>Anna Slobodová</name></json:item></author><host><pages><last>413</last><first>408</first></pages><author></author><title>Proceedings 32nd ACM/IEEE Design Automation Conference</title><publicationDate>1995</publicationDate></host><title>OBDD-Based Boolean manipulation in CAD beyound current limits</title><publicationDate>1995</publicationDate></json:item><json:item><author><json:item><name>Randal,E Bryant</name></json:item></author><host><volume>35</volume><pages><last>691</last><first>677</first></pages><author></author><title>IEEE Transactions on Computers, C</title><publicationDate>1986</publicationDate></host><title>Graph-based algorithms for Boolean function manipulation</title><publicationDate>1986</publicationDate></json:item><json:item><host><author><json:item><name>Randal,E Bryant</name></json:item><json:item><name>Christoph Meinel</name></json:item></author><title>Ordererd Binary Decision Diagrams in Electronic Design Automation, chapter 11</title><publicationDate>2002</publicationDate></host></json:item><json:item><author><json:item><name>Marco Cadoli</name></json:item><json:item><name>Marco Schaerf</name></json:item><json:item><name>Andrea Giovanardi</name></json:item><json:item><name>Massimo Giovanardi</name></json:item></author><host><volume>28</volume><pages><last>142</last><first>101</first></pages><issue>2</issue><author></author><title>Journal of Automated Reasoning</title><publicationDate>2002</publicationDate></host><title>An Algorithm to Evaluate Quantified Boolean Formulae and Its Experimental Evaluation</title><publicationDate>2002</publicationDate></json:item><json:item><author><json:item><name>Philippe Chatalic</name></json:item><json:item><name>Laurent Simon</name></json:item></author><host><author></author><title>Proceedings of the 12th IEEE International Conference on Tools with Artificial Intelligence (ICTAI'00)</title><publicationDate>2000</publicationDate></host><title>Multi-Resolution on Compressed Sets of Cluases</title><publicationDate>2000</publicationDate></json:item><json:item><author><json:item><name>M Davis</name></json:item><json:item><name>G Logemann</name></json:item><json:item><name>D Loveland</name></json:item></author><host><volume>5</volume><pages><last>397</last><first>394</first></pages><author></author><title>Communication of the ACM</title><publicationDate>1962</publicationDate></host><title>A machine program for theorem proving</title><publicationDate>1962</publicationDate></json:item><json:item><author><json:item><name>A Karem</name></json:item><json:item><name>A Sakallah Fadi</name></json:item><json:item><name> Aloul</name></json:item><json:item><name>N Maher</name></json:item><json:item><name> Mneimneh</name></json:item></author><host><pages><first>5</first></pages><author></author><title>International Workshop on Logic and Synthesis (IWLS)</title><publicationDate>2001-06</publicationDate></host><title>Backtrack Search Using ZBDDs</title><publicationDate>2001-06</publicationDate></json:item><json:item><author><json:item><name>Rainer Feldmann</name></json:item><json:item><name>Burkhard Monien</name></json:item><json:item><name>Stefan Schamberger</name></json:item></author><host><author></author><title>Proceedings of the 17th National Conference on Artificial Intelligence</title><publicationDate>2000</publicationDate></host><title>A Distributed Algorithm to Evaluate Quantified Boolean Formulae</title><publicationDate>2000</publicationDate></json:item><json:item><author><json:item><name>Enrico Giunchiglia</name></json:item><json:item><name>Massimo Narizzano</name></json:item><json:item><name>Armando Tacchella</name></json:item></author><host><pages><last>369</last><first>364</first></pages><author></author><title>Proceedings of the International Joint Conference on Automated Reasoning</title><publicationDate>2001</publicationDate></host><title>QUBE: A System for Deciding Quantified Boolean Formulas Satisfiability</title><publicationDate>2001</publicationDate></json:item><json:item><host><author><json:item><name>Reinhold Letz</name></json:item></author><title>Efficient Decision Procedures for Quantified Boolean Formulas</title><publicationDate>2003</publicationDate></host></json:item><json:item><author><json:item><name>Reinhold Letz</name></json:item></author><host><pages><last>175</last><first>160</first></pages><author></author><title>Proceedings of TABLEAUX 2002</title><publicationDate>2002</publicationDate></host><title>Lemma and Model Caching in Decision Procedures for Quantified Boolean Formulas</title><publicationDate>2002</publicationDate></json:item><json:item><author><json:item><name>C,M Meinel</name></json:item><json:item><name>V Ghasemzadeh</name></json:item><json:item><name> Klotz</name></json:item></author><host><pages><last>142</last><first>135</first></pages><author></author><title>International Workshop on Logic and Synthesis (IWLS)</title><publicationDate>2004-06</publicationDate></host><title>FZQSAT: A QSAT Solver for QBFs in Prenex NNF (A Useful Tool for Circuit Verification)</title><publicationDate>2004-06</publicationDate></json:item><json:item><host><author><json:item><name>Christoph Meinel</name></json:item><json:item><name>Thorsten Theobald</name></json:item></author><title>Algorithms and Data Structures in VLSI Design</title><publicationDate>1998</publicationDate></host></json:item><json:item><author><json:item><name>S Minato</name></json:item></author><host><author></author><title>proceedings of the 30th ACM/IEEE Design Automation Conference</title><publicationDate>1993</publicationDate></host><title>Zero-suppressed BDDs for set Manipulation in Combinatorial Problems</title><publicationDate>1993</publicationDate></json:item><json:item><host><author><json:item><name>Alan Mishchenko</name></json:item></author><title>An Introduction to Zero-Suppressed Binary Decision Diagrams</title><publicationDate>2001-06</publicationDate></host></json:item><json:item><author><json:item><name>Jussi Rintanen</name></json:item></author><host><pages><last>1197</last><first>1192</first></pages><author></author><title>Proceedings of the 16th International Joint Conference on Artificial Intelligence (IJCAI-99)</title><publicationDate>1999</publicationDate></host><title>Improvements to the Evaluation of Quantified Boolean Formulae</title><publicationDate>1999</publicationDate></json:item><json:item><author><json:item><name>Ingo Wegener</name></json:item></author><host><author></author><title>SIAM Monographs on Discrete Mathematics and Applications</title><publicationDate>2000</publicationDate></host><title>Branching Programs and Binary Decision Diagrams – Theory and Applications</title><publicationDate>2000</publicationDate></json:item></refBibs><genre><json:string>conference</json:string></genre><serie><editor><json:item><name>David Hutchison</name><affiliations><json:string>Lancaster University, UK</json:string></affiliations></json:item><json:item><name>Takeo Kanade</name><affiliations><json:string>Carnegie Mellon University, Pittsburgh, PA, USA</json:string></affiliations></json:item><json:item><name>Josef Kittler</name><affiliations><json:string>University of Surrey, Guildford, UK</json:string></affiliations></json:item><json:item><name>Jon M. Kleinberg</name><affiliations><json:string>Cornell University, Ithaca, NY, USA</json:string></affiliations></json:item><json:item><name>Friedemann Mattern</name><affiliations><json:string>ETH Zurich, Switzerland</json:string></affiliations></json:item><json:item><name>John C. Mitchell</name><affiliations><json:string>Stanford University, CA, USA</json:string></affiliations></json:item><json:item><name>Moni Naor</name><affiliations><json:string>Weizmann Institute of Science, Rehovot, Israel</json:string></affiliations></json:item><json:item><name>Oscar Nierstrasz</name><affiliations><json:string>University of Bern, Switzerland</json:string></affiliations></json:item><json:item><name>C. Pandu Rangan</name><affiliations><json:string>Indian Institute of Technology, Madras, India</json:string></affiliations></json:item><json:item><name>Bernhard Steffen</name><affiliations><json:string>University of Dortmund, Germany</json:string></affiliations></json:item><json:item><name>Madhu Sudan</name><affiliations><json:string>Massachusetts Institute of Technology, MA, USA</json:string></affiliations></json:item><json:item><name>Demetri Terzopoulos</name><affiliations><json:string>New York University, NY, USA</json:string></affiliations></json:item><json:item><name>Dough Tygar</name><affiliations><json:string>University of California, Berkeley, CA, USA</json:string></affiliations></json:item><json:item><name>Moshe Y. Vardi</name><affiliations><json:string>Rice University, Houston, TX, USA</json:string></affiliations></json:item><json:item><name>Gerhard Weikum</name><affiliations><json:string>Max-Planck Institute of Computer Science, Saarbruecken, Germany</json:string></affiliations></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>2005</copyrightDate></serie><host><editor><json:item><name>Geoffrey I. Webb</name><affiliations><json:string>Faculty of Information Technology, Monash University, VIC 3800, Australia</json:string><json:string>E-mail: Geoff.Webb@infotech.monash.edu.au</json:string></affiliations></json:item><json:item><name>Xinghuo Yu</name><affiliations><json:string>Science, Engineering and Technology Portfolio, Royal Melbourne Institute of Technology, VIC 3001, Melbourne, Australia</json:string><json:string>E-mail: x.yu@rmit.edu.au</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>Artificial Intelligence (incl. Robotics)</value></json:item><json:item><value>Mathematical Logic and Formal Languages</value></json:item><json:item><value>Information Storage and Retrieval</value></json:item><json:item><value>Information Systems Applications (incl.Internet)</value></json:item><json:item><value>Database Management</value></json:item><json:item><value>Computation by Abstract Devices</value></json:item></subject><isbn><json:string>978-3-540-24059-4</json:string></isbn><language><json:string>unknown</json:string></language><eissn><json:string>1611-3349</json:string></eissn><title>AI 2004: Advances in Artificial Intelligence</title><bookId><json:string>978-3-540-30549-1</json:string></bookId><volume>3339</volume><pages><last>693</last><first>681</first></pages><issn><json:string>0302-9743</json:string></issn><genre><json:string>book-series</json:string></genre><eisbn><json:string>978-3-540-30549-1</json:string></eisbn><copyrightDate>2005</copyrightDate><doi><json:string>10.1007/b104336</json:string></doi></host><publicationDate>2004</publicationDate><copyrightDate>2004</copyrightDate><doi><json:string>10.1007/978-3-540-30549-1_59</json:string></doi><id>E74E21DECC13ED4A2B10E61449622E0F569337BC</id><score>1.187649</score><fulltext><json:item><extension>pdf</extension><original>true</original><mimetype>application/pdf</mimetype><uri>https://api.istex.fr/document/E74E21DECC13ED4A2B10E61449622E0F569337BC/fulltext/pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/document/E74E21DECC13ED4A2B10E61449622E0F569337BC/fulltext/zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/document/E74E21DECC13ED4A2B10E61449622E0F569337BC/fulltext/tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Embedding Memoization to the Semantic Tree Search for Deciding QBFs</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, 2004</p></availability><date>2004</date></publicationStmt><sourceDesc><biblStruct type="inbook"><analytic><title level="a" type="main" xml:lang="en">Embedding Memoization to the Semantic Tree Search for Deciding QBFs</title><author xml:id="author-1"><persName><forename type="first">Mohammad</forename><surname>GhasemZadeh</surname></persName><email>GhasemZadeh@TI.Uni-Trier.DE</email><affiliation>FB-IV Informatik, University of Trier, D-54286, Trier, Germany</affiliation></author><author xml:id="author-2"><persName><forename type="first">Volker</forename><surname>Klotz</surname></persName><email>klotz@TI.Uni-Trier.DE</email><affiliation>FB-IV Informatik, University of Trier, D-54286, Trier, Germany</affiliation></author><author xml:id="author-3"><persName><forename type="first">Christoph</forename><surname>Meinel</surname></persName><email>meinel@TI.Uni-Trier.DE</email><affiliation>FB-IV Informatik, University of Trier, D-54286, Trier, Germany</affiliation></author></analytic><monogr><title level="m">AI 2004: Advances in Artificial Intelligence</title><title level="m" type="sub">17th Australian Joint Conference on Artificial Intelligence, Cairns, Australia, December 4-6, 2004. Proceedings</title><idno type="pISBN">978-3-540-24059-4</idno><idno type="eISBN">978-3-540-30549-1</idno><idno type="pISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="DOI">10.1007/b104336</idno><idno type="book-ID">978-3-540-30549-1</idno><idno type="book-title-ID">115428</idno><idno type="book-sequence-number">3339</idno><idno type="book-volume-number">3339</idno><idno type="book-chapter-count">132</idno><editor><persName><forename type="first">Geoffrey</forename><forename type="first">I.</forename><surname>Webb</surname></persName><email>Geoff.Webb@infotech.monash.edu.au</email><affiliation>Faculty of Information Technology, Monash University, VIC 3800, Australia</affiliation></editor><editor><persName><forename type="first">Xinghuo</forename><surname>Yu</surname></persName><email>x.yu@rmit.edu.au</email><affiliation>Science, Engineering and Technology Portfolio, Royal Melbourne Institute of Technology, VIC 3001, Melbourne, Australia</affiliation></editor><imprint><publisher>Springer Berlin Heidelberg</publisher><pubPlace>Berlin, Heidelberg</pubPlace><date type="published" when="2004"></date><biblScope unit="volume">3339</biblScope><biblScope unit="page" from="681">681</biblScope><biblScope unit="page" to="693">693</biblScope></imprint></monogr><series><title level="s">Lecture Notes in Computer Science</title><editor><persName><forename type="first">David</forename><surname>Hutchison</surname></persName><affiliation>Lancaster University, UK</affiliation></editor><editor><persName><forename type="first">Takeo</forename><surname>Kanade</surname></persName><affiliation>Carnegie Mellon University, Pittsburgh, PA, USA</affiliation></editor><editor><persName><forename type="first">Josef</forename><surname>Kittler</surname></persName><affiliation>University of Surrey, Guildford, UK</affiliation></editor><editor><persName><forename type="first">Jon</forename><forename type="first">M.</forename><surname>Kleinberg</surname></persName><affiliation>Cornell University, Ithaca, NY, USA</affiliation></editor><editor><persName><forename type="first">Friedemann</forename><surname>Mattern</surname></persName><affiliation>ETH Zurich, Switzerland</affiliation></editor><editor><persName><forename type="first">John</forename><forename type="first">C.</forename><surname>Mitchell</surname></persName><affiliation>Stanford University, CA, USA</affiliation></editor><editor><persName><forename type="first">Moni</forename><surname>Naor</surname></persName><affiliation>Weizmann Institute of Science, Rehovot, Israel</affiliation></editor><editor><persName><forename type="first">Oscar</forename><surname>Nierstrasz</surname></persName><affiliation>University of Bern, Switzerland</affiliation></editor><editor><persName><forename type="first">C.</forename><surname>Pandu Rangan</surname></persName><affiliation>Indian Institute of Technology, Madras, India</affiliation></editor><editor><persName><forename type="first">Bernhard</forename><surname>Steffen</surname></persName><affiliation>University of Dortmund, Germany</affiliation></editor><editor><persName><forename type="first">Madhu</forename><surname>Sudan</surname></persName><affiliation>Massachusetts Institute of Technology, MA, USA</affiliation></editor><editor><persName><forename type="first">Demetri</forename><surname>Terzopoulos</surname></persName><affiliation>New York University, NY, USA</affiliation></editor><editor><persName><forename type="first">Dough</forename><surname>Tygar</surname></persName><affiliation>University of California, Berkeley, CA, USA</affiliation></editor><editor><persName><forename type="first">Moshe</forename><forename type="first">Y.</forename><surname>Vardi</surname></persName><affiliation>Rice University, Houston, TX, USA</affiliation></editor><editor><persName><forename type="first">Gerhard</forename><surname>Weikum</surname></persName><affiliation>Max-Planck Institute of Computer Science, Saarbruecken, Germany</affiliation></editor><biblScope><date>2005</date></biblScope><idno type="pISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="series-Id">558</idno></series><series><title level="s">Lecture Notes in Artificial Intelligence</title><editor><persName><forename type="first">David</forename><surname>Hutchison</surname></persName><affiliation>Lancaster University, UK</affiliation></editor><editor><persName><forename type="first">Takeo</forename><surname>Kanade</surname></persName><affiliation>Carnegie Mellon University, Pittsburgh, PA, USA</affiliation></editor><editor><persName><forename type="first">Josef</forename><surname>Kittler</surname></persName><affiliation>University of Surrey, Guildford, UK</affiliation></editor><editor><persName><forename type="first">Jon</forename><forename type="first">M.</forename><surname>Kleinberg</surname></persName><affiliation>Cornell University, Ithaca, NY, USA</affiliation></editor><editor><persName><forename type="first">Friedemann</forename><surname>Mattern</surname></persName><affiliation>ETH Zurich, Switzerland</affiliation></editor><editor><persName><forename type="first">John</forename><forename type="first">C.</forename><surname>Mitchell</surname></persName><affiliation>Stanford University, CA, USA</affiliation></editor><editor><persName><forename type="first">Moni</forename><surname>Naor</surname></persName><affiliation>Weizmann Institute of Science, Rehovot, Israel</affiliation></editor><editor><persName><forename type="first">Oscar</forename><surname>Nierstrasz</surname></persName><affiliation>University of Bern, Switzerland</affiliation></editor><editor><persName><forename type="first">C.</forename><surname>Pandu Rangan</surname></persName><affiliation>Indian Institute of Technology, Madras, India</affiliation></editor><editor><persName><forename type="first">Bernhard</forename><surname>Steffen</surname></persName><affiliation>University of Dortmund, Germany</affiliation></editor><editor><persName><forename type="first">Madhu</forename><surname>Sudan</surname></persName><affiliation>Massachusetts Institute of Technology, MA, USA</affiliation></editor><editor><persName><forename type="first">Demetri</forename><surname>Terzopoulos</surname></persName><affiliation>New York University, NY, USA</affiliation></editor><editor><persName><forename type="first">Dough</forename><surname>Tygar</surname></persName><affiliation>University of California, Berkeley, CA, USA</affiliation></editor><editor><persName><forename type="first">Moshe</forename><forename type="first">Y.</forename><surname>Vardi</surname></persName><affiliation>Rice University, Houston, TX, USA</affiliation></editor><editor><persName><forename type="first">Gerhard</forename><surname>Weikum</surname></persName><affiliation>Max-Planck Institute of Computer Science, Saarbruecken, Germany</affiliation></editor><editor><persName><forename type="first">Jaime</forename><forename type="first">G.</forename><surname>Carbonell</surname></persName><affiliation>Carnegie Mellon University, Pittsburgh, PA, USA</affiliation></editor><editor><persName><forename type="first">Jörg</forename><surname>Siekmann</surname></persName><affiliation>University of Saarland, Saarbrücken, Germany</affiliation></editor><editor><persName><forename type="first">Geoffrey</forename><forename type="first">I.</forename><surname>Webb</surname></persName><email>Geoff.Webb@infotech.monash.edu.au</email><affiliation>Faculty of Information Technology, Monash University, VIC 3800, Australia</affiliation></editor><editor><persName><forename type="first">Xinghuo</forename><surname>Yu</surname></persName><email>x.yu@rmit.edu.au</email><affiliation>Science, Engineering and Technology Portfolio, Royal Melbourne Institute of Technology, VIC 3001, Melbourne, Australia</affiliation></editor><idno type="pISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><biblScope unit="seriesId">1244</biblScope></series><idno type="istex">E74E21DECC13ED4A2B10E61449622E0F569337BC</idno><idno type="DOI">10.1007/978-3-540-30549-1_59</idno><idno type="ChapterID">59</idno><idno type="ChapterID">Chap59</idno></biblStruct></sourceDesc></fileDesc><profileDesc><creation><date>2004</date></creation><langUsage><language ident="en">en</language></langUsage><abstract xml:lang="en"><p>Abstract: Quantified Boolean formulas (QBFs) play an important role in artificial intelligence subjects, specially in planning, knowledge representation and reasoning [20]. In this paper we present ZQSAT (sibling of our FZQSAT [15]), which is an algorithm for evaluating quantified Boolean formulas. QBF is a language that extends propositional logic in such a way that many advanced forms of reasoning can be easily formulated and evaluated. ZQSAT is based on ZDD, which is a variant of BDD, and an adopted version of the DPLL algorithm. The program has been implemented in C using the CUDD package. The capability of ZDDs in storing sets of subsets efficiently enabled us to store the clauses of a QBF very compactly and led us to implement the search algorithm in such a way that we could store and reuse the results of all previously solved subformulas with few overheads. This idea along some other techniques, enabled ZQSAT to solve some standard QBF benchmark problems faster than the best existing QSAT solvers.</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>I21017</label><label>I16048</label><label>I18032</label><label>I18040</label><label>I18024</label><label>I16013</label><item><term>Computer Science</term></item><item><term>Artificial Intelligence (incl. Robotics)</term></item><item><term>Mathematical Logic and Formal Languages</term></item><item><term>Information Storage and Retrieval</term></item><item><term>Information Systems Applications (incl.Internet)</term></item><item><term>Database Management</term></item><item><term>Computation by Abstract Devices</term></item></list></keywords></textClass></profileDesc><revisionDesc><change when="2004">Published</change><change xml:id="refBibs-istex" who="#ISTEX-API" when="2016-11-23">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/E74E21DECC13ED4A2B10E61449622E0F569337BC/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><SeriesElectronicISSN>1611-3349</SeriesElectronicISSN><SeriesTitle Language="En">Lecture Notes in Computer Science</SeriesTitle></SeriesInfo><SeriesHeader><EditorGroup><Editor AffiliationIDS="Aff1"><EditorName DisplayOrder="Western"><GivenName>David</GivenName><FamilyName>Hutchison</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff2"><EditorName DisplayOrder="Western"><GivenName>Takeo</GivenName><FamilyName>Kanade</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff3"><EditorName DisplayOrder="Western"><GivenName>Josef</GivenName><FamilyName>Kittler</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff4"><EditorName DisplayOrder="Western"><GivenName>Jon</GivenName><GivenName>M.</GivenName><FamilyName>Kleinberg</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff5"><EditorName DisplayOrder="Western"><GivenName>Friedemann</GivenName><FamilyName>Mattern</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff6"><EditorName DisplayOrder="Western"><GivenName>John</GivenName><GivenName>C.</GivenName><FamilyName>Mitchell</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff7"><EditorName DisplayOrder="Western"><GivenName>Moni</GivenName><FamilyName>Naor</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff8"><EditorName DisplayOrder="Western"><GivenName>Oscar</GivenName><FamilyName>Nierstrasz</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff9"><EditorName DisplayOrder="Western"><GivenName>C.</GivenName><FamilyName>Pandu Rangan</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff10"><EditorName DisplayOrder="Western"><GivenName>Bernhard</GivenName><FamilyName>Steffen</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff11"><EditorName DisplayOrder="Western"><GivenName>Madhu</GivenName><FamilyName>Sudan</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff12"><EditorName DisplayOrder="Western"><GivenName>Demetri</GivenName><FamilyName>Terzopoulos</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff13"><EditorName DisplayOrder="Western"><GivenName>Dough</GivenName><FamilyName>Tygar</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff14"><EditorName DisplayOrder="Western"><GivenName>Moshe</GivenName><GivenName>Y.</GivenName><FamilyName>Vardi</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff15"><EditorName DisplayOrder="Western"><GivenName>Gerhard</GivenName><FamilyName>Weikum</FamilyName></EditorName></Editor><Affiliation ID="Aff1"><OrgName>Lancaster University</OrgName><OrgAddress><Country>UK</Country></OrgAddress></Affiliation><Affiliation ID="Aff2"><OrgName>Carnegie Mellon University</OrgName><OrgAddress><City>Pittsburgh</City><State>PA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff3"><OrgName>University of Surrey</OrgName><OrgAddress><City>Guildford</City><Country>UK</Country></OrgAddress></Affiliation><Affiliation ID="Aff4"><OrgName>Cornell University</OrgName><OrgAddress><City>Ithaca</City><State>NY</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff5"><OrgName>ETH Zurich</OrgName><OrgAddress><Country>Switzerland</Country></OrgAddress></Affiliation><Affiliation ID="Aff6"><OrgName>Stanford University</OrgName><OrgAddress><City>CA</City><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff7"><OrgName>Weizmann Institute of Science</OrgName><OrgAddress><City>Rehovot</City><Country>Israel</Country></OrgAddress></Affiliation><Affiliation ID="Aff8"><OrgName>University of Bern</OrgName><OrgAddress><Country>Switzerland</Country></OrgAddress></Affiliation><Affiliation ID="Aff9"><OrgName>Indian Institute of Technology</OrgName><OrgAddress><City>Madras</City><Country>India</Country></OrgAddress></Affiliation><Affiliation ID="Aff10"><OrgName>University of Dortmund</OrgName><OrgAddress><Country>Germany</Country></OrgAddress></Affiliation><Affiliation ID="Aff11"><OrgName>Massachusetts Institute of Technology</OrgName><OrgAddress><City>MA</City><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff12"><OrgName>New York University</OrgName><OrgAddress><City>NY</City><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff13"><OrgName>University of California</OrgName><OrgAddress><City>Berkeley</City><State>CA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff14"><OrgName>Rice University</OrgName><OrgAddress><City>Houston</City><State>TX</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff15"><OrgName>Max-Planck Institute of Computer Science</OrgName><OrgAddress><City>Saarbruecken</City><Country>Germany</Country></OrgAddress></Affiliation></EditorGroup></SeriesHeader><SubSeries><SubSeriesInfo><SubSeriesID>1244</SubSeriesID><SubSeriesPrintISSN>0302-9743</SubSeriesPrintISSN><SubSeriesElectronicISSN>1611-3349</SubSeriesElectronicISSN><SubSeriesTitle Language="En">Lecture Notes in Artificial Intelligence</SubSeriesTitle></SubSeriesInfo><SubSeriesHeader><EditorGroup><Editor AffiliationIDS="Aff16"><EditorName DisplayOrder="Western"><GivenName>Jaime</GivenName><GivenName>G.</GivenName><FamilyName>Carbonell</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff17"><EditorName DisplayOrder="Western"><GivenName>Jörg</GivenName><FamilyName>Siekmann</FamilyName></EditorName></Editor><Affiliation ID="Aff16"><OrgName>Carnegie Mellon University</OrgName><OrgAddress><City>Pittsburgh</City><State>PA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff17"><OrgName>University of Saarland</OrgName><OrgAddress><City>Saarbrücken</City><Country>Germany</Country></OrgAddress></Affiliation></EditorGroup></SubSeriesHeader></SubSeries><Book Language="En"><BookInfo BookProductType="Proceedings" ContainsESM="No" Language="En" MediaType="eBook" NumberingDepth="2" NumberingStyle="ContentOnly" OutputMedium="All" TocLevels="0"><BookID>978-3-540-30549-1</BookID><BookTitle>AI 2004: Advances in Artificial Intelligence</BookTitle><BookSubTitle>17th Australian Joint Conference on Artificial Intelligence, Cairns, Australia, December 4-6, 2004. Proceedings</BookSubTitle><BookVolumeNumber>3339</BookVolumeNumber><BookSequenceNumber>3339</BookSequenceNumber><BookDOI>10.1007/b104336</BookDOI><BookTitleID>115428</BookTitleID><BookPrintISBN>978-3-540-24059-4</BookPrintISBN><BookElectronicISBN>978-3-540-30549-1</BookElectronicISBN><BookChapterCount>132</BookChapterCount><BookCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2005</CopyrightYear></BookCopyright><BookSubjectGroup><BookSubject Code="I" Type="Primary">Computer Science</BookSubject><BookSubject Code="I21017" Priority="1" Type="Secondary">Artificial Intelligence (incl. Robotics)</BookSubject><BookSubject Code="I16048" Priority="2" Type="Secondary">Mathematical Logic and Formal Languages</BookSubject><BookSubject Code="I18032" Priority="3" Type="Secondary">Information Storage and Retrieval</BookSubject><BookSubject Code="I18040" Priority="4" Type="Secondary">Information Systems Applications (incl.Internet)</BookSubject><BookSubject Code="I18024" Priority="5" Type="Secondary">Database Management</BookSubject><BookSubject Code="I16013" Priority="6" Type="Secondary">Computation by Abstract Devices</BookSubject><SubjectCollection Code="SUCO11645">Computer Science</SubjectCollection></BookSubjectGroup><BookContext><SeriesID>558</SeriesID><SubSeriesID>1244</SubSeriesID></BookContext></BookInfo><BookHeader><EditorGroup><Editor AffiliationIDS="Aff18"><EditorName DisplayOrder="Western"><GivenName>Geoffrey</GivenName><GivenName>I.</GivenName><FamilyName>Webb</FamilyName></EditorName><Contact><Email>Geoff.Webb@infotech.monash.edu.au</Email></Contact></Editor><Editor AffiliationIDS="Aff19"><EditorName DisplayOrder="Western"><GivenName>Xinghuo</GivenName><FamilyName>Yu</FamilyName></EditorName><Contact><Email>x.yu@rmit.edu.au</Email></Contact></Editor><Affiliation ID="Aff18"><OrgDivision>Faculty of Information Technology</OrgDivision><OrgName>Monash University</OrgName><OrgAddress><Postcode>VIC 3800</Postcode><Country>Australia</Country></OrgAddress></Affiliation><Affiliation ID="Aff19"><OrgName>Science, Engineering and Technology Portfolio, Royal Melbourne Institute of Technology</OrgName><OrgAddress><Postcode>VIC 3001</Postcode><City>Melbourne</City><Country>Australia</Country></OrgAddress></Affiliation></EditorGroup></BookHeader><Part ID="Part1"><PartInfo TocLevels="0"><PartID>1</PartID><PartSequenceNumber>1</PartSequenceNumber><PartTitle>Full Papers</PartTitle><PartChapterCount>77</PartChapterCount><PartContext><SeriesID>558</SeriesID><BookTitle>AI 2004: Advances in Artificial Intelligence</BookTitle></PartContext></PartInfo><SubPart ID="SubPart7"><SubPartInfo><SubPartID>7</SubPartID><SubPartSequenceNumber>7</SubPartSequenceNumber><SubPartTitle>Problem Solving and Reasoning</SubPartTitle><SubPartChapterCount>9</SubPartChapterCount></SubPartInfo><Chapter ID="Chap59" Language="En"><ChapterInfo ChapterType="OriginalPaper" ContainsESM="No" NumberingDepth="2" NumberingStyle="ContentOnly" TocLevels="0"><ChapterID>59</ChapterID><ChapterDOI>10.1007/978-3-540-30549-1_59</ChapterDOI><ChapterSequenceNumber>59</ChapterSequenceNumber><ChapterTitle Language="En">Embedding Memoization to the Semantic Tree Search for Deciding QBFs</ChapterTitle><ChapterFirstPage>681</ChapterFirstPage><ChapterLastPage>693</ChapterLastPage><ChapterCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2004</CopyrightYear></ChapterCopyright><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>1</PartID><BookID>978-3-540-30549-1</BookID><BookTitle>AI 2004: Advances in Artificial Intelligence</BookTitle></ChapterContext></ChapterInfo><ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff20"><AuthorName DisplayOrder="Western"><GivenName>Mohammad</GivenName><FamilyName>GhasemZadeh</FamilyName></AuthorName><Contact><Email>GhasemZadeh@TI.Uni-Trier.DE</Email></Contact></Author><Author AffiliationIDS="Aff20"><AuthorName DisplayOrder="Western"><GivenName>Volker</GivenName><FamilyName>Klotz</FamilyName></AuthorName><Contact><Email>klotz@TI.Uni-Trier.DE</Email></Contact></Author><Author AffiliationIDS="Aff20"><AuthorName DisplayOrder="Western"><GivenName>Christoph</GivenName><FamilyName>Meinel</FamilyName></AuthorName><Contact><Email>meinel@TI.Uni-Trier.DE</Email></Contact></Author><Affiliation ID="Aff20"><OrgDivision>FB-IV Informatik</OrgDivision><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>Quantified Boolean formulas (QBFs) play an important role in artificial intelligence subjects, specially in planning, knowledge representation and reasoning [20]. In this paper we present ZQSAT (sibling of our FZQSAT [15]), which is an algorithm for evaluating quantified Boolean formulas. QBF is a language that extends propositional logic in such a way that many advanced forms of reasoning can be easily formulated and evaluated. ZQSAT is based on ZDD, which is a variant of BDD, and an adopted version of the DPLL algorithm. The program has been implemented in C using the CUDD package. The capability of ZDDs in storing sets of subsets efficiently enabled us to store the clauses of a QBF very compactly and led us to implement the search algorithm in such a way that we could store and reuse the results of all previously solved subformulas with few overheads. This idea along some other techniques, enabled ZQSAT to solve some standard QBF benchmark problems faster than the best existing QSAT solvers.</Para></Abstract><KeywordGroup Language="En"><Heading>Keywords</Heading><Keyword>DPLL</Keyword><Keyword>Zero-Suppressed Binary Decision Diagram (ZDD)</Keyword><Keyword>Quantified Boolean Formula (QBF)</Keyword><Keyword>Satisfiability</Keyword><Keyword>QSAT</Keyword></KeywordGroup></ChapterHeader><NoBody></NoBody></Chapter></SubPart></Part></Book></Series></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Embedding Memoization to the Semantic Tree Search for Deciding QBFs</title></titleInfo><titleInfo type="alternative" contentType="CDATA" lang="en"><title>Embedding Memoization to the Semantic Tree Search for Deciding QBFs</title></titleInfo><name type="personal"><namePart type="given">Mohammad</namePart><namePart type="family">GhasemZadeh</namePart><affiliation>FB-IV Informatik, University of Trier, D-54286, Trier, Germany</affiliation><affiliation>E-mail: GhasemZadeh@TI.Uni-Trier.DE</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Volker</namePart><namePart type="family">Klotz</namePart><affiliation>FB-IV Informatik, University of Trier, D-54286, Trier, Germany</affiliation><affiliation>E-mail: klotz@TI.Uni-Trier.DE</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Christoph</namePart><namePart type="family">Meinel</namePart><affiliation>FB-IV Informatik, University of Trier, D-54286, Trier, Germany</affiliation><affiliation>E-mail: meinel@TI.Uni-Trier.DE</affiliation><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre type="conference" displayLabel="proceedings"></genre><originInfo><publisher>Springer Berlin Heidelberg</publisher><place><placeTerm type="text">Berlin, Heidelberg</placeTerm></place><dateIssued encoding="w3cdtf">2004</dateIssued><copyrightDate encoding="w3cdtf">2004</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: Quantified Boolean formulas (QBFs) play an important role in artificial intelligence subjects, specially in planning, knowledge representation and reasoning [20]. In this paper we present ZQSAT (sibling of our FZQSAT [15]), which is an algorithm for evaluating quantified Boolean formulas. QBF is a language that extends propositional logic in such a way that many advanced forms of reasoning can be easily formulated and evaluated. ZQSAT is based on ZDD, which is a variant of BDD, and an adopted version of the DPLL algorithm. The program has been implemented in C using the CUDD package. The capability of ZDDs in storing sets of subsets efficiently enabled us to store the clauses of a QBF very compactly and led us to implement the search algorithm in such a way that we could store and reuse the results of all previously solved subformulas with few overheads. This idea along some other techniques, enabled ZQSAT to solve some standard QBF benchmark problems faster than the best existing QSAT solvers.</abstract><relatedItem type="host"><titleInfo><title>AI 2004: Advances in Artificial Intelligence</title><subTitle>17th Australian Joint Conference on Artificial Intelligence, Cairns, Australia, December 4-6, 2004. Proceedings</subTitle></titleInfo><name type="personal"><namePart type="given">Geoffrey</namePart><namePart type="given">I.</namePart><namePart type="family">Webb</namePart><affiliation>Faculty of Information Technology, Monash University, VIC 3800, Australia</affiliation><affiliation>E-mail: Geoff.Webb@infotech.monash.edu.au</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Xinghuo</namePart><namePart type="family">Yu</namePart><affiliation>Science, Engineering and Technology Portfolio, Royal Melbourne Institute of Technology, VIC 3001, Melbourne, Australia</affiliation><affiliation>E-mail: x.yu@rmit.edu.au</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><genre type="book-series" displayLabel="Proceedings"></genre><originInfo><copyrightDate encoding="w3cdtf">2005</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="I21017">Artificial Intelligence (incl. Robotics)</topic><topic authority="SpringerSubjectCodes" authorityURI="I16048">Mathematical Logic and Formal Languages</topic><topic authority="SpringerSubjectCodes" authorityURI="I18032">Information Storage and Retrieval</topic><topic authority="SpringerSubjectCodes" authorityURI="I18040">Information Systems Applications (incl.Internet)</topic><topic authority="SpringerSubjectCodes" authorityURI="I18024">Database Management</topic><topic authority="SpringerSubjectCodes" authorityURI="I16013">Computation by Abstract Devices</topic></subject><identifier type="DOI">10.1007/b104336</identifier><identifier type="ISBN">978-3-540-24059-4</identifier><identifier type="eISBN">978-3-540-30549-1</identifier><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="BookTitleID">115428</identifier><identifier type="BookID">978-3-540-30549-1</identifier><identifier type="BookChapterCount">132</identifier><identifier type="BookVolumeNumber">3339</identifier><identifier type="BookSequenceNumber">3339</identifier><identifier type="PartChapterCount">77</identifier><part><date>2005</date><detail type="part"><title>Full Papers</title></detail><detail type="volume"><number>3339</number><caption>vol.</caption></detail><extent unit="pages"><start>681</start><end>693</end></extent></part><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2005</recordOrigin></recordInfo></relatedItem><relatedItem type="series"><titleInfo><title>Lecture Notes in Computer Science</title></titleInfo><name type="personal"><namePart type="given">David</namePart><namePart type="family">Hutchison</namePart><affiliation>Lancaster University, UK</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Takeo</namePart><namePart type="family">Kanade</namePart><affiliation>Carnegie Mellon University, Pittsburgh, PA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Josef</namePart><namePart type="family">Kittler</namePart><affiliation>University of Surrey, Guildford, UK</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jon</namePart><namePart type="given">M.</namePart><namePart type="family">Kleinberg</namePart><affiliation>Cornell University, Ithaca, NY, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Friedemann</namePart><namePart type="family">Mattern</namePart><affiliation>ETH Zurich, Switzerland</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">John</namePart><namePart type="given">C.</namePart><namePart type="family">Mitchell</namePart><affiliation>Stanford University, CA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Moni</namePart><namePart type="family">Naor</namePart><affiliation>Weizmann Institute of Science, Rehovot, Israel</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Oscar</namePart><namePart type="family">Nierstrasz</namePart><affiliation>University of Bern, Switzerland</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">C.</namePart><namePart type="family">Pandu Rangan</namePart><affiliation>Indian Institute of Technology, Madras, India</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Bernhard</namePart><namePart type="family">Steffen</namePart><affiliation>University of Dortmund, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Madhu</namePart><namePart type="family">Sudan</namePart><affiliation>Massachusetts Institute of Technology, MA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Demetri</namePart><namePart type="family">Terzopoulos</namePart><affiliation>New York University, NY, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Dough</namePart><namePart type="family">Tygar</namePart><affiliation>University of California, Berkeley, CA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Moshe</namePart><namePart type="given">Y.</namePart><namePart type="family">Vardi</namePart><affiliation>Rice University, Houston, TX, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Gerhard</namePart><namePart type="family">Weikum</namePart><affiliation>Max-Planck Institute of Computer Science, Saarbruecken, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><originInfo><copyrightDate encoding="w3cdtf">2005</copyrightDate><issuance>serial</issuance></originInfo><relatedItem type="constituent"><titleInfo><title>Lecture Notes in Artificial Intelligence</title></titleInfo><name type="personal"><namePart type="given">David</namePart><namePart type="family">Hutchison</namePart><affiliation>Lancaster University, UK</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Takeo</namePart><namePart type="family">Kanade</namePart><affiliation>Carnegie Mellon University, Pittsburgh, PA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Josef</namePart><namePart type="family">Kittler</namePart><affiliation>University of Surrey, Guildford, UK</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jon</namePart><namePart type="given">M.</namePart><namePart type="family">Kleinberg</namePart><affiliation>Cornell University, Ithaca, NY, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Friedemann</namePart><namePart type="family">Mattern</namePart><affiliation>ETH Zurich, Switzerland</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">John</namePart><namePart type="given">C.</namePart><namePart type="family">Mitchell</namePart><affiliation>Stanford University, CA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Moni</namePart><namePart type="family">Naor</namePart><affiliation>Weizmann Institute of Science, Rehovot, Israel</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Oscar</namePart><namePart type="family">Nierstrasz</namePart><affiliation>University of Bern, Switzerland</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">C.</namePart><namePart type="family">Pandu Rangan</namePart><affiliation>Indian Institute of Technology, Madras, India</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Bernhard</namePart><namePart type="family">Steffen</namePart><affiliation>University of Dortmund, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Madhu</namePart><namePart type="family">Sudan</namePart><affiliation>Massachusetts Institute of Technology, MA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Demetri</namePart><namePart type="family">Terzopoulos</namePart><affiliation>New York University, NY, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Dough</namePart><namePart type="family">Tygar</namePart><affiliation>University of California, Berkeley, CA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Moshe</namePart><namePart type="given">Y.</namePart><namePart type="family">Vardi</namePart><affiliation>Rice University, Houston, TX, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Gerhard</namePart><namePart type="family">Weikum</namePart><affiliation>Max-Planck Institute of Computer Science, Saarbruecken, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jaime</namePart><namePart type="given">G.</namePart><namePart type="family">Carbonell</namePart><affiliation>Carnegie Mellon University, Pittsburgh, PA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jörg</namePart><namePart type="family">Siekmann</namePart><affiliation>University of Saarland, Saarbrücken, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Geoffrey</namePart><namePart type="given">I.</namePart><namePart type="family">Webb</namePart><affiliation>Faculty of Information Technology, Monash University, VIC 3800, Australia</affiliation><affiliation>E-mail: Geoff.Webb@infotech.monash.edu.au</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Xinghuo</namePart><namePart type="family">Yu</namePart><affiliation>Science, Engineering and Technology Portfolio, Royal Melbourne Institute of Technology, VIC 3001, Melbourne, Australia</affiliation><affiliation>E-mail: x.yu@rmit.edu.au</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><genre type="sub-series"></genre><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="SubSeriesID">1244</identifier></relatedItem><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="SeriesID">558</identifier><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2005</recordOrigin></recordInfo></relatedItem><identifier type="istex">E74E21DECC13ED4A2B10E61449622E0F569337BC</identifier><identifier type="DOI">10.1007/978-3-540-30549-1_59</identifier><identifier type="ChapterID">59</identifier><identifier type="ChapterID">Chap59</identifier><accessCondition type="use and reproduction" contentType="copyright">Springer-Verlag Berlin Heidelberg, 2004</accessCondition><recordInfo><recordContentSource>SPRINGER</recordContentSource><recordOrigin>Springer-Verlag Berlin Heidelberg, 2004</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 001570 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 001570 | 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:E74E21DECC13ED4A2B10E61449622E0F569337BC
|texte= Embedding Memoization to the Semantic Tree Search for Deciding QBFs
}}
| This area was generated with Dilib version V0.6.31. |  |