{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,25]],"date-time":"2026-06-25T15:14:23Z","timestamp":1782400463642,"version":"3.54.5"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540208518","type":"print"},{"value":"9783540246053","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24605-3_24","type":"book-chapter","created":{"date-parts":[[2010,7,29]],"date-time":"2010-07-29T08:50:35Z","timestamp":1280393435000},"page":"315-329","source":"Crossref","is-referenced-by-count":11,"title":["Guiding SAT Diagnosis with Tree Decompositions"],"prefix":"10.1007","author":[{"given":"Per","family":"Bjesse","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"James","family":"Kukula","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Robert","family":"Damiano","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ted","family":"Stanion","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yunshan","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"Aloul, F., Markov, I., Sakallah, K.: Faster SAT and Smaller BDDs via Common Function Structure. In: Proc. Intl. Conf. on Computer-Aided Design, pp. 443\u2013 448 (2001)","DOI":"10.1109\/ICCAD.2001.968669"},{"key":"24_CR2","unstructured":"Amir, E.: Efficient Approximation for Triangulation of Minimum Treewidth. In: Proc. Conf. on Uncertainty in Artificial Intelligence (2001)"},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"Amir, E., McIlraith, S.: Solving satisfiability using decomposition and the most constrained subproblem. In: Proc. Workshop on Theory and Applications of Satisfiability Testing (2001)","DOI":"10.1016\/S1571-0653(04)00331-2"},{"key":"24_CR4","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/BF01934985","volume":"25","author":"S. Arnborg","year":"1985","unstructured":"Arnborg, S.: Efficient Algorithms for Combinatorial Problems on Graphs with Bounded Decomposability - A Survey. BIT\u00a025, 2\u201323 (1985)","journal-title":"BIT"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"Arnborg, S., Corneil, D.G., Proskurowski, A.: Complexity of finding embeddings in a k-tree. SIAM Journal of Algebraic and Discrete Methods\u00a0(8) (1987)","DOI":"10.1137\/0608024"},{"key":"24_CR6","unstructured":"Bodlaender, H.: A Tourist Guide through Treewidth. Acta Cybernetica\u00a011 (1993)"},{"key":"24_CR7","doi-asserted-by":"crossref","unstructured":"Bodlaender, H.: A linear time algorithm for finding tree-decompositions of small treewidth. In: Proc. ACM Symposium on the Theory of Computing (1993)","DOI":"10.1145\/167088.167161"},{"key":"24_CR8","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1006\/jagm.1995.1009","volume":"18","author":"H. Bodlaender","year":"1995","unstructured":"Bodlaender, H., Gilbert, J., Hafsteinsson, H., Kloks, T.: Approximating Treewidth, Pathwidth, Frontsize, and Shortest Elimination Tree. Journal of Algorithms\u00a018, 155\u2013238 (1995)","journal-title":"Journal of Algorithms"},{"key":"24_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"56","DOI":"10.1007\/3-540-62222-5_36","volume-title":"Database Theory - ICDT \u201997","author":"C. Chekuri","year":"1996","unstructured":"Chekuri, C., Rajaraman, A.: Conjunctive query containment revisited. In: Afrati, F.N., Kolaitis, P.G. (eds.) ICDT 1997. LNCS, vol.\u00a01186, pp. 56\u201370. Springer, Heidelberg (1996)"},{"key":"24_CR10","unstructured":"Darwiche, A.: Compiling knowledge into decomposable negation normal form. In: Proc. Intl. Joint Conf. on Artificial Intelligence (1999)"},{"key":"24_CR11","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logeman, G., Loveland, D.: A machine program for theorem-proving. Communications of the ACM\u00a05, 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"issue":"1","key":"24_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(87)90002-6","volume":"34","author":"R. Dechter","year":"1988","unstructured":"Dechter, R., Pearl, J.: Network-based heuristics for constraint-satisfaction problems. Artificial Intelligence\u00a034(1), 1\u201334 (1988)","journal-title":"Artificial Intelligence"},{"key":"24_CR13","doi-asserted-by":"crossref","unstructured":"Gupta, A., Yang, Z., Ashar, P., Zhang, L., Malik, S.: Partition-Based Decision Heuristics for Image Computation using SAT and BDDs. In: Proc. Intl. Conf. on Computer-Aided Design, pp. 286\u2013292 (2001)","DOI":"10.1109\/ICCAD.2001.968635"},{"key":"24_CR14","unstructured":"Huang, J., Darwiche, A.: A structure-based variable ordering heuristic for SAT. In: Proc. Intl. Joint Conf. on Artificial Intelligence (2003)"},{"key":"24_CR15","unstructured":"The Second DIMACS Implementation Challenge. In: Johnson, D., Trick, M. (eds.). DIMACS series in Discrete Mathematics and Theoretical Computer Science, American Mathematical Society, Providence (1993), http:\/\/dimacs.rutgers.edu\/challenges\/"},{"key":"24_CR16","doi-asserted-by":"crossref","unstructured":"Marques Silva, J.P., Sakallah, K.A.: GRASP\u2014a new search algorithm for satisfiability. In: Proc. Intl. Conf. on Computer-Aided Design, pp. 220\u2013227 (1996)","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT-solver. In: Proc. of the Design Automation Conf. (2001)","DOI":"10.1145\/378239.379017"},{"key":"24_CR18","doi-asserted-by":"crossref","unstructured":"Prasad, M., Chong, P., Keutzer, K.: Why is ATPG easy? In: Proc. of the Design Automation Conf. (1999)","DOI":"10.1145\/309847.309857"},{"key":"24_CR19","unstructured":"Roehrig, H.: Tree Decomposition: A Feasibility Study. M.S. Thesis, Max-Planck- Instit. Inform. Saarbruecken (1998)"},{"key":"24_CR20","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1016\/0012-365X(74)90042-9","volume":"7","author":"D. Rose","year":"1974","unstructured":"Rose, D.: Triangulated Graphs and the Elimination Process. J. of Discrete Mathematics\u00a07, 317\u2013322 (1974)","journal-title":"J. of Discrete Mathematics"},{"issue":"1","key":"24_CR21","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1137\/0134014","volume":"34","author":"D. Rose","year":"1978","unstructured":"Rose, D., Tarjan, R.: Algorithmic Aspects of Vertex Elimination on Directed Graphs. SIAM J. Appl. Math.\u00a034(1), 176\u2013197 (1978)","journal-title":"SIAM J. Appl. Math."},{"key":"24_CR22","doi-asserted-by":"crossref","unstructured":"Zhang, L., Madigan, C., Moskewicz, M., Malik, S.: Efficient conflict driven learning in a boolean satisfiability solver. In: Proc. Intl. Conf. on Computer-Aided Design (2001)","DOI":"10.1145\/774572.774637"},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: The quest for efficient boolean satisfiability solvers. In: Proc. of the Computer Aided Verification Conf. (2002)","DOI":"10.1007\/3-540-45657-0_2"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24605-3_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,2]],"date-time":"2021-11-02T07:56:19Z","timestamp":1635839779000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24605-3_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540208518","9783540246053"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24605-3_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}