{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,15]],"date-time":"2026-01-15T05:09:26Z","timestamp":1768453766235,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540280057","type":"print"},{"value":"9783540318644","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11532231_27","type":"book-chapter","created":{"date-parts":[[2010,7,21]],"date-time":"2010-07-21T18:56:52Z","timestamp":1279738612000},"page":"369-376","source":"Crossref","is-referenced-by-count":53,"title":["sKizzo: A Suite to Evaluate and Certify QBFs"],"prefix":"10.1007","author":[{"given":"Marco","family":"Benedetti","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"27_CR1","doi-asserted-by":"crossref","unstructured":"Ayari, A., Basin, D.: Bounded Model Construction for Monadic Second-order Logics. In: Proc. of CAV 2000 (2000)","DOI":"10.1007\/10722167_11"},{"key":"27_CR2","unstructured":"Benedetti, M.: sKizzo: a QBF Decision Procedure based on Propositional Skolemization and Symbolic Reasoning, Tech.Rep. 04-11-03, ITC-irst (2004)"},{"key":"27_CR3","unstructured":"Benedetti, M.: sKizzo\u2019s web site (2004), http:\/\/sra.itc.it\/people\/benedetti\/sKizzo"},{"key":"27_CR4","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":"27_CR5","unstructured":"Benedetti, M.: Extracting Certificates from Quantified Boolean Formulas. In: Proc. of IJCAI 2005 (2005)"},{"key":"27_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/11499107_28","volume-title":"Theory and Applications of Satisfiability Testing","author":"M. Benedetti","year":"2005","unstructured":"Benedetti, M.: Quantifier trees for qBFs. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 378\u2013385. Springer, Heidelberg (2005)"},{"key":"27_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/11527695_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"A. Biere","year":"2005","unstructured":"Biere, A.: Resolve and expand. In: Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 59\u201370. Springer, Heidelberg (2005)"},{"key":"27_CR8","doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: QuBE: A system for deciding Quantified Boolean Formulas Satisfiability. In: Proc. of the International Joint Conference on Automated Reasoning, IJCAR 2001 (2001)","DOI":"10.1007\/3-540-45744-5_27"},{"key":"27_CR9","doi-asserted-by":"crossref","unstructured":"Le Berre, D., Narizzano, M., Simon, L., Tacchella, A.: Second QBF solvers evaluation, avaliable on-line (2004), at http:\/\/www.qbflib.org","DOI":"10.1007\/11527695_28"},{"key":"27_CR10","unstructured":"Letz, R.: Advances in Decision Procedures for Quantified Boolean Formulas. In: Proceedings of the First International Workshop on Quantified Boolean Formulae (QBF 2001), pp. 55\u201364 (2001)"},{"key":"27_CR11","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: Towards Symmetric Treatment of Conflicts And Satisfaction in Quantified Boolean Satisfiability Solver. In: Proc. of CP 2002 (2002)","DOI":"10.1007\/3-540-46135-3_14"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-20"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11532231_27.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:09:11Z","timestamp":1605643751000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11532231_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540280057","9783540318644"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/11532231_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}