On using SAT solvers for graph computations

Determining the clique-width or the linear clique-width of an undirected graph reduces to a Boolean satisfiability problem (a SAT problem in short) that can be solved for graphs of moderate size, depending on the available solver. This method is due to Heule and Szeider. We extend it to directed graphs, to vertex-labelled graphs and to the computation of relative clique-width. We have checked that certain proved upper-bounds to clique-width are actually reachable. We also propose open questions about upper-bounds to clique-width that this approach may help to solve. Every existential second-order graph property P has an NP-algorithm and can be formulated as a SAT problem constructed from the graph G for which P has to be checked. However, the resulting instance may be much too large to be solved in practice. We consider particular existential second-order sentences from which SAT problems of polynomial size can be easily constructed and, furthermore, that define hereditary graph properties, i.e. preserved by induced graph inclusion. Motivated by the search of minimal excluded graphs for hereditary graph properties (induced subgraph inclusion is here the relevant partial order on graphs), we examine cases where a SAT problem for an induced subgraph of a graph G can be obtained easily from the corresponding SAT problem for G .