A SAT Approach to Clique-Width

TL;DR

This paper introduces a SAT-based method for computing the exact clique-width of graphs, enabling the analysis of small and complex graphs that were previously difficult to evaluate.

Contribution

It presents a novel SAT encoding for clique-width, allowing exact computation and discovery of minimal graphs with specified clique-width.

Findings

Successfully computed clique-width for various small graphs

Identified smallest graphs requiring specific clique-widths

First to use SAT for exact clique-width determination

Abstract

Clique-width is a graph invariant that has been widely studied in combinatorics and computer science. However, computing the clique-width of a graph is an intricate problem, the exact clique-width is not known even for very small graphs. We present a new method for computing the clique-width of graphs based on 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 graphs from the literature as well as random graphs of various density. With our method we determined the smallest graphs that require a small pre-described clique-width.