{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,12]],"date-time":"2026-09-12T01:56:24Z","timestamp":1789178184153,"version":"build-2803163510"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319104270","type":"print"},{"value":"9783319104287","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-10428-7_38","type":"book-chapter","created":{"date-parts":[[2014,8,12]],"date-time":"2014-08-12T21:33:54Z","timestamp":1407879234000},"page":"514-530","source":"Crossref","is-referenced-by-count":13,"title":["Incremental QBF Solving"],"prefix":"10.1007","author":[{"given":"Florian","family":"Lonsing","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Uwe","family":"Egly","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"38_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-642-39071-5_23","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"G. Audemard","year":"2013","unstructured":"Audemard, G., Lagniez, J.M., Simon, L.: Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol.\u00a07962, pp. 309\u2013317. Springer, Heidelberg (2013)"},{"issue":"1","key":"38_CR2","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/s10703-012-0152-6","volume":"41","author":"V. Balabanov","year":"2012","unstructured":"Balabanov, V., Jiang, J.R.: Unified QBF certification and its applications. Formal Methods in System Design\u00a041(1), 45\u201365 (2012)","journal-title":"Formal Methods in System Design"},{"key":"38_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/978-3-642-33386-6_29","volume-title":"Automated Technology for Verification and Analysis","author":"B. Becker","year":"2012","unstructured":"Becker, B., Ehlers, R., Lewis, M.D.T., Marin, P.: ALLQBF Solving by Computational Learning. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol.\u00a07561, pp. 370\u2013384. Springer, Heidelberg (2012)"},{"key":"38_CR4","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"},{"issue":"2-4","key":"38_CR5","first-page":"75","volume":"4","author":"A. Biere","year":"2008","unstructured":"Biere, A.: PicoSAT Essentials. JSAT\u00a04(2-4), 75\u201397 (2008)","journal-title":"JSAT"},{"key":"38_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-54013-4_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R. Bloem","year":"2014","unstructured":"Bloem, R., K\u00f6nighofer, R., Seidl, M.: SAT-Based Synthesis Methods for Safety Specs. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol.\u00a08318, pp. 1\u201320. Springer, Heidelberg (2014)"},{"issue":"1","key":"38_CR7","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"H.K. B\u00fcning","year":"1995","unstructured":"B\u00fcning, H.K., Karpinski, M., Fl\u00f6gel, A.: Resolution for Quantified Boolean Formulas. Inf. Comput.\u00a0117(1), 12\u201318 (1995)","journal-title":"Inf. Comput."},{"issue":"2","key":"38_CR8","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1023\/A:1015019416843","volume":"28","author":"M. Cadoli","year":"2002","unstructured":"Cadoli, M., Schaerf, M., Giovanardi, A., Giovanardi, M.: An Algorithm to Evaluate Quantified Boolean Formulae and Its Experimental Evaluation. J. Autom. Reasoning\u00a028(2), 101\u2013142 (2002)","journal-title":"J. Autom. Reasoning"},{"key":"38_CR9","unstructured":"Cashmore, M., Fox, M., Giunchiglia, E.: Planning as Quantified Boolean Formula. In: Raedt, L.D., Bessi\u00e8re, C., Dubois, D., Doherty, P., Frasconi, P., Heintz, F., Lucas, P.J.F. (eds.) ECAI. Frontiers in Artificial Intelligence and Applications, pp. 217\u2013222. IOS Press (2012)"},{"key":"38_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An Extensible SAT-Solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"issue":"4","key":"38_CR11","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1016\/S1571-0661(05)82542-3","volume":"89","author":"N. E\u00e9n","year":"2003","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Temporal Induction by Incremental SAT Solving. Electr. Notes Theor. Comput. Sci.\u00a089(4), 543\u2013560 (2003)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"38_CR12","doi-asserted-by":"crossref","unstructured":"Egly, U., Kronegger, M., Lonsing, F., Pfandler, A.: Conformant Planning as a Case Study of Incremental QBF Solving. CoRR abs\/1405.7253 (2014)","DOI":"10.1007\/978-3-319-13770-4_11"},{"key":"38_CR13","doi-asserted-by":"crossref","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)","DOI":"10.1613\/jair.1959"},{"key":"38_CR14","unstructured":"Goultiaeva, A., Van Gelder, A., Bacchus, F.: A Uniform Approach for Generating Proofs and Strategies for Both True and False QBF Formulas. In: Walsh, T. (ed.) IJCAI, pp. 546\u2013553. IJCAI\/AAAI (2011)"},{"key":"38_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-642-39071-5_8","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"A. Goultiaeva","year":"2013","unstructured":"Goultiaeva, A., Bacchus, F.: Recovering and Utilizing Partial Duality in QBF. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol.\u00a07962, pp. 83\u201399. Springer, Heidelberg (2013)"},{"key":"38_CR16","doi-asserted-by":"crossref","unstructured":"Goultiaeva, A., Seidl, M., Biere, A.: Bridging the Gap between Dual Propagation and CNF-based QBF Solving. In: Macii, E. (ed.) DATE, pp. 811\u2013814. EDA Consortium. ACM DL, San Jose (2013)","DOI":"10.7873\/DATE.2013.172"},{"key":"38_CR17","doi-asserted-by":"crossref","unstructured":"Hillebrecht, S., Kochte, M.A., Erb, D., Wunderlich, H.J., Becker, B.: Accurate QBF-Based Test Pattern Generation in Presence of Unknown Values. In: Macii, E. (ed.) DATE, pp. 436\u2013441. EDA Consortium, ACM DL, San Jose, CA, USA (2013)","DOI":"10.7873\/DATE.2013.098"},{"key":"38_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/978-3-642-45221-5_32","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Janota","year":"2013","unstructured":"Janota, M., Grigore, R., Marques-Silva, J.: On QBF Proofs and Preprocessing. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol.\u00a08312, pp. 473\u2013489. Springer, Heidelberg (2013)"},{"key":"38_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-642-14186-7_12","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"W. Klieber","year":"2010","unstructured":"Klieber, W., Sapra, S., Gao, S., Clarke, E.M.: A Non-prenex, Non-clausal QBF Solver with Game-State Learning. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol.\u00a06175, pp. 128\u2013142. Springer, Heidelberg (2010)"},{"key":"38_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-642-39071-5_21","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"J.M. Lagniez","year":"2013","unstructured":"Lagniez, J.M., Biere, A.: Factoring Out Assumptions to Speed Up MUS Extraction. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol.\u00a07962, pp. 276\u2013292. Springer, Heidelberg (2013)"},{"key":"38_CR21","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. (eds.) TABLEAUX 2002. LNCS (LNAI), vol.\u00a02381, pp. 160\u2013175. Springer, Heidelberg (2002)"},{"key":"38_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-642-14186-7_14","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"F. Lonsing","year":"2010","unstructured":"Lonsing, F., Biere, A.: Integrating Dependency Schemes in Search-Based QBF Solvers. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol.\u00a06175, pp. 158\u2013171. Springer, Heidelberg (2010)"},{"key":"38_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-662-44199-2_48","volume-title":"Mathematical Software \u2013 ICMS 2014","author":"F. Lonsing","year":"2014","unstructured":"Lonsing, F., Egly, U.: Incremental QBF Solving by DepQBF (Extended Abstract). In: Hong, H., Yap, C. (eds.) ICMS 2014. LNCS, vol.\u00a08592, pp. 307\u2013314. Springer, Heidelberg (2014)"},{"key":"38_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-642-39071-5_9","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"F. Lonsing","year":"2013","unstructured":"Lonsing, F., Egly, U., Van Gelder, A.: Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol.\u00a07962, pp. 100\u2013115. Springer, Heidelberg (2013)"},{"issue":"7","key":"38_CR25","doi-asserted-by":"publisher","first-page":"981","DOI":"10.1109\/TC.2010.74","volume":"59","author":"H. Mangassarian","year":"2010","unstructured":"Mangassarian, H., Veneris, A.G., Benedetti, M.: Robust QBF Encodings for Sequential Circuits with Applications to Verification, Debug, and Test. IEEE Trans. Computers\u00a059(7), 981\u2013994 (2010)","journal-title":"IEEE Trans. Computers"},{"key":"38_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/978-3-642-31612-8_41","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"P. Marin","year":"2012","unstructured":"Marin, P., Miller, C., Becker, B.: Incremental QBF Preprocessing for Partial Design Verification - (Poster Presentation). In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 473\u2013474. Springer, Heidelberg (2012)"},{"key":"38_CR27","doi-asserted-by":"crossref","unstructured":"Marin, P., Miller, C., Lewis, M.D.T., Becker, B.: Verification of Partial Designs using Incremental QBF Solving. In: Rosenstiel, W., Thiele, L. (eds.) DATE, pp. 623\u2013628. IEEE (2012)","DOI":"10.1109\/DATE.2012.6176547"},{"key":"38_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/978-3-642-31612-8_19","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"A. Nadel","year":"2012","unstructured":"Nadel, A., Ryvchin, V.: Efficient SAT Solving under Assumptions. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 242\u2013255. Springer, Heidelberg (2012)"},{"key":"38_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/978-3-642-31612-8_33","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"A. Niemetz","year":"2012","unstructured":"Niemetz, A., Preiner, M., Lonsing, F., Seidl, M., Biere, A.: Resolution-Based Certificate Extraction for QBF - (Tool Presentation). In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 430\u2013435. Springer, Heidelberg (2012)"},{"key":"38_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/11889205_37","volume-title":"Principles and Practice of Constraint Programming - CP 2006","author":"H. Samulowitz","year":"2006","unstructured":"Samulowitz, H., Davies, J., Bacchus, F.: Preprocessing QBF. In: Benhamou, F. (ed.) CP 2006. LNCS, vol.\u00a04204, pp. 514\u2013529. Springer, Heidelberg (2006)"},{"key":"38_CR31","doi-asserted-by":"crossref","unstructured":"Seidl, M., K\u00f6nighofer, R.: Partial witnesses from preprocessed quantified Boolean formulas. In: DATE, pp. 1\u20136. IEEE (2014)","DOI":"10.7873\/DATE2014.162"},{"key":"38_CR32","unstructured":"Silva, J.P.M., Lynce, I., Malik, S.: Conflict-Driven Clause Learning SAT Solvers. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, FAIA, vol.\u00a0185, pp. 131\u2013153. IOS Press (2009)"},{"key":"38_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-540-72788-0_34","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"S. Staber","year":"2007","unstructured":"Staber, S., Bloem, R.: Fault Localization and Correction with QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 355\u2013368. Springer, Heidelberg (2007)"},{"key":"38_CR34","doi-asserted-by":"crossref","unstructured":"S\u00fclflow, A., Fey, G., Drechsler, R.: Using QBF to Increase Accuracy of SAT-Based Debugging. In: ISCAS, pp. 641\u2013644. IEEE (2010)","DOI":"10.1109\/ISCAS.2010.5537506"},{"key":"38_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"694","DOI":"10.1007\/978-3-642-40627-0_51","volume-title":"Principles and Practice of Constraint Programming","author":"A. Gelder Van","year":"2013","unstructured":"Van Gelder, A.: Primal and Dual Encoding from Applications into Quantified Boolean Formulas. In: Schulte, C. (ed.) CP 2013. LNCS, vol.\u00a08124, pp. 694\u2013707. Springer, Heidelberg (2013)"},{"key":"38_CR36","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","Principles and Practice of Constraint Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10428-7_38","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T11:30:03Z","timestamp":1558956603000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10428-7_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319104270","9783319104287"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10428-7_38","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}