Using extended resolution to represent strongly connected components of directed graphs

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

Preview

Text AMI_58_from92to109.pdf - Published Version Download (560kB) | Preview

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.

Actions (login required)

Edit Item