{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,1]],"date-time":"2025-12-01T02:48:29Z","timestamp":1764557309519},"reference-count":61,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2014,3,15]],"date-time":"2014-03-15T00:00:00Z","timestamp":1394841600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2014,4]]},"DOI":"10.1007\/s10472-014-9407-9","type":"journal-article","created":{"date-parts":[[2014,3,18]],"date-time":"2014-03-18T04:23:41Z","timestamp":1395116621000},"page":"399-431","source":"Crossref","is-referenced-by-count":8,"title":["Tradeoffs in the complexity of backdoors to satisfiability: dynamic sub-solvers and learning during search"],"prefix":"10.1007","volume":"70","author":[{"given":"Bistra","family":"Dilkina","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carla P.","family":"Gomes","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ashish","family":"Sabharwal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,3,15]]},"reference":[{"issue":"1","key":"9407_CR1","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0196-6774(80)90007-3","volume":"1","author":"B Aspvall","year":"1980","unstructured":"Aspvall, B.: Recognizing disguised NR(1) instances of the satisfiability problem. J. Algoritm. 1(1), 97\u2013103 (1980)","journal-title":"J. Algoritm."},{"issue":"3","key":"9407_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":"9407_CR3","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1613\/jair.1410","volume":"22","author":"P Beame","year":"2004","unstructured":"Beame, P., Kautz, H., Sabharwal, A.: Understanding and harnessing the potential of clause learning. JAIR: J. Artif. Intell. Res. 22, 319\u2013351 (2004)","journal-title":"JAIR: J. Artif. Intell. Res."},{"key":"9407_CR4","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: DAC-99: 36th Design Automation Conference, pp. 317\u2013320 (1999)","DOI":"10.1145\/309847.309942"},{"key":"9407_CR5","doi-asserted-by":"crossref","unstructured":"Brockington, M., Culberson, J. C.: Camouflaging independent sets in quasi-random graphs. In: Johnson, D.S., Trick, M.A. (eds.) Cliques, Coloring and Satisfiability: The Second DIMACS Implementation Challenge, volume 26 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pp. 75\u201388. American Mathematical Society (1996)","DOI":"10.1090\/dimacs\/026\/05"},{"key":"9407_CR6","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Inf. Comput. 98, 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"issue":"2","key":"9407_CR7","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/0020-0190(92)90098-G","volume":"42","author":"V Chandru","year":"1992","unstructured":"Chandru, V., Hooker, J.N.: Detecting embedded Horn structure in propositional logic. Inf. Process. Lett. 42(2), 109\u2013111 (1992)","journal-title":"Inf. Process. Lett."},{"key":"9407_CR8","doi-asserted-by":"crossref","unstructured":"Chen, H., Dalmau, V.: Beyond hypertree width: decomposition methods without decompositions. In: CP-05: 11th International Conference on Principles and Practice of Constraint Programming, pp. 167\u2013181 (2005)","DOI":"10.1007\/11564751_15"},{"key":"9407_CR9","doi-asserted-by":"crossref","unstructured":"Chen, H., Gomes, C.P., Selman, B.: Formal models of heavy-tailed behavior in combinatorial search. In: CP-01: 7th International Conference on Principles and Practice of Constraint Programming, volume 2239 of LNCS. (2001)","DOI":"10.1007\/3-540-45578-7_28"},{"key":"9407_CR10","first-page":"201","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Commun. ACM 7, 201\u2013215 (1960)","journal-title":"Commun. ACM"},{"key":"9407_CR11","doi-asserted-by":"crossref","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 5, 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"key":"9407_CR12","unstructured":"Dechter, R.: Constraint Processing. Morgan Kaufmann Publishers Inc. (2003). ISBN 1558608907"},{"issue":"1","key":"9407_CR13","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(87)90002-6","volume":"34","author":"R Dechter","year":"1987","unstructured":"Dechter, R., Pearl, J.: Network-based heuristics for constraint-satisfaction problems. Artif. Intell. 34(1), 1\u201338 (1987)","journal-title":"Artif. Intell."},{"key":"9407_CR14","unstructured":"del Val, A.: On 2-SAT and renamable horn. In: AAAI-00: 17th National Conference on Artificial Intelligence, pp. 279\u2013284 (2000)"},{"key":"9407_CR15","unstructured":"Deville, Y., Van Hentenryck, P.: An efficient arc consistency algorithm for a class of CSP problems. In: IJCAI-91: 12th International Joint Conference on Artificial Intelligence, pp. 325\u2013330 (1991)"},{"key":"9407_CR16","doi-asserted-by":"crossref","unstructured":"Dilkina, B., Gomes, C.P., Sabharwal, A.: Tradeoffs in the complexity of backdoor detection. In: CP-07: 13th International Conference on Principles and Practice of Constraint Programming, volume 4741 of LNCS, pp. 256\u2013270 (2007)","DOI":"10.1007\/978-3-540-74970-7_20"},{"key":"9407_CR17","unstructured":"Dilkina, B., Gomes, C.P., Sabharwal, A.: The impact of network topology on pure Nash equilibria in graphical games. In: AAAI-07: 22nd Conference on Artificial Intelligence, pp. 42\u201349 (2007)"},{"key":"9407_CR18","unstructured":"Dilkina, B., Gomes, C.P., Sabharwal, A.: Tradeoffs in backdoors: inconsistency detection, dynamic simplification, and preprocessing. In: ISAIM-08: 10th International Symposium on Artificial Intelligence and Mathematics (2008)"},{"key":"9407_CR19","doi-asserted-by":"crossref","unstructured":"Dilkina, B., Gomes, C.P., Malitsky, Y., Sabharwal, A., Sellmann, M.: Backdoors to combinatorial optimization: feasibility and optimality. In: CPAIOR-09: 6th International Conference on Integration of AI and OR Techniques in Constraint Programming, pp. 56\u201370. Pittsburgh (2009)","DOI":"10.1007\/978-3-642-01929-6_6"},{"key":"9407_CR20","doi-asserted-by":"crossref","unstructured":"Dilkina, B., Gomes, C.P., Sabharwal, A.: Backdoors in the context of learning. In: SAT-09: 12th International Conference on Theory and Applications of Satisfiability Testing, volume 5584 of LNCS, pp. 73\u201379 (2009)","DOI":"10.1007\/978-3-642-02777-2_9"},{"issue":"3","key":"9407_CR21","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","volume":"1","author":"WF Dowling","year":"1984","unstructured":"Dowling, W.F., Gallier, J.H.: Linear-time algorithms for testing the satisfiability of propositional horn formulae. J. Log. Program. 1(3), 267\u2013284 (1984)","journal-title":"J. Log. Program."},{"key":"9407_CR22","doi-asserted-by":"crossref","unstructured":"Downey, R.G., Fellows, M.R.: Parameterized Complexity (Monographs in Computer Science). Springer (1998). ISBN 978-0387948836","DOI":"10.1007\/978-1-4612-0515-9"},{"key":"9407_CR23","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: MiniSat: a SAT solver with conflict-clause minimization. In: SAT-05: 8th International Conference on Theory and Applications of Satisfiability Testing (2005)"},{"key":"9407_CR24","doi-asserted-by":"crossref","first-page":"290","DOI":"10.5486\/PMD.1959.6.3-4.12","volume":"6","author":"P Erdos","year":"1959","unstructured":"Erdos, P., Renyi, A.: On random graphs. Publicationes Mathemticae (Debrecen) 6, 290\u2013297 (1959)","journal-title":"Publicationes Mathemticae (Debrecen)"},{"key":"9407_CR25","doi-asserted-by":"crossref","unstructured":"Fichte, J.K., Szeider, S.: Backdoors to normality for disjunctive logic programs. In: AAAI-13: 27th Conference on Artificial Intelligence (2013)","DOI":"10.1609\/aaai.v27i1.8624"},{"key":"9407_CR26","unstructured":"Flum, J., Grohe, M.: Parameterized Complexity Theory. Springer (2006). ISBN 9783642067570"},{"issue":"1","key":"9407_CR27","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1145\/322290.322292","volume":"29","author":"EC Freuder","year":"1982","unstructured":"Freuder, E.C.: A sufficient condition for backtrack-free search. J. ACM 29(1), 24\u201332 (1982)","journal-title":"J. ACM"},{"issue":"4","key":"9407_CR28","doi-asserted-by":"crossref","first-page":"755","DOI":"10.1145\/4221.4225","volume":"32","author":"EC Freuder","year":"1985","unstructured":"Freuder, E.C.: A sufficient condition for backtrack-bounded search. J. ACM 32(4), 755\u2013761 (1985)","journal-title":"J. ACM"},{"key":"9407_CR29","unstructured":"Freuder, E. C.: Complexity of k-tree structured constraint satisfaction problems. In: AAAI-90: 8th National Conference on Artificial Intelligence, pp. 4\u20139 (1990)"},{"key":"9407_CR30","unstructured":"Gomes, C.P., Selman, B., Kautz, H.: Boosting combinatorial search through randomization. In: AAAI-98: 15th National Conference on Artificial Intelligence, pp. 431\u2013437 (1998)"},{"issue":"1\u20132","key":"9407_CR31","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1023\/A:1006314320276","volume":"24","author":"CP Gomes","year":"2000","unstructured":"Gomes, C.P., Selman, B., Crato, N., Kautz, H.: Heavy-tailed phenomena in satisfiability and constraint satisfaction problems. J. Autom. Reason. 24(1\u20132), 67\u2013100 (2000)","journal-title":"J. Autom. Reason."},{"key":"9407_CR32","doi-asserted-by":"crossref","first-page":"590","DOI":"10.1145\/321850.321857","volume":"21","author":"L Henschen","year":"1974","unstructured":"Henschen, L., Wos, L.: Unit refutations and Horn sets. J. ACM 21, 590\u2013605 (1974)","journal-title":"J. ACM"},{"key":"9407_CR33","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Gomes, C., Selman, B.: Structure and problem hardness: Goal asymmetry and DPLL proofs in SAT-based planning. Logical Methods Comput. Sci. 3(1\u20136), 1\u201341 (2007)","DOI":"10.2168\/LMCS-3(1:6)2007"},{"key":"9407_CR34","unstructured":"Hoos, H.H., St\u00fctzle, T.: SATLIB: an online resource for research on SAT. In: Gent, I.P., van Maaren, H., Walsh, W (eds.) SAT2000, pp. 283\u2013292. IOS Press (2000). http:\/\/www.satlib.org"},{"key":"9407_CR35","unstructured":"ILOG, SA. CPLEX 10.1 Reference Manual (2006)"},{"key":"9407_CR36","unstructured":"Kautz, H.A., Selman, B.: Planning as satisfiability. In: ECAI-92: 10th European Conference on Artificial Intelligence, pp. 359\u2013363 (1992)"},{"key":"9407_CR37","unstructured":"Kautz, H.A., Selman, B.: Pushing the envelope: planning, propositional logic, and stochastic search. In: AAAI-96: 13th Conference on Artificial Intelligence, pp. 1194\u20131201 (1996)"},{"key":"9407_CR38","unstructured":"Kearns, M.J., Littman, M.L., Singh, S.P.: Graphical models for game theory. In: UAI-01: 17th Conference on Uncertainty in Artificial Intelligence, pp. 253\u2013260 (2001)"},{"key":"9407_CR39","unstructured":"Kilby, P., Slaney, J.K., Thi\u00e9baux, S., Walsh, T.: Backbones and backdoors in satisfiability. In: AAAI-05: 20th National Conference on Artificial Intelligence, pp. 1368\u20131373 (2005)"},{"key":"9407_CR40","doi-asserted-by":"crossref","unstructured":"Kottler, S., Kaufmann, M., Sinz, C.: Computation of renameable horn backdoors. In: SAT\u201908: 11th International Conference on Theory and Applications of Satisfiability Testing, pp. 154\u2013160 (2008)","DOI":"10.1007\/978-3-540-79719-7_15"},{"issue":"1","key":"9407_CR41","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1145\/322047.322059","volume":"25","author":"HR Lewis","year":"1978","unstructured":"Lewis, H.R.: Renaming a set of clauses as a Horn set. J. ACM 25(1), 134\u2013135 (1978)","journal-title":"J. ACM"},{"key":"9407_CR42","unstructured":"Li, C.M., Anbulagan: Heuristics based on unit propagation for satisfiability problems. In: IJCAI-97: 15th International Joint Conference on Artificial Intelligence, pp. 366\u2013371 (1997)"},{"key":"9407_CR43","doi-asserted-by":"crossref","unstructured":"Lynce, I., Marques-Silva, J.P.: Hidden structure in unsatisfiable random 3-SAT: an empirical study. In: ICTAI-06: 16th IEEE International Conference on Tools with Artificial Intelligence, pp. 246\u2013251 (2004)","DOI":"10.1109\/ICTAI.2004.68"},{"key":"9407_CR44","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP\u2013a new search algorithm for satisfiability. In: ICCAD-96: International Conference on Computer Aided Design, pp. 220\u2013227 (1996)","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"9407_CR45","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of DAC-01: 38th Design Automation Conference, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"9407_CR46","doi-asserted-by":"crossref","first-page":"289","DOI":"10.2307\/1969529","volume":"54","author":"J Nash","year":"1951","unstructured":"Nash, J.: Noncooperative games. Ann. Math. 54, 289\u2013295 (1951)","journal-title":"Ann. Math."},{"key":"9407_CR47","unstructured":"Nishimura, N., Ragde, P., Szeider, S.: Detecting backdoor sets with respect to Horn and binary clauses. In: SAT-04: 7th International Conference on Theory and Applications of Satisfiability Testing (2004)"},{"key":"9407_CR48","doi-asserted-by":"crossref","unstructured":"Nishimura, N., Ragde, P., Szeider, S.: Solving #SAT using vertex covers. In: SAT-06: 9th International Conference on Theory and Applications of Satisfiability Testing, pp. 396\u2013409 (2006)","DOI":"10.1007\/11814948_36"},{"key":"9407_CR49","doi-asserted-by":"crossref","unstructured":"Paris, L., Ostrowski, R., Siegel, P., Sais, L.: Computing Horn strong backdoor sets thanks to local search. In: ICTAI-06: 17th IEEE International Conference on Tools with Artificial Intelligence, pp. 139\u2013143 (2006)","DOI":"10.1109\/ICTAI.2006.43"},{"key":"9407_CR50","unstructured":"Pfandler, A., R\u00fcmmele, S., Szeider, S.: Backdoors to abduction. In: IJCAI: International Joint Conference on Artificial Intelligence, pp. 1046\u20131052 (2013)"},{"key":"9407_CR51","unstructured":"Pipatsrisawat, K., Darwiche, A.: RS at 2.0: SAT solver description. Technical Report D\u2013153, Automated Reasoning Group, Computer Science Department, UCLA (2007)"},{"key":"9407_CR52","doi-asserted-by":"crossref","unstructured":"Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning SAT solvers with restarts. In CP-09: 15th International Conference on Principles and Practice of Constraint Programming, volume 5732 of LNCS, pp. 654\u2013668 (2009)","DOI":"10.1007\/978-3-642-04244-7_51"},{"issue":"8","key":"9407_CR53","doi-asserted-by":"crossref","first-page":"435","DOI":"10.1016\/j.jcss.2009.04.002","volume":"75","author":"I Razgon","year":"2009","unstructured":"Razgon, I., O\u2019Sullivan, B.: Almost 2-sat is fixed-parameter tractable. J. Comput. Syst. Sci. 75(8), 435\u2013450 (2009)","journal-title":"J. Comput. Syst. Sci."},{"key":"9407_CR54","doi-asserted-by":"crossref","unstructured":"Samer, M., Szeider, S.: Constraint satisfaction with bounded treewidth revisited. In: CP-06: 12th International Conference on Principles and Practice of Constraint Programming, pp. 499\u2013513 (2006)","DOI":"10.1007\/11889205_36"},{"issue":"1","key":"9407_CR55","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/s10817-008-9114-5","volume":"42","author":"M Samer","year":"2009","unstructured":"Samer, M., Szeider, S.: Backdoor sets of quantified boolean formulas. J. Autom. Reason. 42(1), 77\u201397 (2009)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"9407_CR56","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1017\/S0890060403171065","volume":"17","author":"C Sinz","year":"2003","unstructured":"Sinz, C., Kaiser, A., K\u00fcchlin, W.: Formal methods for the validation of automotive product configuration data. Artif. Intell. Eng. Des, Anal. Manuf. 17(1), 75\u201397 (2003). Special issue on configuration","journal-title":"Artif. Intell. Eng. Des, Anal. Manuf."},{"issue":"1\u20133","key":"9407_CR57","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":"3","key":"9407_CR58","doi-asserted-by":"crossref","first-page":"543","DOI":"10.1145\/210346.210347","volume":"42","author":"P Beek van","year":"1995","unstructured":"van Beek, P., Dechter, R.: On the minimality and global consistency of row-convex constraint networks. J. ACM 42(3), 543\u2013561 (1995)","journal-title":"J. ACM"},{"key":"9407_CR59","unstructured":"Williams, R., Gomes, C., Selman, B.: Backdoors to typical case complexity. In: IJCAI-03: 18th International Joint Conference on Artificial Intelligence, pp. 1173\u20131178 (2003)"},{"key":"9407_CR60","unstructured":"Williams, R., Gomes, C., Selman, B.: On the connections between heavy-tails, backdoors, and restarts in combinatorial search. In SAT-03: 6th International Conference on Theory and Applications of Satisfiability Testing, pp. 222\u2013230 (2003)"},{"key":"9407_CR61","unstructured":"Zhang, L., Madigan, C.F., Moskewicz, M.H., Malik, S.: Efficient conflict driven learning in a Boolean satisfiability solver. In: ICCAD-01: International Conference on Computer Aided Design, pp. 279\u2013285 (2001)"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-014-9407-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-014-9407-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-014-9407-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,11]],"date-time":"2023-07-11T07:24:37Z","timestamp":1689060277000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-014-9407-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,3,15]]},"references-count":61,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,4]]}},"alternative-id":["9407"],"URL":"https:\/\/doi.org\/10.1007\/s10472-014-9407-9","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,3,15]]}}}