{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T05:25:30Z","timestamp":1725513930219},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540727873"},{"type":"electronic","value":"9783540727880"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-72788-0_23","type":"book-chapter","created":{"date-parts":[[2007,6,28]],"date-time":"2007-06-28T12:25:22Z","timestamp":1183033522000},"page":"230-243","source":"Crossref","is-referenced-by-count":5,"title":["Backdoor Sets of Quantified Boolean Formulas"],"prefix":"10.1007","author":[{"given":"Marko","family":"Samer","sequence":"first","affiliation":[]},{"given":"Stefan","family":"Szeider","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"23_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.F., Tarjan, R.E.: A linear-time algorithm for testing the truth of certain quantified Boolean formulas. Information Processing Letters\u00a08(3), 121\u2013123 (1979)","journal-title":"Information Processing Letters"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"23_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 59\u201370. Springer, Heidelberg (2005)"},{"key":"23_CR4","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0515-9","volume-title":"Parameterized Complexity","author":"R.G. Downey","year":"1999","unstructured":"Downey, R.G., Fellows, M.R.: Parameterized Complexity. Springer, Heidelberg (1999)"},{"unstructured":"Egly, U., Tompits, H., Woltran, S.: On quantifier shifting for quantified Boolean formulas. In: Proc. SAT\u201902 Workshop on Theory and Applications of Quantified Boolean Formulas, Informal Proceedings, pp. 48\u201361 (2002)","key":"23_CR5"},{"key":"23_CR6","volume-title":"Parameterized Complexity Theory","author":"J. Flum","year":"2006","unstructured":"Flum, J., Grohe, M.: Parameterized Complexity Theory. Springer, Heidelberg (2006)"},{"key":"23_CR7","first-page":"284","volume-title":"Proc. 16th Int. Conf. on Automated Planning and Scheduling (ICAPS\u201906)","author":"J. Hoffmann","year":"2006","unstructured":"Hoffmann, J., Gomes, C., Selman, B.: Structure and problem hardness: Goal asymmetry and DPLL proofs in SAT-based planning. In: Proc. 16th Int. Conf. on Automated Planning and Scheduling (ICAPS\u201906), pp. 284\u2013293. AAAI Press, Menlo Park (2006)"},{"unstructured":"Interian, Y.: Backdoor sets for random 3-SAT. In: Proc. 6th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT\u201903), Informal Proceedings, pp. 231\u2013238 (2003)","key":"23_CR8"},{"key":"23_CR9","first-page":"1368","volume-title":"Proc. 20th National Conf. on Artificial Intelligence (AAAI\u201905)","author":"P. Kilby","year":"2005","unstructured":"Kilby, P., et al.: Backbones and backdoors in satisfiability. In: Proc. 20th National Conf. on Artificial Intelligence (AAAI\u201905), pp. 1368\u20131373. AAAI Press, Menlo Park (2005)"},{"issue":"1","key":"23_CR10","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":"23_CR11","volume-title":"Propositional logic: Deduction and algorithms","author":"H. Kleine B\u00fcning","year":"1999","unstructured":"Kleine B\u00fcning, H., Lettman, T.: Propositional logic: Deduction and algorithms. Cambridge University Press, Cambridge (1999)"},{"key":"23_CR12","series-title":"The Art of Computer Programming","first-page":"106","volume-title":"Sorting and Searching","author":"D.E. Knuth","year":"1973","unstructured":"Knuth, D.E.: Sorting by Exchanging. In: Knuth, D.E. (ed.) Sorting and Searching. The Art of Computer Programming, vol.\u00a03, pp. 106\u2013110. Addison-Wesley, Reading (1973)"},{"key":"23_CR13","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1109\/ICTAI.2004.68","volume-title":"Proc. 16th IEEE Int. Conf. on Tools with Artificial Intelligence (ICTAI\u201904)","author":"I. Lynce","year":"2004","unstructured":"Lynce, I., Marques-Silva, J.P.: Hidden structure in unsatisfiable random 3-SAT: An empirical study. In: Proc. 16th IEEE Int. Conf. on Tools with Artificial Intelligence (ICTAI\u201904), pp. 246\u2013251. IEEE Computer Society Press, Los Alamitos (2004)"},{"key":"23_CR14","doi-asserted-by":"crossref","DOI":"10.1093\/acprof:oso\/9780198566076.001.0001","volume-title":"Invitation to Fixed-Parameter Algorithms","author":"R. Niedermeier","year":"2006","unstructured":"Niedermeier, R.: Invitation to Fixed-Parameter Algorithms. Oxford University Press, Oxford (2006)"},{"unstructured":"Nishimura, N., Ragde, P., Szeider, S.: Detecting backdoor sets with respect to Horn and binary clauses. In: Proc. 7th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT\u201904), Informal Proceedings, pp. 96\u2013103 (2004)","key":"23_CR15"},{"key":"23_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/11814948_36","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"N. Nishimura","year":"2006","unstructured":"Nishimura, N., Ragde, P., Szeider, S.: Solving #SAT using vertex covers. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 396\u2013409. Springer, Heidelberg (2006)"},{"unstructured":"Otwell, C., Remshagen, A., Truemper, K.: An effective QBF solver for planning problems. In: Proc. Int. Conf. on Modeling, Simulation and Visualization Methods and Int. Conf. on Algorithmic Mathematics and Computer Science (MSV\/AMCS\u201904), pp. 311\u2013316. CSREA Press (2004)","key":"23_CR17"},{"key":"23_CR18","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1109\/LICS.2006.25","volume-title":"Proc. 21st Annual IEEE Symposium on Logic in Computer Science (LICS\u201906)","author":"G. Pan","year":"2006","unstructured":"Pan, G., Vardi, M.Y.: Fixed-parameter hierarchies inside PSpace. In: Proc. 21st Annual IEEE Symposium on Logic in Computer Science (LICS\u201906), pp. 27\u201336. IEEE Computer Society Press, Los Alamitos (2006)"},{"key":"23_CR19","volume-title":"Computational Complexity","author":"C.H. Papadimitriou","year":"1994","unstructured":"Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)"},{"key":"23_CR20","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":"23_CR21","first-page":"124","volume-title":"Proc. 19th National Conf. on Artificial Intelligence (AAAI\u201904)","author":"Y. Ruan","year":"2004","unstructured":"Ruan, Y., Kautz, H.A., Horvitz, E.: The backdoor key: A path to understanding problem hardness. In: Proc. 19th National Conf. on Artificial Intelligence (AAAI\u201904), pp. 124\u2013130. AAAI Press, Menlo Park (2004)"},{"key":"23_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/11814948_35","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"A. Sabharwal","year":"2006","unstructured":"Sabharwal, A., et al.: QBF modeling: Exploiting player symmetry for simplicity and efficiency. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 382\u2013395. Springer, Heidelberg (2006)"},{"key":"23_CR23","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)"},{"key":"23_CR24","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/800125.804029","volume-title":"Proc. 5th Annual ACM Symposium on Theory of Computing (STOC\u201973)","author":"L.J. Stockmeyer","year":"1973","unstructured":"Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time. In: Proc. 5th Annual ACM Symposium on Theory of Computing (STOC\u201973), pp. 1\u20139. ACM Press, New York (1973)"},{"issue":"1-3","key":"23_CR25","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. Journal of Automated Reasoning\u00a035(1-3), 73\u201388 (2005)","journal-title":"Journal of Automated Reasoning"},{"issue":"1-4","key":"23_CR26","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/s10472-004-9432-1","volume":"43","author":"S. Szeider","year":"2005","unstructured":"Szeider, S.: Generalizations of matched CNF formulas. Ann. Math. Artif. Intell.\u00a043(1-4), 223\u2013238 (2005)","journal-title":"Ann. Math. Artif. Intell."},{"key":"23_CR27","first-page":"1173","volume-title":"Proc. 18th Int. Joint Conf. on Artificial Intelligence (IJCAI\u201903)","author":"R. Williams","year":"2003","unstructured":"Williams, R., Gomes, C., Selman, B.: Backdoors to typical case complexity. In: Proc. 18th Int. Joint Conf. on Artificial Intelligence (IJCAI\u201903), pp. 1173\u20131178. Morgan Kaufmann, San Francisco (2003)"},{"unstructured":"Williams, R., Gomes, C., Selman, B.: On the connections between backdoors, restarts, and heavy-tailedness in combinatorial search. In: Proc. 6th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT\u201903), Informal Proceedings, pp. 222\u2013230 (2003)","key":"23_CR28"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2007"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-72788-0_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:05:08Z","timestamp":1605762308000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-72788-0_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540727873","9783540727880"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-72788-0_23","relation":{},"subject":[]}}