{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T09:40:24Z","timestamp":1766137224587,"version":"3.41.0"},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T00:00:00Z","timestamp":1559260800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["W1255-N23 and P-27721"],"award-info":[{"award-number":["W1255-N23 and P-27721"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2019,7,31]]},"abstract":"<jats:p>Branch decomposition is a prominent method for structurally decomposing a graph, a hypergraph, or a propositional formula in conjunctive normal form. The width of a branch decomposition provides a measure of how well the object is decomposed. For many applications, it is crucial to computing a branch decomposition whose width is as small as possible. We propose an approach based on Boolean Satisfiability (SAT) to finding branch decompositions of small width. The core of our approach is an efficient SAT encoding that determines with a single SAT-call whether a given hypergraph admits a branch decomposition of a certain width. For our encoding, we propose a natural partition-based characterization of branch decompositions. The encoding size imposes a limit on the size of the given hypergraph. To break through this barrier and to scale the SAT approach to larger instances, we develop a new heuristic approach where the SAT encoding is used to locally improve a given candidate decomposition until a fixed-point is reached. This new SAT-based local improvement method scales now to instances with several thousands of vertices and edges.<\/jats:p>","DOI":"10.1145\/3326159","type":"journal-article","created":{"date-parts":[[2019,6,3]],"date-time":"2019-06-03T12:23:16Z","timestamp":1559564596000},"page":"1-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["A SAT Approach to Branchwidth"],"prefix":"10.1145","volume":"20","author":[{"given":"Neha","family":"Lodha","sequence":"first","affiliation":[{"name":"Algorithms and Complexity Group, Faculty of Informatics, TU Wien, Vienna, Austria"}]},{"given":"Sebastian","family":"Ordyniak","sequence":"additional","affiliation":[{"name":"Algorithms and Complexity Group, Faculty of Informatics, TU Wien, Vienna, Austria"}]},{"given":"Stefan","family":"Szeider","sequence":"additional","affiliation":[{"name":"Algorithms and Complexity Group, Faculty of Informatics, TU Wien, Vienna, Austria"}]}],"member":"320","published-online":{"date-parts":[[2019,5,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939238.1939256"},{"volume-title":"Proceedings of the 43rd Symposium on Foundations of Computer Science (FOCS\u201902)","author":"Alekhnovich Michael","key":"e_1_2_1_2_1","unstructured":"Michael Alekhnovich and Alexander A. Razborov . 2002. Satisfiability, branch-width and Tseitin tautologies . In Proceedings of the 43rd Symposium on Foundations of Computer Science (FOCS\u201902) . IEEE Computer Society, 593--603. Michael Alekhnovich and Alexander A. Razborov. 2002. Satisfiability, branch-width and Tseitin tautologies. In Proceedings of the 43rd Symposium on Foundations of Computer Science (FOCS\u201902). IEEE Computer Society, 593--603."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/946243.946291"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the 16th International Symposium on Experimental Algorithms (SEA\u201917)","volume":"75","author":"Bannach Max","year":"2017","unstructured":"Max Bannach , Sebastian Berndt , and Thorsten Ehlers . 2017 . Jdrasil: A modular library for computing tree decompositions . In Proceedings of the 16th International Symposium on Experimental Algorithms (SEA\u201917) , Costas S. Iliopoulos, Solon P. Pissis, Simon J. Puglisi, and Rajeev Raman (Eds.) , Vol. 75 . Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 28:1--28:21. Max Bannach, Sebastian Berndt, and Thorsten Ehlers. 2017. Jdrasil: A modular library for computing tree decompositions. In Proceedings of the 16th International Symposium on Experimental Algorithms (SEA\u201917), Costas S. Iliopoulos, Solon P. Pissis, Simon J. Puglisi, and Rajeev Raman (Eds.), Vol. 75. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 28:1--28:21."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICTAI.2014.57"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43948-7_17"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2261250.2261257"},{"key":"e_1_2_1_8_1","unstructured":"Hans Bodlander. 2016. TreewidthLIB: A benchmark for algorithms for Treewidth and related graph problems. Retrieved from http:\/\/www.staff.science.uu.nl\/ bodla101\/treewidthlib\/.  Hans Bodlander. 2016. TreewidthLIB: A benchmark for algorithms for Treewidth and related graph problems. Retrieved from http:\/\/www.staff.science.uu.nl\/ bodla101\/treewidthlib\/."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1287\/ijoc.15.3.233.16078"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898717105"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90043-H"},{"volume-title":"Modeling and Reasoning with Bayesian Networks","author":"Darwiche Adnan","key":"e_1_2_1_12_1","unstructured":"Adnan Darwiche . 2009. Modeling and Reasoning with Bayesian Networks . Cambridge University Press . I--XII, 1--548 pages. Adnan Darwiche. 2009. Modeling and Reasoning with Bayesian Networks. Cambridge University Press. I--XII, 1--548 pages."},{"key":"e_1_2_1_13_1","volume-title":"Graph Theory","author":"Diestel Reinhard","unstructured":"Reinhard Diestel . 2000. Graph Theory ( 2 nd ed.). Graduate Texts in Mathematics, Vol. 173 . Springer Verlag , New York. Reinhard Diestel. 2000. Graph Theory (2nd ed.). Graduate Texts in Mathematics, Vol. 173. Springer Verlag, New York.","edition":"2"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24318-4_16"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66263-3_25"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.dam.2008.08.009"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1137\/1.9781611975499.10"},{"volume-title":"Logic and Automata: History and Perspectives (Texts in Logic and Games), J\u00f6rg Flum, Erich Gr\u00e4del","author":"Grohe Martin","key":"e_1_2_1_18_1","unstructured":"Martin Grohe . 2008. Logic, graphs, and algorithms . In Logic and Automata: History and Perspectives (Texts in Logic and Games), J\u00f6rg Flum, Erich Gr\u00e4del , and Thomas Wilke (Eds.), Vol. 2 . Amsterdam University Press , 357--422. Martin Grohe. 2008. Logic, graphs, and algorithms. In Logic and Automata: History and Perspectives (Texts in Logic and Games), J\u00f6rg Flum, Erich Gr\u00e4del, and Thomas Wilke (Eds.), Vol. 2. Amsterdam University Press, 357--422."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1367064.1367070"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2736696"},{"key":"e_1_2_1_21_1","volume-title":"Congr. Numer. 159","author":"Hicks I. V.","year":"2002","unstructured":"I. V. Hicks . 2002 . Branchwidth heuristics . Congr. Numer. 159 (2002), 31--50. I. V. Hicks. 2002. Branchwidth heuristics. Congr. Numer. 159 (2002), 31--50."},{"key":"e_1_2_1_22_1","volume-title":"branchwidth, and tangles&excl","author":"Hicks Illya V.","year":"2005","unstructured":"Illya V. Hicks . 2005. Graphs , branchwidth, and tangles&excl ; Oh my&excl; Networks 45, 2 ( 2005 ), 55--60. Illya V. Hicks. 2005. Graphs, branchwidth, and tangles&excl; Oh my&excl; Networks 45, 2 (2005), 55--60."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1137\/070685920"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the 25th AAAI Conference on Artificial Intelligence (AAAI\u201911)","author":"Kask Kalev","year":"2011","unstructured":"Kalev Kask , Andrew Gelfand , Lars Otten , and Rina Dechter . 2011 . Pushing the power of stochastic greedy ordering schemes for inference in graphical models . In Proceedings of the 25th AAAI Conference on Artificial Intelligence (AAAI\u201911) , Wolfram Burgard and Dan Roth (Eds.). AAAI Press. Kalev Kask, Andrew Gelfand, Lars Otten, and Rina Dechter. 2011. Pushing the power of stochastic greedy ordering schemes for inference in graphical models. In Proceedings of the 25th AAAI Conference on Artificial Intelligence (AAAI\u201911), Wolfram Burgard and Dan Roth (Eds.). AAAI Press."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66263-3_27"},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of the 37th Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM\u201911)","volume":"6543","author":"Overwijk Arnold","unstructured":"Arnold Overwijk , Eelko Penninkx , and Hans L. Bodlaender . 2011. A local search algorithm for branchwidth . In Proceedings of the 37th Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM\u201911) (Lecture Notes in Computer Science), Ivana Cern\u00e1, Tibor Gyim\u00f3thy, Juraj Hromkovic, Keith G. Jeffery, Rastislav Kr\u00e1lovic, Marko Vukolic, and Stefan Wolf (Eds.) , Vol. 6543 . Springer, 444--454. Arnold Overwijk, Eelko Penninkx, and Hans L. Bodlaender. 2011. A local search algorithm for branchwidth. In Proceedings of the 37th Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM\u201911) (Lecture Notes in Computer Science), Ivana Cern\u00e1, Tibor Gyim\u00f3thy, Juraj Hromkovic, Keith G. Jeffery, Rastislav Kr\u00e1lovic, Marko Vukolic, and Stefan Wolf (Eds.), Vol. 6543. Springer, 444--454."},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the 21st European Conference on Artificial Intelligence (ECAI\u201914)","volume":"263","author":"Oztok Umut","year":"2014","unstructured":"Umut Oztok and Adnan Darwiche . 2014 . CV-width: A new complexity parameter for CNFs . In Proceedings of the 21st European Conference on Artificial Intelligence (ECAI\u201914) Including Prestigious Applications of Intelligent Systems (PAIS\u201914) (Frontiers in Artificial Intelligence and Applications), Torsten Schaub, Gerhard Friedrich, and Barry O\u2019Sullivan (Eds.) , Vol. 263 . IOS Press, 675--680. Umut Oztok and Adnan Darwiche. 2014. CV-width: A new complexity parameter for CNFs. In Proceedings of the 21st European Conference on Artificial Intelligence (ECAI\u201914) Including Prestigious Applications of Intelligent Systems (PAIS\u201914) (Frontiers in Artificial Intelligence and Applications), Torsten Schaub, Gerhard Friedrich, and Barry O\u2019Sullivan (Eds.), Vol. 263. IOS Press, 675--680."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/0095-8956(91)90061-N"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0095-8956(91)90061-N"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02777-2_6"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01215352"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10589-011-9397-z"},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the 11th International Conference on Algorithms and Computation (ISAAC\u201900)","volume":"1969","author":"Thilikos Dimitrios M.","unstructured":"Dimitrios M. Thilikos , Maria J. Serna , and Hans L. Bodlaender . 2000. Constructive linear time algorithms for small cutwidth and carving-width . In Proceedings of the 11th International Conference on Algorithms and Computation (ISAAC\u201900) (Lecture Notes in Computer Science), D. T. Lee and Shang-Hua Teng (Eds.) , Vol. 1969 . Springer, 192--203. Dimitrios M. Thilikos, Maria J. Serna, and Hans L. Bodlaender. 2000. Constructive linear time algorithms for small cutwidth and carving-width. In Proceedings of the 11th International Conference on Algorithms and Computation (ISAAC\u201900) (Lecture Notes in Computer Science), D. T. Lee and Shang-Hua Teng (Eds.), Vol. 1969. Springer, 192--203."},{"key":"e_1_2_1_35_1","unstructured":"Eric Weisstein. 2016. MathWorld online Mathematics resource. Retrieved from http:\/\/mathworld.wolfram.com.  Eric Weisstein. 2016. MathWorld online Mathematics resource. Retrieved from http:\/\/mathworld.wolfram.com."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3326159","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3326159","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:53:08Z","timestamp":1750204388000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3326159"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,5,31]]},"references-count":34,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,7,31]]}},"alternative-id":["10.1145\/3326159"],"URL":"https:\/\/doi.org\/10.1145\/3326159","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2019,5,31]]},"assertion":[{"value":"2018-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-05-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}