MMN-2140
Equivalence of strongly connected graphs and black-and-white 2-SAT problems
Csaba Bíró; Gábor Kusper;Abstract
Our goal is to create a propositional logic formula to model a directed graph and use a SAT solver to analyse it. This model is similar to the well-know one of Aspvall et al., but they create a directed graph from a 2-SAT problem, we generate a 2-SAT problem from a directed graph. In their paper if the 2-SAT problem is unsatisfiable, then the generated directed graph is strongly connected, in our case, if the directed graph is strongly connected, then the generated 2-SAT problem is a black-and-white 2-SAT problem, which has two solutions: where each variable is true (the white assignment), and where each variable is false (the black one). If we see a directed graph as a communication model of a network, then we can ask in our model whether a node can send a message to another one through the network. More specifically we can ask whether all nodes can send messages to all other ones, i.e., the graph is strongly connected or not.
Vol. 19 (2018), No. 2, pp. 755-768