{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T17:08:04Z","timestamp":1743095284440,"version":"3.40.3"},"publisher-location":"Cham","reference-count":52,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030802226"},{"type":"electronic","value":"9783030802233"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-80223-3_34","type":"book-chapter","created":{"date-parts":[[2021,7,1]],"date-time":"2021-07-01T14:13:49Z","timestamp":1625148829000},"page":"499-517","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Certified DQBF Solving by Definition Extraction"],"prefix":"10.1007","author":[{"given":"Franz-Xaver","family":"Reichl","sequence":"first","affiliation":[]},{"given":"Friedrich","family":"Slivovsky","sequence":"additional","affiliation":[]},{"given":"Stefan","family":"Szeider","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,2]]},"reference":[{"key":"34_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-319-96145-3_14","volume-title":"Computer Aided Verification","author":"S Akshay","year":"2018","unstructured":"Akshay, S., Chakraborty, S., Goel, S., Kulal, S., Shah, S.: What\u2019s hard about boolean functional synthesis? In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 251\u2013269. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_14"},{"key":"34_CR2","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Boutilier, C. (ed.) IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, pp. 399\u2013404 (2009)"},{"key":"34_CR3","doi-asserted-by":"publisher","first-page":"957","DOI":"10.1016\/S0898-1221(00)00333-3","volume":"41","author":"S Azhar","year":"2001","unstructured":"Azhar, S., Peterson, G., Reif, J.: Lower bounds for multiplayer non-cooperative games of incomplete information. J. Comput. Math. Appl. 41, 957\u2013992 (2001)","journal-title":"J. Comput. Math. Appl."},{"key":"34_CR4","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1016\/j.tcs.2013.12.020","volume":"523","author":"V Balabanov","year":"2014","unstructured":"Balabanov, V., Chiang, H.K., Jiang, J.R.: Henkin quantifiers and boolean formulae: a certification perspective of DQBF. Theor. Comput. Sci. 523, 86\u2013100 (2014)","journal-title":"Theor. Comput. Sci."},{"key":"34_CR5","doi-asserted-by":"crossref","unstructured":"Baldoni, R., Coppa, E., D\u2019Elia, D.C., Demetrescu, C., Finocchi, I.: A survey of symbolic execution techniques. ACM Comput. Surv. 51(3), 50:1\u201350:39 (2018)","DOI":"10.1145\/3182657"},{"issue":"3","key":"34_CR6","doi-asserted-by":"publisher","first-page":"597","DOI":"10.1007\/s10817-018-9482-4","volume":"63","author":"O Beyersdorff","year":"2019","unstructured":"Beyersdorff, O., Blinkhorn, J., Chew, L., Schmidt, R.A., Suda, M.: Reinterpreting dependency schemes: soundness meets incompleteness in DQBF. J. Autom. Reason. 63(3), 597\u2013623 (2019)","journal-title":"J. Autom. Reason."},{"key":"34_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14"},{"key":"34_CR8","unstructured":"Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In: Balyo, T., Froleyks, N., Heule, M., Iser, M., J\u00e4rvisalo, M., Suda, M. (eds.) Proceedings of SAT Competition 2020 - Solver and Benchmark Descriptions. Department of Computer Science Report Series B, vol. B-2020-1, pp. 51\u201353. University of Helsinki (2020)"},{"key":"34_CR9","unstructured":"Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond. Tech. Rep. 11\/2, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria (2011)"},{"key":"34_CR10","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. 8318, pp. 1\u201320. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54013-4_1"},{"key":"34_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/11814948_21","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"U Bubeck","year":"2006","unstructured":"Bubeck, U., B\u00fcning, H.K.: Dependency quantified horn formulas: models and complexity. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 198\u2013211. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814948_21"},{"key":"34_CR12","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. 2919, pp. 502\u2013518. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37"},{"key":"34_CR13","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). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_20"},{"key":"34_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-319-09284-3_19","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"B Finkbeiner","year":"2014","unstructured":"Finkbeiner, B., Tentrup, L.: Fast DQBF refutation. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 243\u2013251. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_19"},{"key":"34_CR15","unstructured":"Fr\u00f6hlich, A., Kov\u00e1sznai, G., Biere, A.: A DPLL algorithm for solving DQBF (2012). http:\/\/fmv.jku.at\/papers\/FroehlichKovasznaiBiere-POS12.pdf, presented at Workshop on Pragmatics of SAT (POS)"},{"key":"34_CR16","unstructured":"Fr\u00f6hlich, A., Kov\u00e1sznai, G., Biere, A., Veith, H.: idq: instantiation-based DQBF solving. In: Berre, D.L. (ed.) POS-14. Fifth Pragmatics of SAT workshop, a workshop of the SAT 2014 conference, part of FLoC 2014 during the Vienna Summer of Logic,Vienna, Austria, 13 July 2014. EPiC Series in Computing, vol. 27, pp. 103\u2013116. EasyChair (2014)"},{"key":"34_CR17","doi-asserted-by":"crossref","unstructured":"Ganian, R., Peitl, T., Slivovsky, F., Szeider, S.: Fixed-parameter tractability of dependency QBF with structural parameters. In: Calvanese, D., Erdem, E., Thielscher, M. (eds.) Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, KR 2020, pp. 392\u2013402 (2020)","DOI":"10.24963\/kr.2020\/40"},{"key":"34_CR18","doi-asserted-by":"crossref","unstructured":"Ge-Ernst, A., Scholl, C., Wimmer, R.: Localizing quantifiers for DQBF. In: Barrett, C.W., Yang, J. (eds.) Formal Methods in Computer Aided Design, FMCAD 2019, pp. 184\u2013192. IEEE (2019)","DOI":"10.23919\/FMCAD.2019.8894269"},{"key":"34_CR19","doi-asserted-by":"crossref","unstructured":"Gitina, K., Reimer, S., Sauer, M., Wimmer, R., Scholl, C., Becker, B.: Equivalence checking of partial designs using dependency quantified boolean formulae. In: IEEE 31st International Conference on Computer Design, ICCD 2013, pp. 396\u2013403. IEEE Computer Society (2013)","DOI":"10.1109\/ICCD.2013.6657071"},{"key":"34_CR20","doi-asserted-by":"crossref","unstructured":"Gitina, K., Wimmer, R., Reimer, S., Sauer, M., Scholl, C., Becker, B.: Solving DQBF through quantifier elimination. In: Nebel, W., Atienza, D. (eds.) Proceedings of the 2015 Design, Automation & Test in Europe Conference & Exhibition, DATE 2015, pp. 1617\u20131622. ACM (2015)","DOI":"10.7873\/DATE.2015.0098"},{"key":"34_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"611","DOI":"10.1007\/978-3-030-53291-8_31","volume-title":"Computer Aided Verification","author":"P Golia","year":"2020","unstructured":"Golia, P., Roy, S., Meel, K.S.: Manthan: a data-driven approach for boolean function synthesis. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 611\u2013633. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_31"},{"key":"34_CR22","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., Vizel, Y.: Druping for interpolates. In: FMCAD 2014, pp. 99\u2013106. IEEE (2014)","DOI":"10.1109\/FMCAD.2014.6987601"},{"issue":"1","key":"34_CR23","first-page":"133","volume":"11","author":"MJH Heule","year":"2019","unstructured":"Heule, M.J.H., J\u00e4rvisalo, M., Suda, M.: SAT competition 2018. J. Satisf. Boolean Model. Comput. 11(1), 133\u2013154 (2019)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"34_CR24","doi-asserted-by":"crossref","unstructured":"Ignatiev, A., Morgado, A., Marques-Silva, J.: PySAT: a python toolkit for prototyping with SAT oracles. In: SAT, pp. 428\u2013437 (2018)","DOI":"10.1007\/978-3-319-94144-8_26"},{"key":"34_CR25","doi-asserted-by":"crossref","unstructured":"Janota, M.: Towards generalization in QBF solving via machine learning. In: McIlraith, S.A., Weinberger, K.Q. (eds.) Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18), pp. 6607\u20136614. AAAI Press (2018)","DOI":"10.1609\/aaai.v32i1.12208"},{"key":"34_CR26","doi-asserted-by":"publisher","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. Artif. Intell. 234, 1\u201325 (2016)","journal-title":"Artif. Intell."},{"key":"34_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-642-39071-5_7","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"M Janota","year":"2013","unstructured":"Janota, M., Marques-Silva, J.: On propositional QBF expansions and Q-resolution. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 67\u201382. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39071-5_7"},{"issue":"7","key":"34_CR28","doi-asserted-by":"publisher","first-page":"693","DOI":"10.1007\/s00236-017-0294-5","volume":"54","author":"S Jha","year":"2017","unstructured":"Jha, S., Seshia, S.A.: A theory of formal synthesis via inductive learning. Acta Informatica 54(7), 693\u2013726 (2017)","journal-title":"Acta Informatica"},{"key":"34_CR29","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-540-71070-7_24","volume-title":"Automated Reasoning","author":"K Korovin","year":"2008","unstructured":"Korovin, K.: iProver \u2013 an instantiation-based theorem prover for first-order logic (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 292\u2013298. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_24"},{"key":"34_CR30","doi-asserted-by":"crossref","unstructured":"Kullmann, O., Shukla, A.: Autarkies for DQCNF. In: Barrett, C.W., Yang, J. (eds.) 2019 Formal Methods in Computer Aided Design, FMCAD 2019, pp. 179\u2013183. IEEE (2019)","DOI":"10.23919\/FMCAD.2019.8894263"},{"key":"34_CR31","unstructured":"Meel, K.S., et al.: Constrained sampling and counting: Universal hashing meets SAT solving. In: Darwiche, A. (ed.) Beyond NP, Papers from the 2016 AAAI Workshop. AAAI Workshops, vol. WS-16-05. AAAI Press (2016)"},{"key":"34_CR32","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. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 430\u2013435. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_33"},{"key":"34_CR33","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1016\/j.artint.2019.04.002","volume":"274","author":"L Pulina","year":"2019","unstructured":"Pulina, L., Seidl, M.: The 2016 and 2017 QBF solvers evaluations (qbfeval\u201916 and qbfeval\u201917). Artif. Intell. 274, 224\u2013248 (2019)","journal-title":"Artif. Intell."},{"key":"34_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/978-3-319-66263-3_20","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2017","author":"MN Rabe","year":"2017","unstructured":"Rabe, M.N.: A resolution-style proof system for DQBF. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 314\u2013325. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66263-3_20"},{"key":"34_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/978-3-319-40970-2_23","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"MN Rabe","year":"2016","unstructured":"Rabe, M.N., Seshia, S.A.: Incremental determinization. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 375\u2013392. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_23"},{"issue":"4","key":"34_CR36","first-page":"139","volume":"7","author":"O Roussel","year":"2011","unstructured":"Roussel, O.: Controlling a solver execution with the runsolver tool. J. Satisf. Boolean Model. Comput. 7(4), 139\u2013144 (2011)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"34_CR37","doi-asserted-by":"crossref","unstructured":"Scholl, C., Becker, B.: Checking equivalence for partial implementations. In: Proceedings of the 38th Design Automation Conference, DAC 2001, pp. 238\u2013243. ACM (2001)","DOI":"10.1145\/378239.378471"},{"key":"34_CR38","doi-asserted-by":"crossref","unstructured":"Scholl, C., Jiang, J.R., Wimmer, R., Ge-Ernst, A.: A PSPACE subclass of dependency quantified boolean formulas and its effective solving. In: The Thirty-Third AAAI Conference on Artificial Intelligence, AAAI 2019, pp. 1584\u20131591. AAAI Press (2019)","DOI":"10.1609\/aaai.v33i01.33011584"},{"key":"34_CR39","unstructured":"S\u00ed\u010d, J.: Satisfiability of DQBF using binary decision diagrams. Master\u2019s thesis, Masaryk University, Brno, Czech Republic (2020)"},{"key":"34_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"508","DOI":"10.1007\/978-3-030-53288-8_24","volume-title":"Computer Aided Verification","author":"F Slivovsky","year":"2020","unstructured":"Slivovsky, F.: Interpolation-based semantic gate extraction and its applications to QBF preprocessing. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 508\u2013528. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_24"},{"key":"34_CR41","doi-asserted-by":"publisher","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. Theor. Comput. Sci. 612, 83\u2013101 (2016)","journal-title":"Theor. Comput. Sci."},{"key":"34_CR42","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Jones, C.G., Bod\u00edk, R.: Sketching concurrent data structures. In: Gupta, R., Amarasinghe, S.P. (eds.) Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, pp. 136\u2013148. ACM (2008)","DOI":"10.1145\/1379022.1375599"},{"key":"34_CR43","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Tancau, L., Bod\u00edk, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: Shen, J.P., Martonosi, M. (eds.) Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2006, pp. 404\u2013415. ACM (2006)","DOI":"10.1145\/1168857.1168907"},{"key":"34_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-642-02777-2_24","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"M Soos","year":"2009","unstructured":"Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 244\u2013257. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02777-2_24"},{"key":"34_CR45","doi-asserted-by":"crossref","unstructured":"Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time: Preliminary report. In: Aho, A.V., et al. (eds.) Proceedings of the 5th Annual ACM Symposium on Theory of Computing, Austin, Texas, USA, 30 April\u20132 May 1973, pp. 1\u20139. ACM (1973)","DOI":"10.1145\/800125.804029"},{"issue":"1","key":"34_CR46","first-page":"155","volume":"11","author":"L Tentrup","year":"2019","unstructured":"Tentrup, L.: CAQE and quabs: Abstraction based QBF solvers. J. Satisf. Boolean Model. Comput. 11(1), 155\u2013210 (2019)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"34_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/978-3-030-24258-9_27","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2019","author":"L Tentrup","year":"2019","unstructured":"Tentrup, L., Rabe, M.N.: Clausal abstraction for DQBF. In: Janota, M., Lynce, I. (eds.) SAT 2019. LNCS, vol. 11628, pp. 388\u2013405. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-24258-9_27"},{"key":"34_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"641","DOI":"10.1007\/978-3-319-21690-4_43","volume-title":"Computer Aided Verification","author":"Y Vizel","year":"2015","unstructured":"Vizel, Y., Gurfinkel, A., Malik, S.: Fast interpolating BMC. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 641\u2013657. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_43"},{"issue":"11","key":"34_CR49","doi-asserted-by":"publisher","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":"34_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-319-66263-3_21","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2017","author":"R Wimmer","year":"2017","unstructured":"Wimmer, R., Karrenbauer, A., Becker, R., Scholl, C., Becker, B.: From DQBF to QBF by dependency elimination. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 326\u2013343. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66263-3_21"},{"issue":"1","key":"34_CR51","first-page":"3","volume":"11","author":"R Wimmer","year":"2019","unstructured":"Wimmer, R., Scholl, C., Becker, B.: The (D)QBF preprocessor hqspre - underlying theory and its implementation. J. Satisf. Boolean Model. Comput. 11(1), 3\u201352 (2019)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"34_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/978-3-319-40970-2_29","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"R Wimmer","year":"2016","unstructured":"Wimmer, R., Scholl, C., Wimmer, K., Becker, B.: Dependency schemes for DQBF. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 473\u2013489. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_29"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2021"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-80223-3_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,3]],"date-time":"2024-09-03T03:16:22Z","timestamp":1725333382000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-80223-3_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030802226","9783030802233"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-80223-3_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"2 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAT","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Theory and Applications of Satisfiability Testing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Barcelona","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sat2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.iiia.csic.es\/sat2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}