{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T14:04:57Z","timestamp":1777125897785,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642141850","type":"print"},{"value":"9783642141867","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-14186-7_14","type":"book-chapter","created":{"date-parts":[[2010,7,8]],"date-time":"2010-07-08T18:20:37Z","timestamp":1278613237000},"page":"158-171","source":"Crossref","is-referenced-by-count":30,"title":["Integrating Dependency Schemes in Search-Based QBF Solvers"],"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":[{"key":"14_CR1","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":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/11499107_28","volume-title":"Theory and Applications of Satisfiability Testing","author":"M. Benedetti","year":"2005","unstructured":"Benedetti, M.: Quantifier Trees for QBFs. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 378\u2013385. Springer, Heidelberg (2005)"},{"issue":"1-3","key":"14_CR3","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10817-005-9005-y","volume":"35","author":"A. Bhalla","year":"2005","unstructured":"Bhalla, A., Lynce, I., de Sousa, J.T., Marques-Silva, J.: Heuristic-Based Backtracking Relaxation for Propositional Satisfiability. Journal of Automated Reasoning (JAR)\u00a035(1-3), 3\u201324 (2005)","journal-title":"Journal of Automated Reasoning (JAR)"},{"key":"14_CR4","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.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 59\u201370. Springer, Heidelberg (2005)"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Bubeck, U., B\u00fcning, H.K.: Bounded Universal Expansion for Preprocessing QBF. In: Marques-Silva, Sakallah (eds.) [25], pp. 244\u2013257.","DOI":"10.1007\/978-3-540-72788-0_24"},{"issue":"1","key":"14_CR6","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":"14_CR7","unstructured":"Cadoli, M., Giovanardi, A., Schaerf, M.: An Algorithm to Evaluate Quantified Boolean Formulae. In: AAAI\/IAAI, pp. 262\u2013267 (1998)"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Egly, U., Seidl, M., Tompits, H., Woltran, S., Zolda, M.: Comparing Different Prenexing Strategies for Quantified Boolean Formulas. In: Giunchiglia, Tacchella (eds.) [17], pp. 214\u2013228","DOI":"10.1007\/978-3-540-24605-3_17"},{"key":"14_CR9","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":"14_CR10","doi-asserted-by":"crossref","unstructured":"Gent, I.P., Giunchiglia, E., Narizzano, M., Rowley, A.G.D., Tacchella, A.: Watched Data Structures for QBF Solvers. In: Giunchiglia, Tacchella (eds.) [17], pp. 25\u201336 (2003)","DOI":"10.1007\/978-3-540-24605-3_3"},{"key":"14_CR11","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Quantified Boolean Formulas Satisfiability Library, QBFLIB (2001), http:\/\/www.qbflib.org"},{"key":"14_CR12","series-title":"Lecture Notes in Artificial Intelligence","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.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 364\u2013369. Springer, Heidelberg (2001)"},{"key":"14_CR13","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Learning for Quantified Boolean Logic Satisfiability. In: AAAI\/IAAI, pp. 649\u2013654 (2002)"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Monotone Literals and Learning in QBF Reasoning. In: Wallace (ed.) [31], pp. 260\u2013273 (2004)","DOI":"10.1007\/978-3-540-30201-8_21"},{"key":"14_CR15","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1613\/jair.1959","volume":"26","author":"E. Giunchiglia","year":"2006","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Clause\/Term Resolution and Learning in the Evaluation of Quantified Boolean Formulas. J. Artif. Intell. Res. (JAIR)\u00a026, 371\u2013416 (2006)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"issue":"3","key":"14_CR16","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"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","volume-title":"Theory and Applications of Satisfiability Testing","year":"2004","unstructured":"Giunchiglia, E., Tacchella, A. (eds.): SAT 2003. LNCS, vol.\u00a02919. Springer, Heidelberg (2004)"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Goultiaeva, A., Iverson, V., Bacchus, F.: Beyond CNF: A Circuit-Based QBF Solver. In: Kullmann (ed.) [21], pp. 412\u2013426","DOI":"10.1007\/978-3-642-02777-2_38"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Pan, G., Vardi, M.Y.: Symbolic Decision Procedures for QBF. In: Wallace (ed.) [31], pp. 453\u2013467","DOI":"10.1007\/978-3-540-30201-8_34"},{"key":"14_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.) [25], pp. 201\u2013214","DOI":"10.1007\/978-3-540-72788-0_21"},{"key":"14_CR21","series-title":"Lecture Notes in Computer Science","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","year":"2009","unstructured":"Kullmann, O. (ed.): SAT 2009. LNCS, vol.\u00a05584. Springer, Heidelberg (2009)"},{"key":"14_CR22","series-title":"Lecture Notes in Artificial Intelligence","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 (LNAI), vol.\u00a02381, pp. 160\u2013175. Springer, Heidelberg (2002)"},{"key":"14_CR23","unstructured":"Lonsing, F.: DepQBF 0.1 Source Code (2010), http:\/\/fmv.jku.at\/depqbf\/"},{"key":"14_CR24","doi-asserted-by":"crossref","unstructured":"Lonsing, F., Biere, A.: A Compact Representation for Syntactic Dependencies in QBFs. In: Kullmann (ed.) [21], pp. 398\u2013411","DOI":"10.1007\/978-3-642-02777-2_37"},{"key":"14_CR25","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":"14_CR26","first-page":"530","volume-title":"DAC 2001","author":"M.W. Moskewicz","year":"2001","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: DAC 2001, pp. 530\u2013535. ACM, New York (2001)"},{"key":"14_CR27","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/978-3-540-89439-1_36","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Samer","year":"2008","unstructured":"Samer, M.: Variable Dependencies of Quantified CSPs. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 512\u2013527. Springer, Heidelberg (2008)"},{"key":"14_CR28","first-page":"1596","volume-title":"DATE","author":"F. Pigorsch","year":"2009","unstructured":"Pigorsch, F., Scholl, C.: Exploiting structure in an AIG based QBF solver. In: DATE, pp. 1596\u20131601. IEEE, Los Alamitos (2009)"},{"key":"14_CR29","doi-asserted-by":"crossref","unstructured":"Pipatsrisawat, K., Darwiche, A.: A Lightweight Component Caching Scheme for Satisfiability Solvers. In: Marques-Silva, Sakallah (eds.) [25], pp. 294\u2013299","DOI":"10.1007\/978-3-540-72788-0_28"},{"issue":"1","key":"14_CR30","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":"14_CR31","series-title":"Lecture Notes in Computer Science","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2004","year":"2004","unstructured":"Wallace, M. (ed.): CP 2004. LNCS, vol.\u00a03258. Springer, Heidelberg (2004)"},{"key":"14_CR32","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)"},{"key":"14_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-46135-3_14","volume-title":"Principles and Practice of Constraint Programming - CP 2002","author":"L. Zhang","year":"2002","unstructured":"Zhang, L., Malik, S.: Towards a Symmetric Treatment of Satisfaction and Conflicts in Quantified Boolean Formula Evaluation. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol.\u00a02470, pp. 200\u2013215. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2010"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14186-7_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T18:31:22Z","timestamp":1559241082000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14186-7_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642141850","9783642141867"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14186-7_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}