{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:53:29Z","timestamp":1725512009523},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540797180"},{"type":"electronic","value":"9783540797197"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-79719-7_15","type":"book-chapter","created":{"date-parts":[[2008,5,6]],"date-time":"2008-05-06T08:04:57Z","timestamp":1210061097000},"page":"154-160","source":"Crossref","is-referenced-by-count":5,"title":["Computation of Renameable Horn Backdoors"],"prefix":"10.1007","author":[{"given":"Stephan","family":"Kottler","sequence":"first","affiliation":[]},{"given":"Michael","family":"Kaufmann","sequence":"additional","affiliation":[]},{"given":"Carsten","family":"Sinz","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","unstructured":"Dimacs, \n                  \n                    ftp:\/\/dimacs.rutgers.edu\/pub\/challenge\/satisfiability\/benchmarks\/"},{"key":"15_CR2","unstructured":"The international SAT competition (2002-2007), \n                  \n                    http:\/\/www.satcompetition.org"},{"key":"15_CR3","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.F., Tarjan, R.E.: A linear-time algorithm for testing the truth of certain quantified boolean formulas. Inf. Proc. Lett.\u00a08, 121\u2013123 (1979)","journal-title":"Inf. Proc. Lett."},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_6","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"J. Buresh-Oppenheim","year":"2006","unstructured":"Buresh-Oppenheim, J., Mitchell, D.G.: Minimum witnesses for unsatisfiable 2CNFs. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, Springer, Heidelberg (2006)"},{"key":"15_CR5","unstructured":"Chen, J., Liu, Y., Lu, S.: Directed feedback vertex set problem is fpt. In Structure Theory and FPT Algorithmics for Graphs, Digraphs and Hypergraphs (2007)"},{"issue":"7","key":"15_CR6","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"issue":"3","key":"15_CR7","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM\u00a07(3), 201\u2013215 (1960)","journal-title":"J. ACM"},{"issue":"3","key":"15_CR8","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/S0020-0190(02)00491-X","volume":"86","author":"C. Demetrescu","year":"2003","unstructured":"Demetrescu, C., Finocchi, I.: Combinatorial algorithms for feedback problems in directed graphs. Inf. Process. Lett.\u00a086(3), 129\u2013136 (2003)","journal-title":"Inf. Process. Lett."},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74970-7_20","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2007","author":"B. Dilkina","year":"2007","unstructured":"Dilkina, B., Gomes, C.P., Sabharwal, A.: Tradeoffs in the complexity of backdoor detection. In: Bessi\u00e8re, C. (ed.) CP 2007. LNCS, vol.\u00a04741, Springer, Heidelberg (2007)"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"Theory and Applications of Satisfiability Testing","author":"Y. Interian","year":"2004","unstructured":"Interian, Y.: Backdoor sets for random 3-sat. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, Springer, Heidelberg (2004)"},{"key":"15_CR11","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1145\/322047.322059","volume":"25","author":"H.R. Lewis","year":"1978","unstructured":"Lewis, H.R.: Renaming a set of clauses as a horn set. J. ACM\u00a025, 134\u2013135 (1978)","journal-title":"J. ACM"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. Nishimura","year":"2005","unstructured":"Nishimura, N., Ragde, P., Szeider, S.: Detecting backdoor sets with respect to Horn and Binary clauses. In: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, Springer, Heidelberg (2005)"},{"issue":"7-8","key":"15_CR13","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1007\/s00236-007-0056-x","volume":"44","author":"N. Nishimura","year":"2007","unstructured":"Nishimura, N., Ragde, P., Szeider, S.: Solving #SAT using vertex covers. Acta Informatica\u00a044(7-8), 509\u2013523 (2007)","journal-title":"Acta Informatica"},{"key":"15_CR14","volume-title":"Computational Complexity","author":"C.H. Papadimitriou","year":"1994","unstructured":"Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)"},{"key":"15_CR15","volume-title":"ICTAI 2006","author":"L. Paris","year":"2006","unstructured":"Paris, L., Ostrowski, R., Siegel, P., Sais, L.: Computing horn strong backdoor sets thanks to local search. In: ICTAI 2006, IEEE Computer Society, Los Alamitos (2006)"},{"key":"15_CR16","unstructured":"Ruan, Y., Kautz, H.A., Horvitz, E.: The backdoor key: A path to understanding problem hardness. In: AAAI, pp. 124\u2013130 (2004)"},{"key":"15_CR17","unstructured":"Sinz, C.: SAT benchmarks (2003), \n                  \n                    http:\/\/www-sr.informatik.uni-tuebingen.de\/~sinz\/DC"},{"key":"15_CR18","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s10817-005-9007-9","volume":"35","author":"S. Szeider","year":"2005","unstructured":"Szeider, S.: Backdoor sets for dll subsolvers. J. Autom. Reasoning\u00a035, 73\u201388 (2005)","journal-title":"J. Autom. Reasoning"},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72788-0_12","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"S. Szeider","year":"2007","unstructured":"Szeider, S.: Matched formulas and backdoor sets. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, Springer, Heidelberg (2007)"},{"key":"15_CR20","unstructured":"Williams, R., Gomes, C., Selman, B.: Backdoors to typical case complexity. In: IJCAI (2003)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2008"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-79719-7_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:29:10Z","timestamp":1619522950000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-79719-7_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540797180","9783540797197"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-79719-7_15","relation":{},"subject":[]}}