{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,16]],"date-time":"2025-12-16T12:21:35Z","timestamp":1765887695099,"version":"3.41.0"},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2015,6,2]],"date-time":"2015-06-02T00:00:00Z","timestamp":1433203200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["239962"],"award-info":[{"award-number":["239962"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006502","name":"Defense Sciences Office, DARPA","doi-asserted-by":"publisher","award":["N66001-10-2-4087"],"award-info":[{"award-number":["N66001-10-2-4087"]}],"id":[{"id":"10.13039\/100006502","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-0910913"],"award-info":[{"award-number":["CNS-0910913"]}],"id":[{"id":"10.13039\/100000001","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":[[2015,7,8]]},"abstract":"<jats:p>Clique-width is a graph invariant that has been widely studied in combinatorics and computational logic. Computing the clique-width of a graph is an intricate problem, because the exact clique-width is not known even for very small graphs. We present a new method for computing clique-width via an encoding to propositional satisfiability (SAT), which is then evaluated by a SAT solver. Our encoding is based on a reformulation of clique-width in terms of partitions that utilizes an efficient encoding of cardinality constraints. Our SAT-based method is the first to discover the exact clique-width of various small graphs, including famous named graphs from the literature as well as random graphs of various density. With our method, we determined the smallest graphs that require a small predescribed clique-width. We further show how our method can be modified to compute the linear clique-width of graphs, a variant of clique-width that has recently received considerable attention. In an appendix, we provide certificates for tight upper bounds for the clique-width and linear clique-width of famous named graphs.<\/jats:p>","DOI":"10.1145\/2736696","type":"journal-article","created":{"date-parts":[[2015,6,2]],"date-time":"2015-06-02T18:19:47Z","timestamp":1433269187000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["A SAT Approach to Clique-Width"],"prefix":"10.1145","volume":"16","author":[{"given":"Marijn J. H.","family":"Heule","sequence":"first","affiliation":[{"name":"Department of Computer Sciences, The University of Texas at Austin, Austin, Texas, United States"}]},{"given":"Stefan","family":"Szeider","sequence":"additional","affiliation":[{"name":"Institute of Computer Graphics and Algorithms, TU Wien, Vienna, Austria"}]}],"member":"320","published-online":{"date-parts":[[2015,6,2]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-45043-3_3"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/1661445.1661509"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36046-6_9"},{"key":"e_1_2_1_4_1","volume-title":"Lingeling and friends entering the SAT Challenge","author":"Biere Armin","year":"2012","unstructured":"Armin Biere . 2012. Lingeling and friends entering the SAT Challenge 2012 . In Solver and Benchmark Descriptions (Department of Computer Science Series of Publications B.) , A. Balint, A. Belov, A. Diepold, S. Gerber, M. J\u00e4rvisalo, and C. Sinz (Eds.), Vol. B-2012-2. University of Helsinki, 33--34. Armin Biere. 2012. Lingeling and friends entering the SAT Challenge 2012. In Solver and Benchmark Descriptions (Department of Computer Science Series of Publications B.), A. Balint, A. Belov, A. Diepold, S. Gerber, M. J\u00e4rvisalo, and C. Sinz (Eds.), Vol. B-2012-2. University of Helsinki, 33--34."},{"key":"e_1_2_1_5_1","volume-title":"Frontiers in Artificial Intelligence and Applications","volume":"185","author":"Biere Armin","year":"2009","unstructured":"Armin Biere , Marijn Heule , Hans van Maaren , and Toby Walsh ( Eds .). 2009 . Handbook of Satisfiability . Frontiers in Artificial Intelligence and Applications , Vol. 185 . IOS Press. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh (Eds.). 2009. Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, Vol. 185. IOS Press."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.05.022"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.dam.2011.03.020"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539701385351"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/647561.730653"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(93)90004-G"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s002249910009"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0166-218X(00)00221-3"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0166-218X(99)00184-5"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-009-9211-9"},{"key":"e_1_2_1_15_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_16_1","volume-title":"Korf","author":"Alex Dow P.","year":"2007","unstructured":"P. Alex Dow and Richard E . Korf . 2007 . Best-first search for treewidth. In Proceedings of the 22nd AAAI Conference on Artificial Intelligence. AAAI Press , 1146--1151. P. Alex Dow and Richard E. Korf. 2007. Best-first search for treewidth. In Proceedings of the 22nd AAAI Conference on Artificial Intelligence. AAAI Press, 1146--1151."},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of 2013 6th European Lisp Symposium (ELS\u201913)","author":"Durand Ir\u00e9ne","year":"2013","unstructured":"Ir\u00e9ne Durand and Bruno Courcelle . 2013 . Infinite transducers on terms denoting graphs . In Proceedings of 2013 6th European Lisp Symposium (ELS\u201913) . 47--58. Retrieved from http:\/\/www.nicklevine.org\/els 2013\/proceedings.pdf. Ir\u00e9ne Durand and Bruno Courcelle. 2013. Infinite transducers on terms denoting graphs. In Proceedings of 2013 6th European Lisp Symposium (ELS\u201913). 47--58. Retrieved from http:\/\/www.nicklevine.org\/els2013\/proceedings.pdf."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1137\/070687256"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/1758481.1758507"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/3000905.3000932"},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the Proceedings of the 29th Conference Annual Conference on Uncertainty in Artificial Intelligence (UAI-04)","author":"Gogate Vibhav","year":"2004","unstructured":"Vibhav Gogate and Rina Dechter . 2004 . A complete anytime algorithm for treewidth . In Proceedings of the Proceedings of the 29th Conference Annual Conference on Uncertainty in Artificial Intelligence (UAI-04) . AUAI Press, Arlington, VA, 201--208. Vibhav Gogate and Rina Dechter. 2004. A complete anytime algorithm for treewidth. In Proceedings of the Proceedings of the 29th Conference Annual Conference on Uncertainty in Artificial Intelligence (UAI-04). AUAI Press, Arlington, VA, 201--208."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054100000260"},{"volume-title":"Handbook of Knowledge Representation. Foundations of Artificial Intelligence","author":"Gomes Carla P.","key":"e_1_2_1_24_1","unstructured":"Carla P. Gomes , Henry Kautz , Ashish Sabharwal , and Bart Selman . 2008. Satisfiability solvers . In Handbook of Knowledge Representation. Foundations of Artificial Intelligence , Vol. 3 . Elsevier , 89--134. Carla P. Gomes, Henry Kautz, Ashish Sabharwal, and Bart Selman. 2008. Satisfiability solvers. In Handbook of Knowledge Representation. Foundations of Artificial Intelligence, Vol. 3. Elsevier, 89--134."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.05.018"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cosrev.2010.01.001"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.06.016"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.dam.2011.03.018"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/2017990.2018008"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28050-4_18"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28717-6_20"},{"key":"e_1_2_1_32_1","volume-title":"Marques-Silva","author":"Katebi Hadi","year":"2011","unstructured":"Hadi Katebi , Karem A. Sakallah , and Jo\u00e3o P . Marques-Silva . 2011 . Empirical study of the anatomy of modern sat solvers. In Proceedings of the 14th International Conference on Theory and Application of Satisfiability Testing. Springer-Verlag , 343--356. Hadi Katebi, Karem A. Sakallah, and Jo\u00e3o P. Marques-Silva. 2011. Empirical study of the anatomy of modern sat solvers. In Proceedings of the 14th International Conference on Theory and Application of Satisfiability Testing. Springer-Verlag, 343--356."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0653(05)80078-2"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1002\/jgt.20620"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jctb.2007.04.001"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1536616.1536637"},{"key":"e_1_2_1_37_1","volume-title":"Proceedings of the Tenth Manitoba Conference on Numerical Mathematics and Computing","author":"McKay Brendan D.","year":"1981","unstructured":"Brendan D. McKay . 1981 . Practical graph isomorphism , In Proceedings of the Tenth Manitoba Conference on Numerical Mathematics and Computing , Vol. I (Winnipeg, Man. , 1980). Congr. Numer. 30 (1981), 45--87. Brendan D. McKay. 1981. Practical graph isomorphism, In Proceedings of the Tenth Manitoba Conference on Numerical Mathematics and Computing, Vol. I (Winnipeg, Man., 1980). Congr. Numer. 30 (1981), 45--87."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jctb.2005.10.006"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1435375.1435385"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02777-2_6"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/11564751_73"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10589-011-9397-z"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-008-9061-0"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-010-9261-z"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/647487.726638"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/0166-218X(94)90026-4"},{"key":"e_1_2_1_47_1","volume-title":"MathWorld Online Mathematics Resource. Last accessed on","author":"Weisstein Eric","year":"2015","unstructured":"Eric Weisstein . 2015. MathWorld Online Mathematics Resource. Last accessed on February 13, 2015 . http:\/\/mathworld.wolfram.com\/. Eric Weisstein. 2015. MathWorld Online Mathematics Resource. Last accessed on February 13, 2015. http:\/\/mathworld.wolfram.com\/."},{"volume-title":"Handbook of Satisfiability, Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh (Eds.). Frontiers in Artificial Intelligence and Applications","author":"Zhang Hantao","key":"e_1_2_1_48_1","unstructured":"Hantao Zhang . 2009. Combinatorial designs by SAT solvers . In Handbook of Satisfiability, Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh (Eds.). Frontiers in Artificial Intelligence and Applications , Vol. 185 . IOS Press , 533--568. Hantao Zhang. 2009. Combinatorial designs by SAT solvers. In Handbook of Satisfiability, Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh (Eds.). Frontiers in Artificial Intelligence and Applications, Vol. 185. IOS Press, 533--568."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2736696","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2736696","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:12:30Z","timestamp":1750227150000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2736696"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,6,2]]},"references-count":48,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2015,7,8]]}},"alternative-id":["10.1145\/2736696"],"URL":"https:\/\/doi.org\/10.1145\/2736696","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2015,6,2]]},"assertion":[{"value":"2014-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-06-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}