{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T21:40:03Z","timestamp":1750801203437,"version":"3.41.0"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319662626"},{"type":"electronic","value":"9783319662633"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-66263-3_19","type":"book-chapter","created":{"date-parts":[[2017,8,8]],"date-time":"2017-08-08T08:05:11Z","timestamp":1502179511000},"page":"298-313","source":"Crossref","is-referenced-by-count":18,"title":["Dependency Learning for QBF"],"prefix":"10.1007","author":[{"given":"Tom\u00e1\u0161","family":"Peitl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Friedrich","family":"Slivovsky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Szeider","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,8,9]]},"reference":[{"issue":"1","key":"19_CR1","doi-asserted-by":"crossref","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 Syst. Des. 41(1), 45\u201365 (2012)","journal-title":"Formal Methods Syst. Des."},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Balabanov, V., Jiang, J.R., Janota, M., Widl, M.: Efficient extraction of QBF (counter)models from long-distance resolution proofs. In: Bonet, B., Koenig, S. (eds.) Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, Austin, Texas, USA, 25\u201330 January 2015, pp. 3694\u20133701. AAAI Press (2015)","DOI":"10.1609\/aaai.v29i1.9750"},{"key":"19_CR3","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. 3542, pp. 59\u201370. Springer, Heidelberg (2005). doi: 10.1007\/11527695_5"},{"key":"19_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-642-02777-2_37","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"F Lonsing","year":"2009","unstructured":"Lonsing, F., Biere, A.: A compact representation for syntactic dependencies in QBFs. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 398\u2013411. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-02777-2_37"},{"key":"19_CR5","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. 6175, pp. 158\u2013171. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14186-7_14"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-3-642-22438-6_10","volume-title":"Automated Deduction \u2013 CADE-23","author":"A Biere","year":"2011","unstructured":"Biere, A., Lonsing, F., Seidl, M.: Blocked clause elimination for QBF. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 101\u2013115. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22438-6_10"},{"issue":"2","key":"19_CR7","doi-asserted-by":"crossref","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. Reason. 28(2), 101\u2013142 (2002)","journal-title":"J. Autom. Reason."},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-642-45221-5_21","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"U Egly","year":"2013","unstructured":"Egly, U., Lonsing, F., Widl, M.: Long-distance resolution: proof generation and strategy extraction in search-based QBF solving. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 291\u2013308. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-45221-5_21"},{"key":"19_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-662-54577-5_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Faymonville","year":"2017","unstructured":"Faymonville, P., Finkbeiner, B., Rabe, M.N., Tentrup, L.: Encodings of bounded synthesis. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 354\u2013370. Springer, Heidelberg (2017). doi: 10.1007\/978-3-662-54577-5_20"},{"key":"19_CR10","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. 26, 371\u2013416 (2006)","journal-title":"J. Artif. Intell. Res."},{"key":"19_CR11","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. 7962, pp. 83\u201399. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39071-5_8"},{"key":"19_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-319-40970-2_15","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"MJH Heule","year":"2016","unstructured":"Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the boolean pythagorean triples problem via cube-and-conquer. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 228\u2013245. Springer, Cham (2016). doi: 10.1007\/978-3-319-40970-2_15"},{"key":"19_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/978-3-319-40970-2_25","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"M Janota","year":"2016","unstructured":"Janota, M.: On Q-resolution and CDCL QBF solving. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 402\u2013418. Springer, Cham (2016). doi: 10.1007\/978-3-319-40970-2_25"},{"key":"19_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-642-31612-8_10","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"M Janota","year":"2012","unstructured":"Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.: Solving QBF with counterexample guided refinement. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 114\u2013128. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31612-8_10"},{"key":"19_CR15","unstructured":"Janota, M., Marques-Silva, J.: Solving QBF by clause selection. In: Yang, Q., Wooldridge, M. (eds.) Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, pp. 325\u2013331. AAAI Press (2015)"},{"key":"19_CR16","unstructured":"Jordan, C., Klieber, W., Seidl, M.: Non-cnf QBF solving with QCIR. In: Darwiche, A. (ed.) Beyond NP, Papers from the 2016 AAAI Workshop. AAAI Workshops, vol. WS-16-05. AAAI Press (2016)"},{"issue":"1","key":"19_CR17","doi-asserted-by":"crossref","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. 117(1), 12\u201318 (1995)","journal-title":"Inf. Comput."},{"key":"19_CR18","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.: A non-prenex, non-clausal QBF solver with game-state learning. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 128\u2013142. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14186-7_12"},{"key":"19_CR19","unstructured":"Lonsing, F., Schemes, D., Solving, Search-Based QBF: Theory and Practice. PhD thesis, Johannes Kepler University, Linz, Austria, April 2012"},{"key":"19_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"418","DOI":"10.1007\/978-3-662-48899-7_29","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"F Lonsing","year":"2015","unstructured":"Lonsing, F., Bacchus, F., Biere, A., Egly, U., Seidl, M.: Enhancing search-based QBF solving by dynamic blocked clause elimination. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 418\u2013433. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-48899-7_29"},{"key":"19_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-540-79719-7_19","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2008","author":"F Lonsing","year":"2008","unstructured":"Lonsing, F., Biere, A.: Nenofex: expanding NNF for QBF solving. In: Kleine B\u00fcning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 196\u2013210. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-79719-7_19"},{"issue":"8","key":"19_CR22","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1145\/1536616.1536637","volume":"52","author":"S Malik","year":"2009","unstructured":"Malik, S., Zhang, L.: Boolean satisfiability from theoretical hardness to practical success. Commun. ACM 52(8), 76\u201382 (2009)","journal-title":"Commun. ACM"},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning sat solvers. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, pp. 131\u2013153. IOS Press (2009)","DOI":"10.3233\/978-1-58603-929-5-131"},{"key":"19_CR24","unstructured":"Meel, K.S., Vardi, M.Y., Chakraborty, S., Fremont, D.J., Seshia, S.A., Fried, D., Ivrii, A., Malik, S.: Constrained sampling and counting: universal hashing meets SAT solving. In Darwiche, A. (ed.) Beyond NP, Papers from the 2016 AAAI Workshop, Phoenix, Arizona, USA. AAAI Workshops, February 12, 2016, vol. WS-16-05. AAAI Press (2016)"},{"key":"19_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/978-3-319-40970-2_31","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"T Peitl","year":"2016","unstructured":"Peitl, T., Slivovsky, F., Szeider, S.: Long distance Q-resolution with dependency schemes. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 500\u2013518. Springer, Cham (2016). doi: 10.1007\/978-3-319-40970-2_31"},{"key":"19_CR26","unstructured":"Pulina, L.: The ninth QBF solvers evaluation - preliminary report. In: Lonsing, F., Seidl, M. (eds.) Proceedings of the 4th International Workshop on Quantified Boolean Formulas (QBF 2016). CEUR Workshop Proceedings, vol. 1719, pp. 1\u201313. CEUR-WS.org (2016)"},{"key":"19_CR27","doi-asserted-by":"crossref","unstructured":"Rabe, M.N., Tentrup, L.: CAQE: a certifying QBF solver. In: Kaivola, R., Wahl, T. (eds.) Formal Methods in Computer-Aided Design - FMCAD 2015, pp. 136\u2013143. IEEE Computer Soc. (2015)","DOI":"10.1109\/FMCAD.2015.7542263"},{"issue":"1","key":"19_CR28","doi-asserted-by":"crossref","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. J. Autom. Reason. 42(1), 77\u201397 (2009)","journal-title":"J. Autom. Reason."},{"key":"19_CR29","unstructured":"Scholl, C., Pigorsch, F.: The QBF solver AIGSolve. In: Lonsing, F., Seidl, M. (eds.) Proceedings of the 4th International Workshop on Quantified Boolean Formulas (QBF 2016). CEUR Workshop Proceedings, vol. 1719, pp. 55\u201362. CEUR-WS.org (2016)"},{"key":"19_CR30","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/j.tcs.2015.10.020","volume":"612","author":"F Slivovsky","year":"2016","unstructured":"Slivovsky, F., Szeider, S.: Soundness of Q-resolution with dependency schemes. Theoret. Comput. Sci. 612, 83\u2013101 (2016)","journal-title":"Theoret. Comput. Sci."},{"key":"19_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/978-3-319-40970-2_24","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"L Tentrup","year":"2016","unstructured":"Tentrup, L.: Non-prenex QBF solving using abstraction. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 393\u2013401. Springer, Cham (2016). doi: 10.1007\/978-3-319-40970-2_24"},{"key":"19_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"789","DOI":"10.1007\/978-3-642-23786-7_59","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2011","author":"A Gelder","year":"2011","unstructured":"Gelder, A.: Variable independence and resolution paths for quantified boolean formulas. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 789\u2013803. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-23786-7_59"},{"issue":"11","key":"19_CR33","doi-asserted-by":"crossref","first-page":"2021","DOI":"10.1109\/JPROC.2015.2455034","volume":"103","author":"Y Vizel","year":"2015","unstructured":"Vizel, Y., Weissenbacher, G., Malik, S.: Boolean satisfiability solvers and their applications in model checking. Proc. IEEE 103(11), 2021\u20132035 (2015)","journal-title":"Proc. IEEE"},{"key":"19_CR34","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: Conflict driven learning in a quantified Boolean satisfiability solver. In: Pileggi, L.T., Kuehlmann, A. (eds.) Proceedings of the 2002 IEEE\/ACM International Conference on Computer-Aided Design, ICCAD 2002, San Jose, California, USA, 10\u201314 November 2002, pp. 442\u2013449. ACM\/IEEE Computer Society (2002)","DOI":"10.1145\/774572.774637"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2017"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66263-3_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T20:59:54Z","timestamp":1750798794000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66263-3_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319662626","9783319662633"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66263-3_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}