{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T14:00:08Z","timestamp":1777125608127,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642027765","type":"print"},{"value":"9783642027772","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02777-2_37","type":"book-chapter","created":{"date-parts":[[2009,6,26]],"date-time":"2009-06-26T02:58:18Z","timestamp":1245985098000},"page":"398-411","source":"Crossref","is-referenced-by-count":8,"title":["A Compact Representation for Syntactic Dependencies in QBFs"],"prefix":"10.1007","author":[{"given":"Florian","family":"Lonsing","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"37_CR1","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1137\/0201008","volume":"1","author":"A.V. Aho","year":"1972","unstructured":"Aho, A.V., Garey, M.R., Ullman, J.D.: The Transitive Reduction of a Directed Graph. SIAM J. Comput.\u00a01(2), 131\u2013137 (1972)","journal-title":"SIAM J. Comput."},{"key":"37_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/3-540-36126-X_12","volume-title":"Formal Methods in Computer-Aided Design","author":"A. Ayari","year":"2002","unstructured":"Ayari, A., Basin, D.A.: QUBOS: Deciding Quantified Boolean Logic Using Propositional Satisfiability Solvers. In: Aagaard, M., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 187\u2013201. Springer, Heidelberg (2002)"},{"key":"37_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"Theory and Applications of Satisfiability Testing","year":"2005","unstructured":"Bacchus, F., Walsh, T. (eds.): SAT 2005. LNCS, vol.\u00a03569. Springer, Heidelberg (2005)"},{"key":"37_CR4","doi-asserted-by":"crossref","unstructured":"Benedetti, M.: Quantifier Trees for QBFs. In: [3], pp. 378\u2013385","DOI":"10.1007\/11499107_28"},{"key":"37_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/11532231_27","volume-title":"Automated Deduction \u2013 CADE-20","author":"M. Benedetti","year":"2005","unstructured":"Benedetti, M.: sKizzo: A Suite to Evaluate and Certify QBFs. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS, vol.\u00a03632, pp. 369\u2013376. Springer, Heidelberg (2005)"},{"key":"37_CR6","first-page":"133","volume":"5","author":"M. Benedetti","year":"2008","unstructured":"Benedetti, M., Mangassarian, H.: QBF-Based Formal Verification: Experience and Perspectives. JSAT\u00a05, 133\u2013191 (2008)","journal-title":"JSAT"},{"key":"37_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/11527695_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"A. Biere","year":"2005","unstructured":"Biere, A.: Resolve and Expand. In: Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 59\u201370. Springer, Heidelberg (2005)"},{"key":"37_CR8","doi-asserted-by":"crossref","unstructured":"Bubeck, U., Kleine B\u00fcning, H.: Bounded Universal Expansion for Preprocessing QBF. In: Marques-Silva, Sakallah (eds.) [23], pp. 244\u2013257","DOI":"10.1007\/978-3-540-72788-0_24"},{"issue":"1","key":"37_CR9","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"H. Kleine B\u00fcning","year":"1995","unstructured":"Kleine B\u00fcning, H., Karpinski, M., Fl\u00f6gel, A.: Resolution for Quantified Boolean Formulas. Inf. Comput.\u00a0117(1), 12\u201318 (1995)","journal-title":"Inf. Comput."},{"key":"37_CR10","unstructured":"Cadoli, M., Giovanardi, A., Schaerf, M.: An Algorithm to Evaluate Quantified Boolean Formulae. In: AAAI\/IAAI, pp. 262\u2013267 (1998)"},{"key":"37_CR11","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Hanna, Z., Katz, J.: Bounded Model Checking with QBF. In: [3], pp. 408\u2013414","DOI":"10.1007\/11499107_32"},{"key":"37_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-540-24605-3_17","volume-title":"Theory and Applications of Satisfiability Testing","author":"U. Egly","year":"2004","unstructured":"Egly, U., Seidl, M., Tompits, H., Woltran, S., Zolda, M.: Comparing Different Prenexing Strategies for Quantified Boolean Formulas. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 214\u2013228. Springer, Heidelberg (2004)"},{"key":"37_CR13","series-title":"FAIA","first-page":"477","volume-title":"ECAI","author":"U. Egly","year":"2006","unstructured":"Egly, U., Seidl, M., Woltran, S.: A Solver for QBFs in Nonprenex Form. In: Brewka, G., Coradeschi, S., Perini, A., Traverso, P. (eds.) ECAI. FAIA, vol.\u00a0141, pp. 477\u2013481. IOS Press, Amsterdam (2006)"},{"key":"37_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/3-540-45744-5_27","volume-title":"Automated Reasoning","author":"E. Giunchiglia","year":"2001","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: QUBE: A System for Deciding Quantified Boolean Formulas Satisfiability. In: Gor\u00e9, R., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS, vol.\u00a02083, pp. 364\u2013369. Springer, Heidelberg (2001)"},{"key":"37_CR15","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: QBF Solver Evaluation Portal, 2001-2009, http:\/\/www.qbflib.org\/index_eval.php"},{"key":"37_CR16","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Learning for Quantified Boolean Logic Satisfiability. In: AAAI\/IAAI, pp. 649\u2013654 (2002)"},{"issue":"1-2","key":"37_CR17","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/S0004-3702(02)00373-9","volume":"145","author":"E. Giunchiglia","year":"2003","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Backjumping for Quantified Boolean Logic satisfiability. Artif. Intell.\u00a0145(1-2), 99\u2013120 (2003)","journal-title":"Artif. Intell."},{"issue":"3","key":"37_CR18","first-page":"497","volume":"26","author":"E. Giunchiglia","year":"2007","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Quantifier Structure in Search-Based Procedures for QBFs. TCAD\u00a026(3), 497\u2013507 (2007)","journal-title":"TCAD"},{"issue":"3","key":"37_CR19","first-page":"45","volume":"174","author":"T. Jussila","year":"2007","unstructured":"Jussila, T., Biere, A.: Compressing BMC Encodings with QBF. ENTCS\u00a0174(3), 45\u201356 (2007)","journal-title":"ENTCS"},{"key":"37_CR20","doi-asserted-by":"crossref","unstructured":"Jussila, T., Biere, A., Sinz, C., Kr\u00f6ning, D., Wintersteiger, C.M.: A First Step Towards a Unified Proof Checker for QBF. In: Marques-Silva, Sakallah (eds.) [23], pp. 201\u2013214","DOI":"10.1007\/978-3-540-72788-0_21"},{"key":"37_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-45616-3_12","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"R. Letz","year":"2002","unstructured":"Letz, R.: Lemma and Model Caching in Decision Procedures for Quantified Boolean Formulas. In: Egly, U., Ferm\u00fcller, C.G. (eds.) TABLEAUX 2002. LNCS, vol.\u00a02381, pp. 160\u2013175. Springer, Heidelberg (2002)"},{"key":"37_CR22","doi-asserted-by":"crossref","unstructured":"Lonsing, F., Biere, A.: Efficiently Representing Existential Dependency Sets for Expansion-based QBF Solvers. In: Proc.\u00a0MEMICS, pp. 148\u2013155 (2008)","DOI":"10.1016\/j.entcs.2009.08.029"},{"key":"37_CR23","series-title":"Lecture Notes in Computer Science","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","year":"2007","unstructured":"Marques-Silva, J., Sakallah, K.A. (eds.): SAT 2007. LNCS, vol.\u00a04501. Springer, Heidelberg (2007)"},{"key":"37_CR24","unstructured":"QBFLIB. QDIMACS Standard v1.1, http:\/\/www.qbflib.org\/qdimacs.html"},{"issue":"1","key":"37_CR25","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/s10817-008-9114-5","volume":"42","author":"M. Samer","year":"2009","unstructured":"Samer, M., Szeider, S.: Backdoor Sets of Quantified Boolean Formulas. Journal of Automated Reasoning (JAR)\u00a042(1), 77\u201397 (2009)","journal-title":"Journal of Automated Reasoning (JAR)"},{"key":"37_CR26","first-page":"1","volume-title":"STOC","author":"L.J. Stockmeyer","year":"1973","unstructured":"Stockmeyer, L.J., Meyer, A.R.: Word Problems Requiring Exponential Time: Preliminary Report. In: STOC, pp. 1\u20139. ACM, New York (1973)"},{"issue":"2","key":"37_CR27","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1145\/321879.321884","volume":"22","author":"R.E. Tarjan","year":"1975","unstructured":"Tarjan, R.E.: Efficiency of a Good But Not Linear Set Union Algorithm. J. ACM\u00a022(2), 215\u2013225 (1975)","journal-title":"J. ACM"},{"key":"37_CR28","first-page":"442","volume-title":"ICCAD","author":"L. Zhang","year":"2002","unstructured":"Zhang, L., Malik, S.: Conflict driven learning in a quantified Boolean Satisfiability solver. In: Pileggi, L.T., Kuehlmann, A. (eds.) ICCAD, pp. 442\u2013449. ACM, New York (2002)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing - SAT 2009"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02777-2_37","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T22:58:08Z","timestamp":1558393088000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02777-2_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642027765","9783642027772"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02777-2_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}