{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T04:47:03Z","timestamp":1725857223534},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319409696"},{"type":"electronic","value":"9783319409702"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-40970-2_28","type":"book-chapter","created":{"date-parts":[[2016,6,10]],"date-time":"2016-06-10T11:14:55Z","timestamp":1465557295000},"page":"453-469","source":"Crossref","is-referenced-by-count":7,"title":["2QBF: Challenges and Solutions"],"prefix":"10.1007","author":[{"given":"Valeriy","family":"Balabanov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jie-Hong Roland","family":"Jiang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Scholl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan","family":"Mishchenko","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert K.","family":"Brayton","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,11]]},"reference":[{"key":"28_CR1","unstructured":"QBF Gallery 2014. http:\/\/qbf.satisfiability.org\/gallery\/"},{"key":"28_CR2","unstructured":"QBF solver evaluation portal. http:\/\/www.qbflib.org\/qbfeval\/"},{"key":"28_CR3","unstructured":"QDIMACS: Standard QBF input format. http:\/\/www.qbflib.org\/qdimacs"},{"key":"28_CR4","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.-H.R.: Unified QBF certification and its applications. Formal Meth. Syst. Des. 41, 45\u201365 (2012)","journal-title":"Formal Meth. Syst. Des."},{"key":"28_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/11532231_27","volume-title":"Automated Deduction \u2013 CADE-20","author":"M Benedetti","year":"2005","unstructured":"Benedetti, M.: sKizzo: a suite to evaluate and certify QBFs. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 369\u2013376. Springer, Heidelberg (2005)"},{"key":"28_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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, vol. 6803, pp. 101\u2013115. Springer, Heidelberg (2011)"},{"key":"28_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"28_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1007\/978-3-540-30494-4_15","volume-title":"Formal Methods in Computer-Aided Design","author":"E Giunchiglia","year":"2004","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: QuBE++: an efficient QBF solver. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 201\u2013213. Springer, Heidelberg (2004)"},{"key":"28_CR9","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":"28_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"28_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"230","DOI":"10.1007\/978-3-642-21581-0_19","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"M Janota","year":"2011","unstructured":"Janota, M., Marques-Silva, J.: Abstraction-based algorithm for 2QBF. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 230\u2013244. Springer, Heidelberg (2011)"},{"key":"28_CR12","unstructured":"Janota, M., Marques-Silva, J.: Solving QBF by clause selection. In: Proceedings International Joint Conference on Artificial Intelligence (IJCAI), pp. 325\u2013331 (2015)"},{"key":"28_CR13","doi-asserted-by":"crossref","first-page":"71","DOI":"10.3233\/SAT190077","volume":"7","author":"F Lonsing","year":"2010","unstructured":"Lonsing, F., Biere, A.: DepQBF: a dependency-aware QBF solver (system description). J. Satisfiability Boolean Model. Comput. 7, 71\u201376 (2010)","journal-title":"J. Satisfiability Boolean Model. Comput."},{"key":"28_CR14","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: Boolean satisfiability in electronic design automation. In: Proceednigs Design Automation Conference (DAC), pp. 675\u2013680 (2000)","DOI":"10.1145\/337292.337611"},{"key":"28_CR15","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Brayton, R.K., Feng, W., Greene, J.W.: Technology mapping into general programmable cells. In: Proceedings International Symposium on Field-Programmable Gate Arrays (FPGA), pp. 70\u201373 (2015)","DOI":"10.1145\/2684746.2689082"},{"key":"28_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/978-3-540-24605-3_31","volume-title":"Theory and Applications of Satisfiability Testing","author":"M Mneimneh","year":"2004","unstructured":"Mneimneh, M., Sakallah, K.A.: Computing vertex eccentricity in exponentially large graphs: QBF formulation and solution. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 411\u2013425. Springer, Heidelberg (2004)"},{"key":"28_CR17","doi-asserted-by":"crossref","unstructured":"Pigorsch, F., Scholl, C.: Exploiting structure in an AIG based QBF solver. In: Proceedings Design, Automation and Test in Europe (DATE), pp. 1596\u20131601 (2009)","DOI":"10.1109\/DATE.2009.5090919"},{"issue":"1","key":"28_CR18","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/s10817-005-0981-8","volume":"34","author":"A Remshagen","year":"2005","unstructured":"Remshagen, A., Truemper, K.: An effective algorithm for the futile questioning problem. J. Autom. Reasoning 34(1), 31\u201347 (2005)","journal-title":"J. Autom. Reasoning"},{"key":"28_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"174","DOI":"10.1007\/978-3-642-21581-0_15","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"V Ryvchin","year":"2011","unstructured":"Ryvchin, V., Strichman, O.: Faster extraction of high-level minimal unsatisfiable cores. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 174\u2013187. Springer, Heidelberg (2011)"},{"key":"28_CR20","doi-asserted-by":"crossref","unstructured":"Tseitin, G.: On the complexity of derivation in propositional calculus. Studies in Constructive Mathematics and Mathematical Logic (1970)","DOI":"10.1007\/978-1-4899-5327-8_25"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2016"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40970-2_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,22]],"date-time":"2020-09-22T01:27:23Z","timestamp":1600738043000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40970-2_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319409696","9783319409702"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40970-2_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}