Bibliographic Metadata

A SAT spproach to clique-width of a digraph and an application on model counting problems / von Aykut Parlak
Additional Titles
Ein SAT-Ansatz zur Cliquenweite von Digraphen und eine Anwendung auf das Zählen von Modellen
AuthorParlak, Aykut
CensorSzeider, Stefan ; Bova, Simone Maria
PublishedWien, 2016
Descriptionxiii, 46 Seiten : Illustrationen, Diagramme
Institutional NoteTechnische Universität Wien, Diplomarbeit, 2017
Zusammenfassung in deutscher Sprache
Abweichender Titel nach Übersetzung der Verfasserin/des Verfassers
Document typeThesis (Diplom)
Keywords (DE)Cliquenweite / SAT-Kodierung / Zählen von Modellen
Keywords (EN)Clique-width / SAT Encoding / Model Counting
URNurn:nbn:at:at-ubtuw:1-101013 Persistent Identifier (URN)
 The work is publicly available
A SAT spproach to clique-width of a digraph and an application on model counting problems [0.66 mb]
Abstract (English)

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.

The PDF-Document has been downloaded 31 times.