{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,20]],"date-time":"2026-07-20T19:04:27Z","timestamp":1784574267762,"version":"3.55.0"},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2016,11,5]],"date-time":"2016-11-05T00:00:00Z","timestamp":1478304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,11,5]],"date-time":"2016-11-05T00:00:00Z","timestamp":1478304000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["1618574"],"award-info":[{"award-number":["1618574"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006602","name":"Air Force Research Laboratory","doi-asserted-by":"publisher","award":["FA8750-15-2-0096"],"award-info":[{"award-number":["FA8750-15-2-0096"]}],"id":[{"id":"10.13039\/100006602","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["S11408-N23"],"award-info":[{"award-number":["S11408-N23"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["S11408-N23"],"award-info":[{"award-number":["S11408-N23"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001821","name":"Vienna Science and Technology Fund","doi-asserted-by":"publisher","award":["ICT10-018"],"award-info":[{"award-number":["ICT10-018"]}],"id":[{"id":"10.13039\/501100001821","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2017,1]]},"DOI":"10.1007\/s10817-016-9390-4","type":"journal-article","created":{"date-parts":[[2016,11,5]],"date-time":"2016-11-05T05:32:07Z","timestamp":1478323927000},"page":"97-125","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Solution Validation and Extraction for QBF Preprocessing"],"prefix":"10.1007","volume":"58","author":[{"given":"Marijn J. H.","family":"Heule","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Martina","family":"Seidl","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,11,5]]},"reference":[{"key":"9390_CR1","doi-asserted-by":"crossref","unstructured":"Ayari ,A., Basin, D.A.: QUBOS: Deciding quantified Boolean logic using propositional satisfiability solvers. In: Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2002), Springer, LNCS, vol. 2517, pp. 187\u2013201 (2002)","DOI":"10.1007\/3-540-36126-X_12"},{"key":"9390_CR2","doi-asserted-by":"crossref","unstructured":"Balabanov, V., Jiang, J.R.: Resolution Proofs and Skolem Functions in QBF Evaluation and Applications. In: Proceedings of the 23rd Conference on Computer Aided Verification (CAV 2011), Springer, LNCS, vol. 6806, pp. 149\u2013164 (2011)","DOI":"10.1007\/978-3-642-22110-1_12"},{"issue":"1","key":"9390_CR3","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 Syst. Design 41(1), 45\u201365 (2012)","journal-title":"Formal Methods Syst. Design"},{"key":"9390_CR4","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: Proceedings of the 29th Conference on Artificial Intelligence (AAAI 2015), pp. 3694\u20133701. AAAI Press (2015)","DOI":"10.1609\/aaai.v29i1.9750"},{"key":"9390_CR5","unstructured":"Benedetti, M.: Extracting certificates from quantified Boolean formulas. In: Proceedings of the 19th International Joint Conference on Artificial Intelligence (IJCAI 2005), Professional Book Center, pp. 47\u201353 (2005)"},{"key":"9390_CR6","doi-asserted-by":"crossref","unstructured":"Benedetti, M.: sKizzo: a suite to evaluate and certify QBFs. In: Proceedings of the 20th International Conference on Automated Deduction (CADE 2005), LNCS, vol. 3632, pp. 369\u2013376. Springer, Berlin (2005)","DOI":"10.1007\/11532231_27"},{"issue":"1\u20134","key":"9390_CR7","first-page":"133","volume":"5","author":"M Benedetti","year":"2008","unstructured":"Benedetti, M., Mangassarian, H.: QBF-based formal verification: experience and perspectives. J. Satisf. Boolean Model. Comput. 5(1\u20134), 133\u2013191 (2008)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"9390_CR8","doi-asserted-by":"crossref","unstructured":"Biere, A.: Resolve and expand. In: Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing (SAT 2004), LNCS, vol. 3542, pp. 59\u201370. Springer, Berlin (2005)","DOI":"10.1007\/11527695_5"},{"key":"9390_CR9","unstructured":"Biere, A.: Lingeling, Plingeling and Treengeling entering the SAT competition 2013. In: Proceedings of SAT Competition 2013 (2013)"},{"key":"9390_CR10","doi-asserted-by":"crossref","unstructured":"Biere, A., Lonsing, F., Seidl, M.: Blocked clause elimination for QBF. In: Proceedings of the 23th International Conference on Automated Deduction (CADE 2011), LNCS, vol. 6803, pp. 101\u2013115. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22438-6_10"},{"key":"9390_CR11","doi-asserted-by":"crossref","unstructured":"Bloem, R., K\u00f6nighofer, R., Seidl, M.: SAT-based synthesis methods for safety specs. In: Proceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2014), LNCS, vol. 8318, pp. 1\u201320. Springer, Berlin (2014)","DOI":"10.1007\/978-3-642-54013-4_1"},{"key":"9390_CR12","doi-asserted-by":"crossref","unstructured":"Bubeck, U., Kleine B\u00fcning, H.: Bounded universal expansion for preprocessing QBF. In: Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing (SAT 2007), LNCS, vol. 4501, pp. 244\u2013257. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-72788-0_24"},{"key":"9390_CR13","unstructured":"Cadoli, M., Giovanardi, A., Schaerf, M.: An algorithm to evaluate quantified Boolean formulae. In: Proceedings of the 15th National Conference on Artificial Intelligence and 10th Innovative Applications of Artificial Intelligence Conference, (AAAI 98\/IAAI 98), pp. 262\u2013267. AAAI Press\/The MIT Press, Cambridge (1998)"},{"issue":"3","key":"9390_CR14","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201\u2013215 (1960)","journal-title":"J. ACM"},{"key":"9390_CR15","doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., Marin, P., Narizzano, M.: sQueezeBF: an effective preprocessor for QBFs based on equivalence reasoning. In: Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing (SAT 2010), LNCS, vol. 6175, pp. 85\u201398. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-14186-7_9"},{"key":"9390_CR16","unstructured":"Goldberg, E.I., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: Proceedings of the Design, Automation and Test in Europe Conference and Exposition (DATE 2003), IEEE, pp. 10886\u201310891 (2003)"},{"key":"9390_CR17","doi-asserted-by":"crossref","unstructured":"Heule, M., J\u00e4rvisalo, M., Biere, A.: Covered clause elimination. In: Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2013), EasyChair Proceedings in Computing, vol.\u00a013, pp. 41\u201346 (2013)","DOI":"10.29007\/cl8s"},{"key":"9390_CR18","doi-asserted-by":"crossref","unstructured":"Heule, M., Seidl, M., Biere, A.: Efficient extraction of Skolem functions from QRAT proofs. In: Proceedings of the 17th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2014), IEEE, pp. 107\u2013114 (2014)","DOI":"10.1109\/FMCAD.2014.6987602"},{"key":"9390_CR19","doi-asserted-by":"crossref","unstructured":"Heule, M., Seidl, M., Biere, A.: A unified proof system for QBF preprocessing. In: Proceedings of the 7th Internatioanl Joint Conference on Automated Reasoning (IJCAR 2014), LNCS, vol. 8562, pp. 91\u2013106. Springer, Berlin (2014)","DOI":"10.1007\/978-3-319-08587-6_7"},{"key":"9390_CR20","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1613\/jair.4694","volume":"53","author":"M Heule","year":"2015","unstructured":"Heule, M., J\u00e4rvisalo, M., Lonsing, F., Seidl, M., Biere, A.: Clause elimination for SAT and QSAT. J. Artif. Intel. Res. 53, 127\u2013168 (2015a)","journal-title":"J. Artif. Intel. Res."},{"key":"9390_CR21","doi-asserted-by":"crossref","unstructured":"Heule, M., Jr WAH, Wetzler, N.: Expressing symmetry breaking in DRAT proofs. In: Proceedings of the 25th International Conference on Automated Deduction (CADE 2015), LNCS, vol. 9195, pp. 591\u2013606. Springer, Berlin (2015)","DOI":"10.1007\/978-3-319-21401-6_40"},{"key":"9390_CR22","doi-asserted-by":"crossref","unstructured":"Heule, M., Seidl, M., Biere, A.: Blocked literals are universal. In: Proceedings of the 7th Internatonal Symposium on NASA Formal Methods (NFM 2015), LNCS, vol. 9058, pp. 436\u2013442. Springer, Berlin (2015)","DOI":"10.1007\/978-3-319-17524-9_33"},{"key":"9390_CR23","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., J\u00e4rvisalo, M., Biere, A.: Clause elimination procedures for CNF formulas. In: Proceedings\u00a014th International\u00a0Conference\u00a0on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2010), LNCS, vol. 6397, pp. 357\u2013371. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-16242-8_26"},{"key":"9390_CR24","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Hunt, W.A., Wetzler, N.: Verifying refutations with extended resolution. In: Proceedings of the 24th International Conference on Automated Deduction (CADE 2013), LNAI, vol. 7898, pp. 345\u2013359. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-38574-2_24"},{"key":"9390_CR25","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Hunt, Jr W.A., Wetzler, N.: Trimming while checking clausal proofs. In: Proceedings of the 16th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2013), IEEE, pp. 181\u2013188 (2013)","DOI":"10.1109\/FMCAD.2013.6679408"},{"key":"9390_CR26","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/j.tcs.2015.01.048","volume":"577","author":"M Janota","year":"2015","unstructured":"Janota, M., Marques-Silva, J.: Expansion-based QBF solving versus Q-resolution. Theor. Comput. Sci. 577, 25\u201342 (2015)","journal-title":"Theor. Comput. Sci."},{"key":"9390_CR27","unstructured":"Janota, M., Grigore, R., Marques-Silva, J.: On Checking of Skolem-based Models of QBF. In: Proceedings of the International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion (2012)"},{"key":"9390_CR28","doi-asserted-by":"crossref","unstructured":"Janota, M,. Grigore, R., Marques-Silva, J.: On QBF proofs and preprocessing. In: Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2013), LNCS, vol. 8312, pp. 473\u2013489. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-45221-5_32"},{"key":"9390_CR29","doi-asserted-by":"crossref","unstructured":"J\u00e4rvisalo, M., Heule, M.J.H., Biere, A. Inprocessing rules. In: Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR 2012), LNCS, vol. 7364, pp. 355\u2013370. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-31365-3_28"},{"key":"9390_CR30","unstructured":"Jordan, C., Seidl, M.: The QBF Gallery 2014. http:\/\/qbf.satisfiability.org\/gallery\/ (2014)"},{"key":"9390_CR31","doi-asserted-by":"crossref","unstructured":"Jussila, T., Sinz, C., Biere, A.: Extended resolution proofs for symbolic sat solving with quantification. In: Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing (SAT 2006), vol. 4121, pp. 54\u201360. Springer, Berlin (2006)","DOI":"10.1007\/11814948_8"},{"key":"9390_CR32","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: Proceedings of the 7th International Conference Theory and Applications of Satisfiability Testing (SAT 2007), LNCS, vol. 4501, pp. 201\u2013214. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-72788-0_21"},{"issue":"1","key":"9390_CR33","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. 117(1), 12\u201318 (1995)","journal-title":"Inf. Comput."},{"key":"9390_CR34","doi-asserted-by":"crossref","unstructured":"Kleine B\u00fcning, H., Subramani, K., Zhao, X.: Boolean functions as models for quantified Boolean formulas. J. Autom. Reason. 39(1), 49\u201375 (2007)","DOI":"10.1007\/s10817-007-9067-0"},{"key":"9390_CR35","doi-asserted-by":"crossref","unstructured":"K\u00f6nighofer, R., Seidl, M.: Partial witnesses from preprocessed quantified boolean formulas. In: Proceedings of Design, Automation & Test in Europe Conference & Exhibition, (DATE 2014), IEEE, pp. 1\u20136 (2014)","DOI":"10.7873\/DATE.2014.162"},{"issue":"2\u20133","key":"9390_CR36","first-page":"71","volume":"7","author":"F Lonsing","year":"2010","unstructured":"Lonsing, F., Biere, A.: DepQBF: a dependency-aware QBF solver. J. Satisf. Boolean Model. Comput. 7(2\u20133), 71\u201376 (2010)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"9390_CR37","unstructured":"Lonsing, F., Seidl, M., Van Gelder. A.: The QBF Gallery: Behind the Scenes. CoRR abs\/1508.01045, http:\/\/arxiv.org\/abs\/1508.01045 (2013)"},{"key":"9390_CR38","doi-asserted-by":"crossref","unstructured":"Lonsing, F., Bacchus, F., Biere, A., Egly, U., Seidl, M.: Enhancing search-based QBF solving by dynamic blocked clause elimination. In: Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2015), , LNCS, vol. 9450, pp. 418\u2013433. Springer, Berlin (2015)","DOI":"10.1007\/978-3-662-48899-7_29"},{"issue":"4","key":"9390_CR39","doi-asserted-by":"crossref","first-page":"191","DOI":"10.3233\/AIC-2009-0468","volume":"22","author":"M Narizzano","year":"2009","unstructured":"Narizzano, M., Peschiera, C., Pulina, L., Tacchella, A.: Evaluating and certifying QBFS: a comparison of state-of-the-art tools. AI Commun. 22(4), 191\u2013210 (2009)","journal-title":"AI Commun."},{"key":"9390_CR40","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M., Lonsing, F., Seidl, M., Biere, A.: Resolution-based certificate extraction for QBF\u2014(tool presentation). In: Proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing (SAT 2012), LNCS, vol. 7317, pp. 430\u2013435. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-31612-8_33"},{"key":"9390_CR41","doi-asserted-by":"crossref","unstructured":"Samulowitz, H., Davies, J., Bacchus F.: Preprocessing QBF. In: Proceedings of the 12th International Conference on Principles and Practice of Constraint Programming (CP 2006), LNCS, vol. 4204, pp. 514\u2013529. Springer, Berlin (2006)","DOI":"10.1007\/11889205_37"},{"key":"9390_CR42","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":"9390_CR43","doi-asserted-by":"crossref","unstructured":"Van\u00a0Gelder, A.: Variable independence and resolution paths for quantified Boolean formulas. In: Proceedings of the 17th International Conference on Principles and Practice of Constraint Programming (CP 2011), LNCS, vol 6876, pp. 789\u2013803. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-23786-7_59"},{"key":"9390_CR44","unstructured":"Van\u00a0Gelder, A.: Certificate extraction from variable-elimination QBF preprocessors. In: Proceedings of the 1st International Workshop on Quantified Boolean Formulas (QBF 2013), pp. 35\u201339 (2013)"},{"key":"9390_CR45","doi-asserted-by":"crossref","unstructured":"Wetzler, N., Heule, M.J.H., Hunt, W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT 2014), LNCS, vol. 8561, pp. 422\u2013429. Springer, Berlin (2014)","DOI":"10.1007\/978-3-319-09284-3_31"},{"key":"9390_CR46","doi-asserted-by":"crossref","unstructured":"Yu, Y., Malik, S.: Validating the result of a quantified boolean formula (QBF) solver: theory and practice. In: Proceedings of the Conference on Asia South Pacific Design Automation, (ASP-DAC 2005), pp. 1047\u20131051. ACM Press, New York (2005)","DOI":"10.1145\/1120725.1120821"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9390-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-016-9390-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9390-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T00:48:12Z","timestamp":1749689292000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-016-9390-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,11,5]]},"references-count":46,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,1]]}},"alternative-id":["9390"],"URL":"https:\/\/doi.org\/10.1007\/s10817-016-9390-4","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,11,5]]},"assertion":[{"value":"15 September 2016","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 October 2016","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 November 2016","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}