{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:21:00Z","timestamp":1747592460089},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2008,12,18]],"date-time":"2008-12-18T00:00:00Z","timestamp":1229558400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2009,1]]},"DOI":"10.1007\/s10817-008-9114-5","type":"journal-article","created":{"date-parts":[[2008,12,17]],"date-time":"2008-12-17T03:58:42Z","timestamp":1229486322000},"page":"77-97","source":"Crossref","is-referenced-by-count":48,"title":["Backdoor Sets of Quantified Boolean Formulas"],"prefix":"10.1007","volume":"42","author":[{"given":"Marko","family":"Samer","sequence":"first","affiliation":[]},{"given":"Stefan","family":"Szeider","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2008,12,18]]},"reference":[{"key":"9114_CR1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"434","DOI":"10.1007\/978-3-540-73951-7_38","volume-title":"Proc. 10th International Workshop on Algorithms and Data Structures (WADS\u201907)","author":"F.N. Abu-Khzam","year":"2007","unstructured":"Abu-Khzam, F.N.: Kernelization algorithms for d-hitting set problems. In: Proc. 10th International Workshop on Algorithms and Data Structures (WADS\u201907), LNCS, vol. 4619, pp. 434\u2013445. Springer, New York (2007)"},{"issue":"3","key":"9114_CR2","doi-asserted-by":"crossref","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. Process. Lett. 8(3), 121\u2013123 (1979)","journal-title":"Inf. Process. Lett."},{"key":"9114_CR3","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/3-540-36126-X_12","volume-title":"Proc. 4th International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201902)","author":"A. Ayari","year":"2002","unstructured":"Ayari, A., Basin, D.: Qubos: Deciding quantified Boolean logic using propositional satisfiability solvers. In: Proc. 4th International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201902), LNCS, vol.\u00a02517, pp.\u00a0187\u2013201. Springer, New York (2002)"},{"key":"9114_CR4","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"378","DOI":"10.1007\/11499107_28","volume-title":"Proc. 8th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201905)","author":"M. Benedetti","year":"2005","unstructured":"Benedetti, M.: Quantifier trees for QBFs. In: Proc. 8th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201905), LNCS, vol.\u00a03569, pp. 378\u2013385. Springer, New York (2005)"},{"key":"9114_CR5","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1007\/11527695_5","volume-title":"Proc. 7th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201904)","author":"A. Biere","year":"2005","unstructured":"Biere, A.: Resolve and expand. In: Proc. 7th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201904), LNCS, vol.\u00a03542, pp.\u00a059\u201370. Springer, New York (2005)"},{"key":"9114_CR6","series-title":"LNCS","first-page":"244","volume-title":"Proc. 10th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201907)","author":"U. Bubeck","year":"2007","unstructured":"Bubeck, U., Kleine B\u00fcning, H.: Bounded universal expansion for preprocessing QBF. In: Proc. 10th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201907), LNCS, vol.\u00a04501 of, pages 244\u2013257. Springer, New York (2007)"},{"key":"9114_CR7","series-title":"LNCS","first-page":"238","volume-title":"Proc. 31st International Symposium on Mathematical Foundations of Computer Science (MFCS\u201906)","author":"J. Chen","year":"2006","unstructured":"Chen, J., Kanj, I.A., Xia, G.: Improved parameterized upper bounds for vertex cover. In: Proc. 31st International Symposium on Mathematical Foundations of Computer Science (MFCS\u201906), LNCS, vol.\u00a04162, pp.\u00a0238\u2013249. Springer, New York (2006)"},{"issue":"3","key":"9114_CR8","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/S0166-218X(96)00028-5","volume":"75","author":"Y. Crama","year":"1997","unstructured":"Crama, Y., Ekin, O., Hammer, P.L.: Variable and term removal from Boolean formulae. Discrete Appl. Math. 75(3), 217\u2013230 (1997)","journal-title":"Discrete Appl. Math."},{"key":"9114_CR9","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, New York (1999)"},{"key":"9114_CR10","first-page":"417","volume-title":"Proc. 17th AAAI Conference on Artificial Intelligence (AAAI\u201900)","author":"U. Egly","year":"2000","unstructured":"Egly, U., Eiter, T., Tompits, H., Woltran, S.: Solving advanced reasoning tasks using quantified Boolean formulas. In: Proc. 17th AAAI Conference on Artificial Intelligence (AAAI\u201900), pp.\u00a0417\u2013422. AAAI, Menlo Park (2000)"},{"key":"9114_CR11","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, pp.\u00a048\u201361. Informal Proceedings (2002)"},{"key":"9114_CR12","volume-title":"Parameterized Complexity Theory","author":"J. Flum","year":"2006","unstructured":"Flum, J., Grohe, M.: Parameterized Complexity Theory. Springer, New York (2006)"},{"key":"9114_CR13","first-page":"284","volume-title":"Proc. 16th International Conference 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 International Conference on Automated Planning and Scheduling (ICAPS\u201906), pp.\u00a0284\u2013293. AAAI, Menlo Park (2006)"},{"key":"9114_CR14","unstructured":"Interian, Y.: Backdoor sets for random 3-SAT. In: Proc. 6th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201903), pp.\u00a0231\u2013238. Informal Proceedings (2003)"},{"key":"9114_CR15","first-page":"1368","volume-title":"Proc. 20th AAAI Conference on Artificial Intelligence (AAAI\u201905)","author":"P. Kilby","year":"2005","unstructured":"Kilby, P., Slaney, J.K., Thi\u00e9baux, S., Walsh, T.: Backbones and backdoors in satisfiability. In: Proc. 20th AAAI Conference on Artificial Intelligence (AAAI\u201905), pp.\u00a01368\u20131373. AAAI, Menlo Park (2005)"},{"issue":"1","key":"9114_CR16","doi-asserted-by":"crossref","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. Inf. Comput. 117(1), 12\u201318 (1995)","journal-title":"Inf. Comput."},{"key":"9114_CR17","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":"9114_CR18","first-page":"106","volume-title":"The Art of Computer Programming, vol.\u00a03: Sorting and Searching, chapter 5.2.2 Sorting by Exchanging","author":"D.E. Knuth","year":"1973","unstructured":"Knuth, D.E.: The Art of Computer Programming, vol.\u00a03: Sorting and Searching, chapter 5.2.2 Sorting by Exchanging, pp.\u00a0106\u2013110. Addison-Wesley, Reading (1973)"},{"key":"9114_CR19","first-page":"246","volume-title":"Proc. 16th IEEE International Conference 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 International Conference on Tools with Artificial Intelligence (ICTAI\u201904), pp.\u00a0246\u2013251. IEEE Computer Society, Los Alamitos (2004)"},{"key":"9114_CR20","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)"},{"issue":"1","key":"9114_CR21","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1016\/S1570-8667(03)00009-1","volume":"1","author":"R. Niedermeier","year":"2003","unstructured":"Niedermeier, R., Rossmanith, P.: An efficient fixed-parameter algorithm for 3-hitting set. J. Discret. Algorithms 1(1), 89\u2013102 (2003)","journal-title":"J. Discret. Algorithms"},{"key":"9114_CR22","unstructured":"Nishimura, N., Ragde, P., Szeider, S.: Detecting backdoor sets with respect to Horn and binary clauses. In: Proc. 7th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201904), pp.\u00a096\u2013103. Informal Proceedings (2004)"},{"issue":"7\u20138","key":"9114_CR23","doi-asserted-by":"crossref","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 Inform. 44(7\u20138), 509\u2013523 (2007)","journal-title":"Acta Inform."},{"key":"9114_CR24","first-page":"311","volume-title":"Proc. International Conference on Modeling, Simulation and Visualization Methods and International Conference on Algorithmic Mathematics and Computer Science (MSV\/AMCS\u201904)","author":"C. Otwell","year":"2004","unstructured":"Otwell, C., Remshagen, A., Truemper, K.: An effective QBF solver for planning problems. In: Proc. International Conference on Modeling, Simulation and Visualization Methods and International Conference on Algorithmic Mathematics and Computer Science (MSV\/AMCS\u201904), pp.\u00a0311\u2013316. CSREA, Las Vegas (2004)"},{"key":"9114_CR25","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.\u00a027\u201336. IEEE Computer Society, Los Alamitos (2006)"},{"key":"9114_CR26","volume-title":"Computational Complexity","author":"C.H. Papadimitriou","year":"1994","unstructured":"Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)"},{"key":"9114_CR27","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. J. Artif. Intell. Res. 10, 323\u2013352 (1999)","journal-title":"J. Artif. Intell. Res."},{"key":"9114_CR28","first-page":"124","volume-title":"Proc. 19th AAAI Conference 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 AAAI Conference on Artificial Intelligence (AAAI\u201904), pp.\u00a0124\u2013130. AAAI, Menlo Park (2004)"},{"key":"9114_CR29","series-title":"LNCS","first-page":"382","volume-title":"Proc. 9th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201906)","author":"A. Sabharwal","year":"2006","unstructured":"Sabharwal, A., Ansotegui, C., Gomes, C., Hart, J., Selman, B.: QBF modeling: Exploiting player symmetry for simplicity and efficiency. In: Proc. 9th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201906), LNCS, vol.\u00a04121, pp.\u00a0382\u2013395. Springer, New York (2006)"},{"key":"9114_CR30","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1007\/978-3-540-89439-1_36","volume-title":"Proc. 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR\u201908)","author":"M. Samer","year":"2008","unstructured":"Samer, M.: Variable dependencies of quantified CSPs. In: Proc. 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR\u201908), LNCS, vol.\u00a05330, pp.\u00a0512\u2013527. Springer, New York (2008)"},{"key":"9114_CR31","series-title":"LNCS","first-page":"230","volume-title":"Proc. 10th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201907)","author":"M. Samer","year":"2007","unstructured":"Samer, M., Szeider, S.: Backdoor sets of quantified Boolean formulas. In: Proc. 10th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201907), LNCS, vol.\u00a04501, pp.\u00a0230\u2013243. Springer, New York (2007)"},{"key":"9114_CR32","series-title":"LNCS","first-page":"353","volume-title":"Proc. 9th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201906)","author":"H. Samulowitz","year":"2006","unstructured":"Samulowitz, H., Bacchus, F.: Binary clause reasoning in QBF. In: Proc. 9th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201906), LNCS, vol.\u00a04121, pp.\u00a0353\u2013367. Springer, New York (2006)"},{"key":"9114_CR33","first-page":"1","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.\u00a01\u20139. ACM, New York (1973)"},{"issue":"1\u20133","key":"9114_CR34","first-page":"73","volume":"35","author":"S. Szeider","year":"2005","unstructured":"Szeider, S.: Backdoor sets for DLL subsolvers. J. Autom. Reason. 35(1\u20133), 73\u201388 (2005)","journal-title":"J. Autom. Reason."},{"issue":"1\u20134","key":"9114_CR35","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/s10472-005-0432-6","volume":"43","author":"S. Szeider","year":"2005","unstructured":"Szeider, S.: Generalizations of matched CNF formulas. Ann. Math. Artif. Intell. 43(1\u20134), 223\u2013238 (2005)","journal-title":"Ann. Math. Artif. Intell."},{"key":"9114_CR36","series-title":"LNCS","first-page":"94","volume-title":"Proc. 10th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201907)","author":"S. Szeider","year":"2007","unstructured":"Szeider, S.: Matched formulas and backdoor sets. In: Proc. 10th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201907), LNCS, vol.\u00a04501, pp.\u00a094\u201399. Springer, New York (2007)"},{"issue":"2","key":"9114_CR37","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R.E. Tarjan","year":"1972","unstructured":"Tarjan, R.E.: Depth first search and linear graph algorithms. SIAM J. Comput. 1(2), 146\u2013160 (1972)","journal-title":"SIAM J. Comput."},{"key":"9114_CR38","first-page":"1173","volume-title":"Proc. 18th International Joint Conference 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 International Joint Conference on Artificial Intelligence (IJCAI\u201903), pp.\u00a01173\u20131178. Morgan Kaufmann, San Francisco (2003)"},{"key":"9114_CR39","unstructured":"Williams, R., Gomes, C., Selman, B.: On the connections between backdoors, restarts, and heavy-tailedness in combinatorial search. In: Proc. 6th International Conference on Theory and Applications of Satisfiability Testing (SAT\u201903), pp.\u00a0222\u2013230. Informal Proceedings (2003)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-008-9114-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-008-9114-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-008-9114-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T21:21:48Z","timestamp":1559251308000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-008-9114-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,12,18]]},"references-count":39,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2009,1]]}},"alternative-id":["9114"],"URL":"https:\/\/doi.org\/10.1007\/s10817-008-9114-5","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,12,18]]}}}