{"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":1750801203570,"version":"3.41.0"},"publisher-location":"Cham","reference-count":33,"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_17","type":"book-chapter","created":{"date-parts":[[2017,8,8]],"date-time":"2017-08-08T08:05:11Z","timestamp":1502179511000},"page":"263-280","source":"Crossref","is-referenced-by-count":10,"title":["Shortening QBF Proofs with Dependency Schemes"],"prefix":"10.1007","author":[{"given":"Joshua","family":"Blinkhorn","sequence":"first","affiliation":[]},{"given":"Olaf","family":"Beyersdorff","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,9]]},"reference":[{"issue":"1\u20134","key":"17_CR1","doi-asserted-by":"crossref","first-page":"133","DOI":"10.3233\/SAT190055","volume":"5","author":"M Benedetti","year":"2008","unstructured":"Benedetti, M., Mangassarian, H.: QBF-based formal verification: experience and perspectives. J. Satisfiability Boolean Model. Comput. (JSAT) 5(1\u20134), 133\u2013191 (2008)","journal-title":"J. Satisfiability Boolean Model. Comput. (JSAT)"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-319-44953-1_7","volume-title":"Principles and Practice of Constraint Programming","author":"O Beyersdorff","year":"2016","unstructured":"Beyersdorff, O., Blinkhorn, J.: Dependency schemes in QBF calculi: semantics and soundness. In: Rueher, M. (ed.) CP 2016. LNCS, vol. 9892, pp. 96\u2013112. Springer, Cham (2016). doi: 10.1007\/978-3-319-44953-1_7"},{"key":"17_CR3","unstructured":"Beyersdorff, O., Chew, L., Janota, M.: Proof complexity of resolution-based QBF calculi. In: International Symposium on Theoretical Aspects of Computer Science (STACS). Leibniz International Proceedings in Informatics (LIPIcs), vol. 30, pp. 76\u201389 (2015)"},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/978-3-662-47672-7_15","volume-title":"Automata, Languages, and Programming","author":"O Beyersdorff","year":"2015","unstructured":"Beyersdorff, O., Chew, L., Mahajan, M., Shukla, A.: Feasible interpolation for QBF resolution calculi. In: Halld\u00f3rsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9134, pp. 180\u2013192. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-47672-7_15"},{"key":"17_CR5","unstructured":"Beyersdorff, O., Chew, L., Mahajan, M., Shukla, A.: Are short proofs narrow? QBF resolution is not simple. In: Symposium on Theoretical Aspects of Computer Science (STACS), pp. 15:1\u201315:14 (2016)"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"486","DOI":"10.1007\/978-3-319-15579-1_38","volume-title":"Language and Automata Theory and Applications","author":"O Beyersdorff","year":"2015","unstructured":"Beyersdorff, O., Chew, L., Sreenivasaiah, K.: A game characterisation of tree-like Q-resolution size. In: Dediu, A.-H., Formenti, E., Mart\u00edn-Vide, C., Truthe, B. (eds.) LATA 2015. LNCS, vol. 8977, pp. 486\u2013498. Springer, Cham (2015). doi: 10.1007\/978-3-319-15579-1_38"},{"key":"17_CR7","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"},{"issue":"7","key":"17_CR8","doi-asserted-by":"crossref","first-page":"906","DOI":"10.1016\/j.apal.2011.09.009","volume":"163","author":"SR Buss","year":"2012","unstructured":"Buss, S.R.: Towards NP-P via proof complexity and search. Ann. Pure Appl. Logic 163(7), 906\u2013917 (2012)","journal-title":"Ann. Pure Appl. Logic"},{"key":"17_CR9","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511676277","volume-title":"Logical Foundations of Proof Complexity","author":"SA Cook","year":"2010","unstructured":"Cook, S.A., Nguyen, P.: Logical Foundations of Proof Complexity. Cambridge University Press, Cambridge (2010)"},{"issue":"1","key":"17_CR10","doi-asserted-by":"crossref","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"SA Cook","year":"1979","unstructured":"Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symbolic Logic 44(1), 36\u201350 (1979)","journal-title":"J. Symbolic Logic"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Egly, U., Kronegger, M., Lonsing, F., Pfandler, A.: Conformant planning as a case study of incremental QBF solving. In: Artificial Intelligence and Symbolic Computation (AISC 2014), pp. 120\u2013131 (2014)","DOI":"10.1007\/978-3-319-13770-4_11"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., Marin, P., Narizzano, M.: Reasoning with quantified boolean formulas. In: Handbook of Satisfiability, pp. 761\u2013780. IOS Press (2009)","DOI":"10.3233\/978-1-58603-929-5-761"},{"key":"17_CR13","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) 26, 371\u2013416 (2006)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"key":"17_CR14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.artint.2016.01.004","volume":"234","author":"M Janota","year":"2016","unstructured":"Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.M.: Solving QBF with counterexample guided refinement. J. Artif. Intell. 234, 1\u201325 (2016)","journal-title":"J. Artif. Intell."},{"issue":"1","key":"17_CR15","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":"17_CR16","unstructured":"Kontchakov, R., Pulina, L., Sattler, U., Schneider, T., Selmer, P., Wolter, F., Zakharyaschev, M.: Minimal module extraction from DL-lite ontologies using QBF solvers. In: International Joint Conference on Artificial Intelligence (IJCAI), pp. 836\u2013841. AAAI Press (2009)"},{"key":"17_CR17","volume-title":"Bounded Arithmetic, Propositional Logic, and Complexity Theory, Encyclopedia of Mathematics and Its Applications","author":"J Kraj\u00ed\u010dek","year":"1995","unstructured":"Kraj\u00ed\u010dek, J.: Bounded Arithmetic, Propositional Logic, and Complexity Theory, Encyclopedia of Mathematics and Its Applications, vol. 60. Cambridge University Press, Cambridge (1995)"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-319-26287-1_14","volume-title":"Hardware and Software: Verification and Testing","author":"JH Liang","year":"2015","unstructured":"Liang, J.H., Ganesh, V., Zulkoski, E., Zaman, A., Czarnecki, K.: Understanding VSIDS branching heuristics in conflict-driven clause-learning SAT solvers. In: Piterman, N. (ed.) HVC 2015. LNCS, vol. 9434, pp. 225\u2013241. Springer, Cham (2015). doi: 10.1007\/978-3-319-26287-1_14"},{"key":"17_CR19","unstructured":"Lonsing, F.: Dependency schemes and search-based QBF solving: theory and practice. Ph.D. thesis, Johannes Kepler University (2012)"},{"key":"17_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/978-3-319-40970-2_27","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"F Lonsing","year":"2016","unstructured":"Lonsing, F., Egly, U., Seidl, M.: Q-resolution with generalized axioms. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 435\u2013452. Springer, Cham (2016). doi: 10.1007\/978-3-319-40970-2_27"},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of Design Automation Conference (DAC), pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"17_CR22","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":"17_CR23","unstructured":"Rintanen, J.: Asymptotically optimal encodings of conformant planning in QBF. In: National Conference on Artificial Intelligence (AAAI), pp. 1045\u20131050. AAAI Press (2007)"},{"issue":"1","key":"17_CR24","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. Reasoning 42(1), 77\u201397 (2009)","journal-title":"J. Autom. Reasoning"},{"key":"17_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"578","DOI":"10.1007\/11564751_43","volume-title":"Principles and Practice of Constraint Programming - CP 2005","author":"H Samulowitz","year":"2005","unstructured":"Samulowitz, H., Bacchus, F.: Using SAT in QBF. In: Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 578\u2013592. Springer, Heidelberg (2005). doi: 10.1007\/11564751_43"},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"Shacham, O., Zarpas, E.: Tuning the VSIDS decision heuristic for bounded model checking. In: International Workshop on Microprocessor Test and Verification (MTV), p. 75 (2003)","DOI":"10.1109\/MTV.2003.1250266"},{"key":"17_CR27","doi-asserted-by":"crossref","unstructured":"Silva, J.P.M.: The impact of branching heuristics in propositional satisfiability algorithms. In: Portugese Conference on Progress in Artificial Intelligence (EPIA), pp. 62\u201374 (1999)","DOI":"10.1007\/3-540-48159-1_5"},{"key":"17_CR28","doi-asserted-by":"crossref","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP - a new search algorithm for satisfiability. In: International Conference on Computer-Aided Design (ICCAD), pp. 220\u2013227 (1996)","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"17_CR29","unstructured":"Slivovsky, F.: Structure in $$\\#$$ SAT and QBF. Ph.D. thesis, Vienna University of Technology (2015)"},{"key":"17_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-319-09284-3_21","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"F Slivovsky","year":"2014","unstructured":"Slivovsky, F., Szeider, S.: Variable dependencies and Q-resolution. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 269\u2013284. Springer, Cham (2014). doi: 10.1007\/978-3-319-09284-3_21"},{"key":"17_CR31","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. TCS 612, 83\u2013101 (2016)","journal-title":"TCS"},{"key":"17_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 Van","year":"2011","unstructured":"Van 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"},{"key":"17_CR33","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: Conflict driven learning in a quantified boolean satisfiability solver. In: International Conference on Computer-aided Design (ICCAD), pp. 442\u2013449 (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_17","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_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319662626","9783319662633"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66263-3_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}