{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T13:29:36Z","timestamp":1725542976093},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540372066"},{"type":"electronic","value":"9783540372073"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814948_33","type":"book-chapter","created":{"date-parts":[[2006,7,18]],"date-time":"2006-07-18T10:12:38Z","timestamp":1153217558000},"page":"353-367","source":"Crossref","is-referenced-by-count":12,"title":["Binary Clause Reasoning in QBF"],"prefix":"10.1007","author":[{"given":"Horst","family":"Samulowitz","sequence":"first","affiliation":[]},{"given":"Fahiem","family":"Bacchus","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"33_CR1","series-title":"DIMACS Series","doi-asserted-by":"crossref","first-page":"559","DOI":"10.1090\/dimacs\/026\/27","volume-title":"Cliques, Coloring and Satisfiability","author":"A. Gelder Van","year":"1996","unstructured":"Van Gelder, A., Tsuji, Y.K.: Satisfiability testing with more reasoning and less guessing. In: Johnson, D., Trick, M. (eds.) Cliques, Coloring and Satisfiability. DIMACS Series, vol.\u00a026, pp. 559\u2013586. American Mathematical Society, Providence (1996)"},{"key":"33_CR2","unstructured":"Bacchus, F.: Enhancing davis putnam with extended binary clause reasoning. In: Eighteenth national conference on Artificial intelligence, pp. 613\u2013619 (2002)"},{"key":"33_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)"},{"key":"33_CR4","doi-asserted-by":"crossref","unstructured":"Samulowitz, H., Davies, J., Bacchus, F.: Preprocessing QBF. Submitted to CP (2006)","DOI":"10.1007\/11889205_37"},{"key":"33_CR5","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, 12\u201318 (1995)","journal-title":"Inf. Comput."},{"key":"33_CR6","unstructured":"Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient conflict driven learning in a Boolean satisfiability solver. In: International Conference on Computer-Aided Design (ICCAD 2001), pp. 279\u2013285 (2001)"},{"key":"33_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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 a Symmetric Treatment of Satisfaction and Conflicts in Quantified Boolean Formula Evaluation. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol.\u00a02470, Springer, Heidelberg (2002)"},{"key":"33_CR8","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Quantified Boolean Formulas satisfiability library (QBFLIB) (2001), http:\/\/www.qbflib.org\/"},{"key":"33_CR9","unstructured":"Samulowitz, H., Bacchus, F.: QBF Solver 2clsQ (2006), available at http:\/\/www.cs.toronto.edu\/~fbacchus\/sat.html"},{"key":"33_CR10","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)"},{"key":"33_CR11","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)"},{"key":"33_CR12","unstructured":"Benedetti, M.: skizzo: a QBF decision procedure based on propositional skolemization and symbolic reasoning. Technical Report TR04-11-03 (2004)"},{"key":"33_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"578","DOI":"10.1007\/11564751_43","volume-title":"Principles and Practice of Constraint Programming - CP 2005","author":"H. Samulowitz","year":"2005","unstructured":"Samulowitz, H., Bacchus, F.: Using SAT in QBF. In: van Beek, P. (ed.) CP 2005. LNCS, vol.\u00a03709, pp. 578\u2013592. Springer, Heidelberg (2005), http:\/\/www.cs.toronto.edu\/~fbacchus\/sat.html"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing - SAT 2006"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814948_33.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:28:03Z","timestamp":1619508483000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814948_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540372066","9783540372073"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/11814948_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}