Using extended resolution to represent strongly connected components of directed graphs

Kusper, Gábor, Yang, Zijian Győző, Nagy, Benedek (2023) Using extended resolution to represent strongly connected components of directed graphs Annales Mathematicae et Informaticae. 58. pp. 92-109. ISSN 1787-6117 (Online)

pdf AMI_58_from92to109.pdf Download (560kB) [error in script]

Absztrakt (kivonat)

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.

Mű típusa:	Folyóiratcikk - Journal article
Szerző:	Szerző neve Email MTMT azonosító ORCID azonosító Közreműködés Kusper, Gábor NEM RÉSZLETEZETT NEM RÉSZLETEZETT NEM RÉSZLETEZETT Szerző Yang, Zijian Győző NEM RÉSZLETEZETT NEM RÉSZLETEZETT NEM RÉSZLETEZETT Szerző Nagy, Benedek NEM RÉSZLETEZETT NEM RÉSZLETEZETT NEM RÉSZLETEZETT Szerző
Kapcsolódó URL-ek:	Befoglaló kötet
Kulcsszavak:	SAT problem, boolean logic, directed graphs
Folyóirat alcíme:	Selected papers of the 12th International Conference on Applied Informatics
Nyelv:	angol
Kötetszám:	58.
DOI azonosító:	10.33039/ami.2023.08.011
ISSN:	1787-6117 (Online)
Felhasználó:	Tibor Gál
Dátum:	24 Aug 2023 06:31
Utolsó módosítás:	10 Nov 2023 14:01
URI:	http://publikacio.uni-eszterhazy.hu/id/eprint/7712

Műveletek (bejelentkezés szükséges)

Tétel nézet