[Back]

M. Heule, S. Szeider:
"A SAT Approach to Clique-Width";
ACM Transactions on Computational Logic, 16/3 (2015), 1 - 27.

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 proposi- tional 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.

http://dx.doi.org/10.1145/2736696