Bibliographic Details
| Title: |
On using SAT solvers for graph computations. |
| Authors: |
Courcelle, B.1 (AUTHOR) courcell@labri.fr, Durand, I.1 (AUTHOR) irene.durand@u-bordeaux.fr |
| Source: |
Discrete Applied Mathematics. Feb2026, Vol. 380, p348-366. 19p. |
| Subjects: |
Directed graphs, Satisfiability (Computer science), Graph labelings, Graph algorithms, NP-complete problems |
| Abstract: |
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. [ABSTRACT FROM AUTHOR] |
|
Copyright of Discrete Applied Mathematics is the property of Elsevier B.V. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) |
| Database: |
Engineering Source |
