A SAT Approach to Clique-Width
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.
Cite
@article{arxiv.1304.5498,
title = {A SAT Approach to Clique-Width},
author = {Marijn J. H. Heule and Stefan Szeider},
journal= {arXiv preprint arXiv:1304.5498},
year = {2013}
}
Comments
proofs in section 3 updated, results remain unchanged