{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T17:27:29Z","timestamp":1725470849584},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540462675"},{"type":"electronic","value":"9783540462682"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11889205_37","type":"book-chapter","created":{"date-parts":[[2006,9,28]],"date-time":"2006-09-28T08:07:42Z","timestamp":1159430862000},"page":"514-529","source":"Crossref","is-referenced-by-count":23,"title":["Preprocessing QBF"],"prefix":"10.1007","author":[{"given":"Horst","family":"Samulowitz","sequence":"first","affiliation":[]},{"given":"Jessica","family":"Davies","sequence":"additional","affiliation":[]},{"given":"Fahiem","family":"Bacchus","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"37_CR1","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/0020-0190(79)90002-4","volume":"8","author":"B. Aspvall","year":"1979","unstructured":"Aspvall, B., Plass, M., Tarjan, R.: A linear-time algorithms for testing the truth of certain quantified boolean formulas. Information Processing Letters\u00a08, 121\u2013123 (1979)","journal-title":"Information Processing Letters"},{"unstructured":"Bacchus, F.: Enhancing davis putnam with extended binary clause reasoning. In: Eighteenth national conference on Artificial intelligence, pp. 613\u2013619 (2002)","key":"37_CR2"},{"key":"37_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-3-540-24605-3_26","volume-title":"Theory and Applications of Satisfiability Testing","author":"F. Bacchus","year":"2004","unstructured":"Bacchus, F., Winter, J.: Effective preprocessing with hyper-resolution and equality reduction. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 341\u2013355. Springer, Heidelberg (2004)"},{"unstructured":"Benedetti, M.: Skizzo: a QBF decision procedure based on propositional skolemization and symbolic reasoning. Technical Report TR04-11-03 (2004)","key":"37_CR4"},{"key":"37_CR5","series-title":"Lecture Notes in Computer Science","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, vol.\u00a03452, pp. 285\u2013300. Springer, Heidelberg (2005)"},{"unstructured":"Benedetti, M.: Extracting Certificates from Quantified Boolean Formulas. In: Proc. of 9th International Joint Conference on Artificial Intelligence (IJCAI 2005) (2005)","key":"37_CR6"},{"key":"37_CR7","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":"37_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","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.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 238\u2013246. Springer, Heidelberg (2005)"},{"issue":"1","key":"37_CR9","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"H.K. B\u00fcning","year":"1995","unstructured":"B\u00fcning, H.K., Karpinski, M., Fl\u00fcgel, A.: Resolution for quantified boolean formulas. Inf. Comput.\u00a0117(1), 12\u201318 (1995)","journal-title":"Inf. Comput."},{"key":"37_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/11499107_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2005","unstructured":"E\u00e9n, N., Biere, A.: Effective Preprocessing in SAT Through Variable and Clause Elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 61\u201375. Springer, Heidelberg (2005)"},{"unstructured":"Egly, U., Eiter, T., Tompits, H., Woltran, S.: Solving advanced reasoning tasks using quantified boolean formulas. In: AAAI\/IAAI, pp. 417\u2013422 (2000)","key":"37_CR11"},{"unstructured":"Gent, I.P., Nightingale, P., Stergiou, K.: Qcsp-solve: A solver for quantified constraint satisfaction problems. In: Proceedings of the International Joint Conference on Artifical Intelligence (IJCAI), pp. 138\u2013143 (2005)","key":"37_CR12"},{"unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Quantified Boolean Formulas satisfiability library (QBFLIB) (2001), \n                    \n                      http:\/\/www.qbflib.org\/","key":"37_CR13"},{"key":"37_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/3-540-45744-5_27","volume-title":"Automated Reasoning","author":"E. Giunchiglia","year":"2001","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: QUBE: A system for deciding quantified boolean formulas satisfiability. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 364\u2013369. Springer, Heidelberg (2001)"},{"unstructured":"Narizzano, M., Tacchella, A.: QBF evaluation (2005), \n                    \n                      http:\/\/www.qbflib.org\/qbfeval\/2005","key":"37_CR15"},{"key":"37_CR16","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":"37_CR17","doi-asserted-by":"publisher","first-page":"578","DOI":"10.1007\/11564751_43","volume-title":"Principles and Practice of Constraint Programming","author":"H. Samulowitz","year":"2005","unstructured":"Samulowitz, H., Bacchus, F.: Using SAT in QBF. In: Principles and Practice of Constraint Programming, pp. 578\u2013592. Springer, New York (2005), Available at: \n                    \n                      http:\/\/www.cs.toronto.edu\/~fbacchus\/sat.html"},{"key":"37_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/11814948_33","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"H. Samulowitz","year":"2006","unstructured":"Samulowitz, H., Bacchus, F.: Binary clause reasoning in QBF. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 353\u2013367. Springer, Heidelberg (2006)"},{"unstructured":"Samulowitz, H., Davies, J., Bacchus, F.: QBF Preprocessor Prequel (2006), Available at: \n                    \n                      http:\/\/www.cs.toronto.edu\/~fbacchus\/sat.html","key":"37_CR19"},{"doi-asserted-by":"crossref","unstructured":"Stergiou, K.: Repair-based methods for quantified csps. In: Principles and Practice of Constraint Programming, pp. 652\u2013666 (2005)","key":"37_CR20","DOI":"10.1007\/11564751_48"},{"key":"37_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1007\/3-540-46027-6","volume-title":"Principles and Practice of Constraint Programming - CP 2002","author":"L. Zhang","year":"2002","unstructured":"Zhang, L., Malik, S.: Towards symmetric treatment of conflicts and satisfaction in quantified boolean satisfiability solver. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol.\u00a02470, pp. 185\u2013199. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming - CP 2006"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11889205_37.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T03:30:37Z","timestamp":1619494237000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11889205_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540462675","9783540462682"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/11889205_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}