Back to Search
Start Over
Using extended resolution to represent strongly connected components of directed graphs.
- Source :
-
Annales Mathematicae et Informaticae . 2023, Vol. 58, p92-109. 18p. - Publication Year :
- 2023
-
Abstract
- In this paper, we study how to represent a directed graph as a SAT problem. We study those directed graphs which consists of two strongly connected components (SCC). We reuse the SAT models which are known as the Black-and-White SAT representations. We present the so-called 3rd Solution Lemma: If a directed graph consists of two SCCs, A and B, and there is an edge from A to B, then the corresponding SAT representation has 3 solutions: the black assignment, the white assignment, and the 3rd solution can be written as ¬A union B. Using this result, we present an important negative result: We cannot represent all SAT problems as directed graphs using the Black-and-White SAT representations. Furthermore, we study the question how to represent an SCC by one Boolean variable to maintain the 3rd Solution Lemma. For that we use extended resolution. [ABSTRACT FROM AUTHOR]
- Subjects :
- *DIRECTED graphs
*LOGIC
Subjects
Details
- Language :
- English
- ISSN :
- 17875021
- Volume :
- 58
- Database :
- Academic Search Index
- Journal :
- Annales Mathematicae et Informaticae
- Publication Type :
- Academic Journal
- Accession number :
- 174359856
- Full Text :
- https://doi.org/10.33039/ami.2023.08.011