2015/06/02 by Marijn J. H. Heule, Stefan Szeider · 25 citations
Computer Science · Mathematics · #Advanced Graph Theory Research #semigroups and automata theory #Formal Methods in Verification #Clique problem #Combinatorics #Mathematics #Treewidth #Clique graph #Clique #Split graph #Clique-sum #Discrete mathematics #Cardinality (data modeling) #Chordal graph #Graph #Pathwidth #Computer science #1-planar graph #Line graph #Graph power
paper · doi:10.1145/2736696
published in ACM Transactions on Computational Logic 16(3), 1-27 (Association for Computing Machinery)
openalex publication_date 2015/06/02 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/06
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.