A SAT spproach to clique-width of a digraph and an application on model counting problems

Abstract

Introduced by Courcelle, Engelfriet, and Rozenberg, clique-width is a fundamental graph invariant that has been widely studied in discrete mathematics and computer science. Many hard problems on graphs and digraphs become tractable when restricted to graphs and digraphs of small clique-width, indeed solvable in linear time when restricted to classes of bounded clique-width. Clique-width is more general than treewidth, in the sense that algorithms parameterized by clique-width are effective on larger classes of instances than algorithms parameterized by treewidth (as there are graph classes of bounded clique-width where treewidth is unbounded, whereas small treewidth implies small clique-width). Typically algorithms for graphs of small clique-width require as input a certificate for small clique-width, which is already computationally hard to compute. In recent work Heule and Szeider presented a method for computing the clique-width of graphs based on an encoding to propositional satisfiability (SAT), which is then evaluated by a SAT solver, managing to discover the exact clique-width of various small graphs, previously unknown. Our main contribution is a generalization of the method by Heule and Szeider to directed graphs. Namely we present and implement an algorithm that, by invoking a SAT solver on a suitable instance, certifies the clique-width of a given directed graph. We exploit this implementation in two ways. First, we find the exact clique-width of various small directed graphs. Second, we implement an algorithm by Fischer, Makowsky, and Ravve and combine this and the aforementioned to an algorithm that counts models of CNFformulas of small directed incidence clique-width.