On using SAT solvers for graph computations.
Saved in:
| 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 |
| FullText | Text: Availability: 0 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 189851005 AccessLevel: 6 PubType: Academic Journal PubTypeId: academicJournal PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: On using SAT solvers for graph computations. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22Courcelle%2C+B%2E%22">Courcelle, B.</searchLink><relatesTo>1</relatesTo> (AUTHOR)<i> courcell@labri.fr</i><br /><searchLink fieldCode="AR" term="%22Durand%2C+I%2E%22">Durand, I.</searchLink><relatesTo>1</relatesTo> (AUTHOR)<i> irene.durand@u-bordeaux.fr</i> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22Discrete+Applied+Mathematics%22">Discrete Applied Mathematics</searchLink>. Feb2026, Vol. 380, p348-366. 19p. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22Directed+graphs%22">Directed graphs</searchLink><br /><searchLink fieldCode="DE" term="%22Satisfiability+%28Computer+science%29%22">Satisfiability (Computer science)</searchLink><br /><searchLink fieldCode="DE" term="%22Graph+labelings%22">Graph labelings</searchLink><br /><searchLink fieldCode="DE" term="%22Graph+algorithms%22">Graph algorithms</searchLink><br /><searchLink fieldCode="DE" term="%22NP-complete+problems%22">NP-complete problems</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: 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] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>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.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=189851005 |
| RecordInfo | BibRecord: BibEntity: Identifiers: – Type: doi Value: 10.1016/j.dam.2025.10.017 Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 19 StartPage: 348 Subjects: – SubjectFull: Directed graphs Type: general – SubjectFull: Satisfiability (Computer science) Type: general – SubjectFull: Graph labelings Type: general – SubjectFull: Graph algorithms Type: general – SubjectFull: NP-complete problems Type: general Titles: – TitleFull: On using SAT solvers for graph computations. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: Courcelle, B. – PersonEntity: Name: NameFull: Durand, I. IsPartOfRelationships: – BibEntity: Dates: – D: 15 M: 02 Text: Feb2026 Type: published Y: 2026 Identifiers: – Type: issn-print Value: 0166218X Numbering: – Type: volume Value: 380 Titles: – TitleFull: Discrete Applied Mathematics Type: main |
| ResultId | 1 |
