{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T03:53:16Z","timestamp":1725594796286},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642221095"},{"type":"electronic","value":"9783642221101"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-22110-1_12","type":"book-chapter","created":{"date-parts":[[2011,7,4]],"date-time":"2011-07-04T13:08:45Z","timestamp":1309784925000},"page":"149-164","source":"Crossref","is-referenced-by-count":18,"title":["Resolution Proofs and Skolem Functions in QBF Evaluation and Applications"],"prefix":"10.1007","author":[{"given":"Valeriy","family":"Balabanov","sequence":"first","affiliation":[]},{"given":"Jie-Hong R.","family":"Jiang","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/978-3-540-32275-7_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Benedetti","year":"2005","unstructured":"Benedetti, M.: Evaluating qBFs via symbolic skolemization. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 285\u2013300. Springer, Heidelberg (2005)"},{"key":"12_CR2","unstructured":"Benedetti, M.: Extracting Certificates from Quantified Boolean Formulas. In: Proc. Int.Joint Conf. on Artificial Intelligence (IJCAI) (2005)"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Automatic Hardware Synthesis from Specifications: A Case Study. In: Proc. Design Automation and Test in Europe (2007)","DOI":"10.1109\/DATE.2007.364456"},{"key":"12_CR4","unstructured":"Berkeley Logic Synthesis and Verification Group. ABC: A System for Sequential Synthesis and Verification, http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc\/"},{"issue":"2","key":"12_CR5","doi-asserted-by":"publisher","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. Journal of Automated Reasoning\u00a028(2), 101\u2013142 (2002)","journal-title":"Journal of Automated Reasoning"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/11499107_32","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. Dershowitz","year":"2005","unstructured":"Dershowitz, N., Hanna, Z., Katz, J.: Bounded model checking with QBF. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 408\u2013414. Springer, Heidelberg (2005)"},{"key":"12_CR7","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.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"12_CR8","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 Quantified Boolean Logic Satisfiability. Artificial Intelligence Research\u00a026, 371\u2013416 (2006)","journal-title":"Artificial Intelligence Research"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-540-72788-0_21","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"T. Jussila","year":"2007","unstructured":"Jussila, T., Biere, A., Sinz, C., Kr\u00f6ning, D., Wintersteiger, C.M.: A first step towards a unified proof checker for QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 201\u2013214. Springer, Heidelberg (2007)"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Jiang, J.-H.R., Lin, H.-P., Hung, W.-L.: Interpolating Functions from Large Boolean Relations. In: Proc. Int.Conf. on Computer-Aided Design (ICCAD), pp. 779\u2013784 (2009)","DOI":"10.1145\/1687399.1687544"},{"issue":"1","key":"12_CR11","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. Information and Computation\u00a0117(1), 12\u201318 (1995)","journal-title":"Information and Computation"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Narizzano, M., Peschiera, C., Pulina, L., Tacchella, A.: Evaluating and Certifying QBFs: A Comparison of State-of-the-Art Tools. AI Communications (2009)","DOI":"10.3233\/AIC-2009-0468"},{"key":"12_CR13","volume-title":"Computational Complexity","author":"C.H. Papadimitriou","year":"1994","unstructured":"Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)"},{"key":"12_CR14","unstructured":"QBF Solver Evaluation Protal, http:\/\/www.qbflib.org\/qbfeval\/"},{"key":"12_CR15","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1613\/jair.591","volume":"10","author":"J. Rintanen","year":"1999","unstructured":"Rintanen, J.: Constructing Conditional Plans by a Theorem-Prover. Journal of Artificial Intelligence Research\u00a010, 323\u2013352 (1999)","journal-title":"Journal of Artificial Intelligence Research"},{"key":"12_CR16","first-page":"125","volume-title":"Translation in From Frege to G\u00f6del, A Source Book in Mathematical Logic","author":"T. Skolem","year":"1928","unstructured":"Skolem, T.: \u00dcber die Mathematische Logik. Norsk. Mat. Tidsk. In: van Heijenoor, J. (ed.) Translation in From Frege to G\u00f6del, A Source Book in Mathematical Logic, vol.\u00a010, pp. 125\u2013142. Harvard Univ. Press, Cambridge (1928)"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-540-72788-0_34","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"S. Staber","year":"2007","unstructured":"Staber, S., Bloem, R.: Fault localization and correction with QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 355\u2013368. Springer, Heidelberg (2007)"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Tancau, L., Bod\u00edk, R., Seshia, S., Saraswat, V.: Combinatorial Sketching for Finite Programs. In: Int.Conf. on Architectural Support for Programming Languages and Operating Systems(ASPLOS), pp. 404\u2013415 (2006)","DOI":"10.1145\/1168857.1168907"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Tseitin, G.: On the Complexity of Derivation in Propositional Calculus. Studies in Constructive Mathematics and Mathematical Logic, 466\u2013483 (1970)","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Yu, Y., Malik, S.: Validating the Result of a Quantified Boolean Formula (QBF) Solvers: Theory and Practice. In: Proc. Asia and South Pacific Design Automation Conference (2005)","DOI":"10.1145\/1120725.1120821"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: Conflict Driven Learning in a Quantified Boolean Satisfiability Solver. In: Proc. Int\u2019l Conf. on Computer-Aided Design (ICCAD), pp. 442\u2013449 (2002)","DOI":"10.1145\/774572.774637"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22110-1_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,21]],"date-time":"2020-06-21T03:01:45Z","timestamp":1592708505000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22110-1_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642221095","9783642221101"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22110-1_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}