{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T19:10:02Z","timestamp":1748545802388,"version":"3.41.0"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319218397"},{"type":"electronic","value":"9783319218403"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21840-3_46","type":"book-chapter","created":{"date-parts":[[2015,7,27]],"date-time":"2015-07-27T09:57:38Z","timestamp":1437991058000},"page":"554-565","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A Moderately Exponential Time Algorithm for k-IBDD Satisfiability"],"prefix":"10.1007","author":[{"given":"Atsuki","family":"Nagao","sequence":"first","affiliation":[]},{"given":"Kazuhisa","family":"Seto","sequence":"additional","affiliation":[]},{"given":"Junichi","family":"Teruyama","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,28]]},"reference":[{"key":"46_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24587-2_19","volume-title":"Algorithms and Computation","author":"V Arvind","year":"2003","unstructured":"Arvind, V., Schuler, R.: The Quantum Query Complexity of 0-1 Knapsack and Associated Claw Problems. In: Ibaraki, T., Katoh, N., Ono, H. (eds.) ISAAC 2003. LNCS, vol. 2906, pp. 168\u2013177. Springer, Heidelberg (2003)"},{"key":"46_CR2","doi-asserted-by":"crossref","unstructured":"Bergroth, L., Hakonen, H., Raita, T.: A Survey of Longest Common Subsequence Algorithms. In: Proceedings of the 7th International Symposium on String Processing and Information Retrieval (SPIRE), pp. 39\u201348 (2000)","DOI":"10.1109\/SPIRE.2000.878178"},{"key":"46_CR3","unstructured":"Bollig, B., Sauerhoff, M., Sieling, D., Wegener, I.: On the Power of Different Types of Restricted Branching Programs. In: Electronic Colloquium on Computational Complexity (ECCC), vol. 1(26) (1994)"},{"issue":"8","key":"46_CR4","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based Algorithm for Boolean Function Manipulation. IEEE Transaction on Computers 35(8), 677\u2013691 (1986)","journal-title":"IEEE Transaction on Computers"},{"key":"46_CR5","doi-asserted-by":"crossref","unstructured":"Calabro, C., Impagliazzo, R., Paturi, R.: A Duality between Clause Width and Clause Density for SAT. In: Proceedings of the 21st Annual IEEE Conference Computational Complexity (CCC), pp. 252\u2013260 (2006)","DOI":"10.1109\/CCC.2006.6"},{"key":"46_CR6","doi-asserted-by":"crossref","unstructured":"Chen, R., Kabanets, V., Kolokolova, A., Shaltiel, R., Zuckerman, D.: Mining Circuit Lower Bound Proofs for Meta-Algorithms. In: Proceedings of the 29th Annual IEEE Conference on Computational Complexity (CCC), pp. 262\u2013273 (2014)","DOI":"10.1109\/CCC.2014.34"},{"key":"46_CR7","doi-asserted-by":"crossref","unstructured":"Dantsin, E., Hirsch, E.A., Wolpert, A.: Algorithms for SAT Based on Search in Hamming Balls. In: Proceedings of the 21st Annual Symposium on Theoretical Aspects of Computer Science (STACS), pp. 141\u2013151 (2004)","DOI":"10.1007\/978-3-540-24749-4_13"},{"key":"46_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/11758471_9","volume-title":"Algorithms and Complexity","author":"E Dantsin","year":"2006","unstructured":"Dantsin, E., Hirsch, E.A., Wolpert, A.: Clause Shortening Combined with Pruning Yields a New Upper Bound for Deterministic SAT Algorithms. In: Calamoneri, T., Finocchi, I., Italiano, G.F. (eds.) CIAC 2006. LNCS, vol. 3998, pp. 60\u201368. Springer, Heidelberg (2006)"},{"key":"46_CR9","first-page":"463","volume":"2","author":"P Erd\u0151s","year":"1935","unstructured":"Erd\u0151s, P., Szekeres, G.: A Combinatorial Problem in Geometry. Compositio Mathematica 2, 463\u2013470 (1935)","journal-title":"Compositio Mathematica"},{"key":"46_CR10","doi-asserted-by":"crossref","unstructured":"Hirsch, E.A.: Exact Algorithm for General CNF SAT, Encyclopedia of Algorithms. Springer (2008)","DOI":"10.1007\/978-0-387-30162-4_133"},{"key":"46_CR11","doi-asserted-by":"crossref","unstructured":"Impagliazzo, R., Matthews, W., Paturi, R.: A satisfiability algorithm for AC$$^{\\text{0 }}$$. In: Proceedings of the 23rd Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pp. 961\u2013972 (2012)","DOI":"10.1137\/1.9781611973099.77"},{"issue":"11","key":"46_CR12","doi-asserted-by":"publisher","first-page":"1230","DOI":"10.1109\/12.644298","volume":"46","author":"J Jain","year":"1997","unstructured":"Jain, J., Bitner, J., Abadir, M.S., Abraham, J.A., Fussell, D.S.: Indexed BDDs: Algorithmic Advances in Techniques to Represent and Verify Boolean Functions. IEEE Transaction on Computers 46(11), 1230\u20131245 (1997)","journal-title":"IEEE Transaction on Computers"},{"key":"46_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/BFb0055762","volume-title":"Mathematical Foundations of Computer Science 1998","author":"P Pudl\u00e1k","year":"1998","unstructured":"Pudl\u00e1k, P.: Satisfiability - Algorithms and Logic. In: Brim, L., Gruska, J., Zlatu\u0161ka, J. (eds.) MFCS 1998. LNCS, vol. 1450, pp. 129\u2013141. Springer, Heidelberg (1998)"},{"key":"46_CR14","doi-asserted-by":"crossref","unstructured":"Santhanam, R.: Fighting Perebor: New and Improved Algorithms for Formula and QBF Satisfiability. In: Proceedings of the 51st International Symposium on Foundations of Computer Science (FOCS), pp. 183\u2013192 (2010)","DOI":"10.1109\/FOCS.2010.25"},{"issue":"1","key":"46_CR15","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1016\/j.jalgor.2004.04.012","volume":"54","author":"R Schuler","year":"2005","unstructured":"Schuler, R.: An algorithm for the satisfiability problem of formulas in conjunctive normal form. J. Algorithms 54(1), 40\u201344 (2005)","journal-title":"J. Algorithms"},{"issue":"2","key":"46_CR16","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/s00037-013-0067-7","volume":"22","author":"K Seto","year":"2013","unstructured":"Seto, K., Tamaki, S.: A Satisfiability Algorithm and Average-Case Hardness for Formulas over the Full Binary Basis. Computational Complexity 22(2), 245\u2013274 (2013)","journal-title":"Computational Complexity"},{"key":"46_CR17","doi-asserted-by":"crossref","unstructured":"Wegener, I.: Branching Programs and Binary Decision Diagrams. SIAM Monographs on Discrete Mathematics and Applications (2000)","DOI":"10.1137\/1.9780898719789"}],"container-title":["Lecture Notes in Computer Science","Algorithms and Data Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21840-3_46","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T18:50:26Z","timestamp":1748544626000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21840-3_46"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319218397","9783319218403"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21840-3_46","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"28 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}