Convert a Strongly Connected Directed Graph to a Black-and-White 3-SAT Problem by the Balatonboglár Model

Abstract

In a previous paper we defined the black and white SAT problem which has exactly two solutions, where each variable is either true or false. We showed that black and white 2-SAT problems represent strongly connected directed graphs. We presented also the strong model of communication graphs. In this work we introduce two new models, the weak model, and the Balatonboglár model of communication graphs. A communication graph is a directed graph, where no self loops are allowed. In this work we show that the weak model of a strongly connected communication graph is a black and white SAT problem. We prove a powerful theorem, the so called transitions theorem. This theorem states that for any model which is between the strong and the weak model, we have that this model represents strongly connected communication graphs as black and white SAT problems. We show that the Balatonboglár model is between the strong and the weak model, and it generates 3-SAT problems, so the Balatonboglár model represents strongly connected communication graphs as black and white 3-SAT problems. Our motivation to study these models is the following: The strong model generates a 2-SAT problem from the input directed graph, so it does not give us a deep insight how to convert a general SAT problem into a directed graph. The weak model generates huge models, because it represents all cycles, even non-simple cycles, of the input directed graph. We need something between them to gain more experience. From the Balatonboglár model we learned that it is enough to have a subset of a clause, which represents a cycle in the weak model, to make the Balatonboglár model more compact. We still do not know how to represent a SAT problem as a directed graph, but this work gives a strong link between two prominent fields of formal methods: the SAT problem and directed graphs.

1. Motivation

In logic the most natural representation of an edge of a directed graph, say $a\to b$, is to use implication—i.e., $a\Rightarrow b$; i.e., the edge $a\to b$ can be represented by the binary clause: $(\neg a\vee b)$. We used that representation in a previous paper [1] and we were able to prove that the SAT representation of a strongly connected directed graph is a black and white 2-SAT problem. It is not a surprise that the SAT representation is a 2-SAT problem, since each edge can be represented by a binary clause.

The other property, black and white, means that the resulting SAT problem is "nearly" unsatisfiable; that means it has only two solutions, the white assignment and the black one. The white assignment assigns true to each variable; the black one assigns false to each variable.

This representation helps to translate a graph into a 2-SAT problem. We can also translate a black and white 2-SAT problem into a directed graph. We can also translate any other 2-SAT problem into a directed graph, if it does not subsume either the black or the white clause—i.e., it does not contain a clause which contains only positive or negative literals, for instance, $(a\vee b)$ or $(\neg a\vee \neg b).$

There are some natural questions. Why should we translate a 2-SAT problem into a direct graph? What can one do with clauses which contain only positive or negative literals?

Actually, there is no point to translating a 2-SAT problem into a directed graph, because the 2-SAT problem is solvable in linear time [2]. Preferably, we should translate 3-SAT problems into directed graphs, because then we could use graphical tools to study them, or we can translate them into 2-SAT problems. To be able to do so, the first step is to create a 3-SAT representation for directed graphs. The second step should answer the second question—what can one do with clauses which contain only positive or negative literals?

This paper aims to help to answer the first question. We present several models which can translate a directed graph into a SAT problem such that the SAT problem is black and white if and only if the directed graph is strongly connected.

The second question is answered partially in another study from our research group (http://fmv.ektf.hu/team.html); see [3].

2. Introduction

In recent years one of the most promising directions in mathematics has been the idea that one can unify various mathematical theories. One excellent example of this is the Langlands [4] program, which relates algebraic number theory to automorphic forms and representation theory. Another very interesting example is the modularity theorem [5]. This theory states that elliptic curves over the field of rational numbers are related to modular forms. Without this modularity theorem, Andrew Wiles could not have proven Fermat’s last theorem [6]. In this paper, we show some connection points between directed graphs and propositional logic formulas. We prove a theorem which allows one to use an algorithm from the field of propositional logic to check a graph property. Namely, we transform a directed graph into a SAT problem to check whether the graph is strongly connected or not.

The most well-known graphical representations are: the implication graph [2], the and-inverter graph [7], the reduced ordered binary decision diagram [8] and the zero-suppressed binary decision diagram [9]. Graphical representations of logical games stand as a well-known connection between graphs and logical formulas; see, for example, [10,11]. A more detailed list can be found in [12].

As we can see, great effort has been made in the direction of formulas to graphs. In this paper, we study the other way, the direction of graphs to formulas.

In a previous paper [1] we showed how to convert a directed graph into a 2-SAT problem. In this paper, we aim to translate directed graphs into 3-SAT problems.

3. Definitions

Negation of a set H is denoted by $\neg H$, which means that all elements in H are negated. Note that $\neg \neg H=H$.

A literal is normally a Boolean variable—a positive literal; the negation of a Boolean variable is called a negative literal. Examples for literals are: $a,\neg a,b,\neg b,\dots$.

A clause is a set of literals. A clause set is a set of clauses. A SAT problem is a clause set. An assignment is a set of literals.

Clauses are interpreted as disjunctions of their literals. Assignments are interpreted as conjunctions of their literals. Clause sets are interpreted as conjunctions of their clauses.

If a clause or an assignment contains exactly k literals, then we say it is a k-clause or a k-assignment, respectively. A k-SAT problem is a clause set where its clauses have at most k literals. A clause from a clause set is a full-length clause if and only if (iff) it contains all variables from the clause set.

If a is a literal in clause set S, and $\neg a$ is not a literal in S, then we say that a is a pure literal in S.

Let V be the set of variables of a clause set. We say that $WW$ is the white clause or the white assignment iff $WW=V$. We say that $BB$ is the black clause or the black assignment iff $BB=\neg V$. For example, if $V=\{a,b,c\}$, then $WW=\{a,b,c\}$, and $BB=\{\neg a,\neg b,\neg c\}$.

We say that clause C subsumes clause D iff C is a subset of D.

We say that clause set S subsumes clause C iff there is a clause in S which subsumes C. Formally: $SsubsumesC\iff \exists D(D\in S\wedge D\subseteq C)$.

We say that assignment M is a solution for clause set S iff for all $C\in S$ we have $M\cap C\ne \left\{\right\}$.

We say that the clause set S is a black and white SAT problem iff it has only two solutions, the white assignment ($WW$) and the black one ($BB$).

We say that clause sets A and B are equivalent iff they have the same set of solutions. We say that clause set A entails clause set B iff the set of solutions of A is a subset of the set of solutions of B; i.e., A may have no other solutions than B. This notion is denoted by $A\ge B$. Note that if A subsumes all clauses of B, then $A\ge B$.

We say that A is stronger than B iff $A\ge B$ and A and B are not equivalent. This notion is denoted by $A>B$.

The construction $\mathcal{D}=(\mathcal{V},\mathcal{E})$ is a directed graph, where $\mathcal{V}$ is the set of vertices, and $\mathcal{E}$ is the set of edges. An edge is an ordered pair of vertices. The edge $(a,b)$ is depicted by $a\to b$, and we can say that a has a child b. If $(a,b)$ is an element of $\mathcal{E}$, then we may say that $(a,b)$ is an edge of $\mathcal{D}$.

We say that $\mathcal{D}$ is a communication graph iff for all a in $\mathcal{V}$ have that $(a,a)$ is not in $\mathcal{E}$, and if x is an element of $\mathcal{V}$ then $\neg x$ must not be an element of $\mathcal{V}$. We need this constraint because we generate a logical formula out of $\mathcal{D}$. If we speak about a communication graph then we may use the word node as a synonym of vertex.

A path from $a_1$ to $a_j$ in directed graph $\mathcal{D}$ is a sequence of vertices $a_1,a_2,\dots ,a_j$ such that for each $i\in \{1,\dots ,j-1\}$ we have that $(a_i,a_{i+1})$ is an edge of $\mathcal{D}$. A path from $a_1$ to $a_j$ in directed graph $\mathcal{D}$ is a cycle iff $(a_j,a_1)$ is an edge of $\mathcal{D}$. The cycle $a_1,a_2,\dots ,a_j,a_1$ is represented by the following tuple: $(a_1,a_2,\dots ,a_j)$. This tuple can be used as a set of its elements. Note that in the representation of a cycle the first and the last element must not be the same vertex. Figure 1 shows an example for a path and a cycle.

If we have a cycle $(a_1,a_2,\dots ,a_n)$ then b is an exit point of it iff for some $j\in \{1,2,\dots ,m\}$ we have that $(a_j,b)$ is an edge and $b\notin \{a_1,a_2,\dots ,a_n\}$.

A directed graph is complete iff every pair of distinct vertices is connected by a pair of unique edges (one in each direction). A directed graph is strongly connected iff there is a path from each vertex to each other vertex. Note that a complete graph is also strongly connected. Note that a strongly connected graph contains a cycle which contains all vertices.

4. The Strong Model of Communication Graphs

In our previous model [1], which we call in this paper the strong model of communication graphs, edges are represented by logical implication: Let us assume that the graph $\mathcal{D}$ is $\left(\right\{a,b,c\},\{(a,b),(a,c)\left\}\right)$; i.e., $\mathcal{D}$ is a graph with three vertices, a, b and c, and with two edges, from a to b and from a to c. Thus, the strong model of $\mathcal{D}$ is $(a\Rightarrow b)\wedge (a\Rightarrow c)$.

The interpretation of this formula is the following in the field of wireless sensors networks: If node a is able to send a message to nodes b and c, then node a sends the message to both nodes b and c. However, this might result in an error, because both nodes have to send an acknowledgment that the message has arrived, but using the same frequency at the same time results in interference. A more natural way of communication is that we use some protocol, which decides where to send the message, either to node b or to node c; see the next section.

The strong model was defined formally in our previous work [1]. We recall its definition.

Let $\mathcal{D}=(\mathcal{V},\mathcal{E})$ be a communication graph; then the strong model of $\mathcal{D}$ is denoted by $\mathcal{SM}$, and defined as follows:

$$\mathcal{SM}:=\left\{\right\{\neg a,b\left\}\right|(a,b)\in \mathcal{E}\}.$$

Note that $\mathcal{SM}$ is a 2-SAT problem and has a nice property: each clause in it has exactly one positive and one negative literal; therefore, $\mathcal{SM}$ is satisfiable for any communication graph $\mathcal{D}$.

Furthermore, $\mathcal{SM}$ is a black and white SAT problem iff $\mathcal{D}$ is strongly connected; see Theorem 1 in [1]. Since we use this theorem several times herein, we recall it:

Theorem 1

(Theorem 1 from [1]). Let $\mathcal{D}$ be a communication graph. Let $\mathcal{SM}$ be the strong model of $\mathcal{D}$. Then $\mathcal{SM}$ is a black and white 2-SAT problem if and only if $\mathcal{D}$ is strongly connected.

As an example we show the strong model of the communication graph of Figure 2:

$$\begin{array}{c}\hfill \mathcal{SM}=\left\{\right\{\neg a,b\},\{\neg a,c\},\{\neg b,a\},\{\neg b,c\},\\ \hfill \{\neg b,d\},\{\neg c,a\},\{\neg c,d\}\}.\end{array}$$

(1)

Note that since the communication graph from Figure 2 is not strongly connected, its strong model (1) is not a black and white SAT problem. For example, $\{\neg a,\neg b,\neg c,d\}$ is a solution of it.

As a second example we show the strong model of the communication graph from Figure 3. This graph is almost the same as the previous one (Figure 2), but here we have an edge from d to a, which makes this graph strongly connected. Its strong model is:

$$\begin{array}{c}\hfill \mathcal{SM}=\left\{\right\{\neg a,b\},\{\neg a,c\},\{\neg b,a\},\{\neg b,c\},\\ \hfill \{\neg b,d\},\{\neg c,a\},\{\neg c,d\},\{\neg d,a\}\}.\end{array}$$

(2)

Note that since the communication graph from Figure 3 is strongly connected, its strong model is a black and white SAT problem; i.e., the SAT problem in (2) has only these two solutions: $\{a,b,c,d\}$ and $\{\neg a,\neg b,\neg c,\neg d\}$.

It is not easy to check that this SAT problem is indeed a black and white SAT problem. Therefore, first we show the set of all full-length clauses on the variables $\{a,b,c,d\}$ with an index number (index number: full-length clause):

$$\begin{array}{c}\hfill \{0:\{\neg a,\neg b,\neg c,\neg d\},1:\{\neg a,\neg b,\neg c,d\},2:\{\neg a,\neg b,c,\neg d\},\\ \hfill 3:\{\neg a,\neg b,c,d\},4:\{\neg a,b,\neg c,\neg d\},5:\{\neg a,b,\neg c,d\},\\ \hfill 6:\{\neg a,b,c,\neg d\},7:\{\neg a,b,c,d\},8:\{a,\neg b,\neg c,\neg d\},\\ \hfill 9:\{a,\neg b,\neg c,d\},10:\{a,\neg b,c,\neg d\},11:\{a,\neg b,c,d\},\\ \hfill 12:\{a,b,\neg c,\neg d\},13:\{a,b,\neg c,d\},14:\{a,b,c,\neg d\},\\ \hfill 15:\{a,b,c,d\}\},\end{array}$$

(3)

As a second step, we give which clause from (2) subsumes which full-length clauses (clause: indices of subsumed full-length clauses):

$$\begin{array}{c}\hfill \mathcal{SM}=\left\{\right\{\neg a,b\}:4,5,6,7,\{\neg a,c\}:2,3,6,7,\{\neg b,a\}:9,10,11,12,\\ \hfill \{\neg b,c\}:2,3,10,11,\{\neg b,d\}:1,3,9,11,\{\neg c,a\}:8,9,13,14,\\ \hfill \{\neg c,d\}:1,5,9,13,\{\neg d,a\}:8,10,12,14\}.\end{array}$$

(4)

From this one can check that (2) subsumes all full-length clauses, except the black and the white clause; hence, it has only two solutions, the white and the black assignment.

5. The Weak Model of Communication Graphs

We define the weak model of communication graphs. Let us assume that $\mathcal{D}=\left(\right\{a,b,c\},\{(a,b),(a,c)\left\}\right)$, as in the previous section. The weak model of $\mathcal{D}$ contains the clause $(a\Rightarrow b)\vee (a\Rightarrow c)$, which means that if a node can send a message to more than one nodes, then it can send the message only to one of them. Note that $(a\Rightarrow b)\vee (a\Rightarrow c)$ is equivalent to $(\neg a\vee b\vee c)$.

The only problem with this representation is that the message can be trapped if a graph contains a cycle. Let us assume that we have a cycle with two nodes, $n_1$ and $n_2$. Then $n_1$ may send the message to $n_2$, and $n_2$ to $n_1$, and so on, which means that other nodes could never get the message. This is not good, since our goal is to send a message to each node, if it is possible.

Let us add a new edge to the graph $\left(\right\{a,b,c\},\{(a,b),(a,c)\left\}\right)$. The new edge should go from b to a. Now we have a cycle with the nodes a and b. Now we have to add a clause to our model which ensures that if b sends a message to a, and a can send a message to b or c, then a should not send back the message to b, but it has to send it to c: $\left(\right(b\Rightarrow a)\wedge (a\Rightarrow (b\vee c))\Rightarrow (a\Rightarrow c)$. Note that this is equivalent to the clause: $(\neg a\vee \neg b\vee c)$.

In a more general way, node a which has outgoing edges to nodes $b_1,b_2,\dots ,b_k$ is represented by the clause: $(\neg a\vee b_1\vee b_2\vee \dots \vee b_k)$; and the cycle $a_1,a_2\dots a_n,a_1$ with exit points $b_1,b_2,\dots ,b_m$ is represented by the clause: $(\neg a_1\vee \neg a_2\vee \dots \vee \neg a_n\vee b_1\vee b_2\vee \dots \vee b_m)$. We call this model as the weak model of communication graphs.

We also define it formally: Let $\mathcal{D}$ be a communication graph. Let $\mathcal{V}$ be the set of vertices of $\mathcal{D}$ and $\mathcal{E}$ the set of edges of $\mathcal{D}$. Since $\mathcal{D}$ is a communication graph, we know that elements of $\mathcal{V}$ can be used as positive literals. Then we define the following notion:

$$OutE\left(a\right):=\left\{b\right|(a,b)\in \mathcal{E}\}.$$

$$NodeRep\left(a\right):=\{\neg a\}\cup OutE\left(a\right).$$

$$NodeRep:=\left\{NodeRep\right(a\left)\right|a\in \mathcal{V}\wedge OutE\left(a\right)\ne \varnothing \}.$$

$$Cycles:=\left\{(a_1,a_2,\dots ,a_k)\right|k=1\vee {\forall }_{i=1\dots k}(a_{\left(imodk\right)+1}\in OutE\left(a_i\right)\},$$

and for any two elements of $Cycles$ they cannot be equal as a set.

$$ExitPonts\left((a_1,a_2,\dots a_k)\right):=\left\{b\right|{\exists }_{i=1\dots k}(b\in OutE\left(a_i\right))\wedge \neg {\exists }_{j=1\dots k}(b=a_j)\}.$$

$$CycleRep:=\{\neg C\cup ExitPonts(C\left)\right|C\in Cycles\wedge ExitPonts\left(C\right)\ne \varnothing \}.$$

$$\mathcal{WM}:=NodeRep\cup CycleRep.$$

$\mathcal{WM}$ is the weak model of $\mathcal{D}$.

Note that $NodeRep$ is a subset of $CycleRep$, because we take each node itself as a cycle; see the constraint $k=1\vee \dots$ in the definition of $CycleRep$. Thus, alternatively we can define $\mathcal{WM}$ as follows: $\mathcal{WM}:=CycleRep.$ We do not use this observation in this work, although some proofs would be shorter.

Please note that each clause in $\mathcal{WM}$ contains at least one positive and one negative literal, because a node is only represented if it has an outgoing edge, and a cycle is only represented if it has an exit point; therefore, $\mathcal{SM}$ is satisfiable for any communication graph $\mathcal{D}$.

Figure 4 shows two simple communication graphs. Their $NodeRep$ values are: $\left\{\right\{\neg a,b,c\left\}\right\}$, and $\left\{\right\{\neg a,b,c,d\left\}\right\}$, respectively.

Figure 2 shows a communication graph with three cycles:

$$(a,b),(a,b,c),(a,c).$$

Thus, its weak model is (after each clause we list the indices of subsumed full-length clauses from (3)):

$$\begin{array}{c}\hfill \mathcal{WM}=\left\{\right\{\neg a,b,c\}:6,7,\{\neg b,a,c,d\}:11,\{\neg c,a,d\}:9,14,\\ \hfill \{\neg a,\neg b,c,d\}:3,\{\neg a,\neg b,\neg c,d\}:1,\{\neg a,\neg c,b,d\}:5\}.\end{array}$$

(5)

Note that since d has no child node, it does not occur as a negative literal in the model.

Note that since the communication graph from Figure 2 is not strongly connected, its weak model (5) is not a black and white SAT problem. For example, $\{\neg a,\neg b,\neg c,d\}$ is a solution of the SAT problem in (5).

As a second example we show the weak model of the communication graph from Figure 3. In this graph we have six cycles:

$$(a,b),(a,b,c),(a,c),(a,b,d),(a,c,d),(a,b,c,d).$$

The last cycle contains all vertices, so it has no exit point; therefore, no clause is generated for it. Note that in this graph we have an edge from d to a. The corresponding clauses are the last three clauses in this example; the last two clauses correspond to the new cycles. The remaining clause is the same as in the previous model. Thus, the weak model is (after each clause we list the indices of subsumed full-length clauses from (3)):

$$\begin{array}{c}\hfill \mathcal{WM}=\left\{\right\{\neg a,b,c\}:6,7,\{\neg b,a,c,d\}:11,\{\neg c,a,d\}:9,14,\\ \hfill \{\neg a,\neg b,c,d\}:3,\{\neg a,\neg b,\neg c,d\}:1,\{\neg a,\neg c,b,d\}:5\\ \hfill \{\neg d,a\}:8,10,12,14,\{\neg a,\neg b,\neg d,c\}:2,\{\neg a,\neg c,\neg d,b\}:4\}.\end{array}$$

(6)

Note that since the communication graph from Figure 3 is strongly connected, its weak model is a black and white SAT problem; i.e., the SAT problem in (6) has only these two solutions: $\{a,b,c,d\}$ and $\{\neg a,\neg b,\neg c,\neg d\}$.

Each cycle was a simple cycle in the above two examples. A cycle is simple iff only the first and last vertices are repeated. Thus, we might think that it is enough to consider simple cycles. The next example shows a case when we need to consider a non-simple cycle as well.

In Figure 5 we can see a strongly connected communication graph which contains three simple cycles, $(a,b),(a,b,c,d)$ and $(b,c)$, and one non-simple cycle, $(a,b,c,b)$. As a third example we give the weak model of this communication graph (after each clause we list the indices of subsumed full-length clauses from (3)):

$$\begin{array}{c}\hfill \mathcal{WM}=\left\{\right\{\neg a,b\}:4,5,6,7,\{\neg b,a,c\}:10,11,\{\neg c,b,d\}:5,13,\\ \hfill \{\neg d,a\}:8,10,12,14,\{\neg a,\neg b,c\}:2,3,\{\neg b,\neg c,a,d\}:9,\\ \hfill \{\neg a,\neg b,\neg c,d\}:1\}.\end{array}$$

(7)

Note that the last clause is generated from the non-simple cycle, and that full-length clause is not subsumed by any other clause.

6. The Balatonboglár Model of Communication Graphs

Since the weak model does not result in a 3-SAT problem, we introduce also the Balatonboglár model, which is a simplified version of the weak model, which uses the trick that instead of detecting each cycle in the graph, it generates from each path $a,b,c$ the following 3-clause: $(\neg a\vee \neg b\vee c)$ even if there is no cycle which contains the vertices a and b. This simplification allows very fast 3-SAT model generation from a directed graph, and the model will be black and white 3-SAT if and only if the input directed graph is strongly connected.

We define the Balatonboglár model of communication graphs as follows. Let $\mathcal{D}$ be a communication graph. Let $\mathcal{V}$ be the set of vertices of $\mathcal{D}$ and $\mathcal{E}$ the set of edges of $\mathcal{D}$. Since $\mathcal{D}$ is a communication graph, we know that elements of $\mathcal{V}$ can be used as positive literals. Then we define the following notion:

$$NodeRep2:=\left\{\right\{\neg a,b\left\}\right|a\in \mathcal{V}\wedge \left\{b\right\}=OutE\left(a\right)\}.$$

$$NodeRep3\left(a\right):=\{\neg a,b,c\},wherea\in \mathcal{V}\wedge b\in OutE\left(a\right)\wedge c\in OutE\left(a\right)\wedge b\ne c.$$

$$NodeRep3:=\left\{NodeRep3\right(a\left)\right|a\in \mathcal{V}\}.$$

$$TagForward:=\left\{\right\{\neg a,\neg b,c\left\}\right|a\in \mathcal{V}\wedge b\in OutE\left(a\right)\wedge c\in OutE\left(b\right)\wedge a\ne b\ne c\}.$$

$$\mathcal{BM}:=NodeRep2\cup NodeRep3\cup TagForward.$$

$\mathcal{BM}$ is a Balatonboglár model of $\mathcal{D}$.

Note that $NodeRep3\left(a\right)$ is not a deterministic function, it is just any 3 length subset of $NodeRep\left(a\right)$.

The name $TagForward$ comes from the children’s game tag: There is one child who has to catch someone else by touching he or she. This action is called tagging. There is a rule: the tagged one cannot tag back; he or she must tag someone else, so must tag forward.

As a first example, we give the Balatonboglár model of the graph from Figure 2 (after each clause we list the indices of subsumed full-length clauses from (3)):

$$\begin{array}{c}\hfill \mathcal{BM}=\left\{\right\{\neg a,b,c\}:6,7,\{\neg b,c,d\}:3,11,\{\neg c,a,d\}:9,13,\\ \hfill \{\neg a,\neg b,c\}:2,3,\{\neg a,\neg b,d\}:1,3,\{\neg a,\neg c,b\}:4,5,\\ \hfill \{\neg a,\neg c,d\}:1,5,\{\neg b,\neg c,a\}:8,9,\{\neg b,\neg c,d\}:1,9\}.\end{array}$$

(8)

Note that b has three child nodes, so instead of $\{\neg b,c,d\}$, we could use either $\{\neg b,a,c\}$ or $\{\neg b,a,d\}$. Note also that Figure 2 is not strongly connected, so its Balatonboglár model is not a black and white SAT problem. For example, $\{\neg a,\neg b,\neg c,d\}$ is a solution of the SAT problem in (8).

As a second example, we show the Balatonboglár model of the communication graph from Figure 3. Note that in this graph we have an edge from d to a. The corresponding clauses are the last three clauses in this Balatonboglár model: (after each clause we list the indices of subsumed full-length clauses from (3)):

$$\begin{array}{c}\hfill \mathcal{BM}=\left\{\right\{\neg a,b,c\}:6,7,\{\neg b,c,d\}:3,11,\{\neg c,a,d\}:9,13,\\ \hfill \{\neg d,a\}:8,10,12,14,\{\neg a,\neg b,c\}:2,3,\{\neg a,\neg b,d\}:1,3,\{\neg a,\neg c,d\}:1,5,\\ \hfill \{\neg b,\neg c,a\}:8,9,\{\neg b,\neg c,d\}:1,9,\{\neg b,\neg d,a\}:8,10,\\ \hfill \{\neg c,\neg a,b\}:4,5,\{\neg c,\neg d,a\}:8,12,\{\neg d,\neg a,b\}:4,6,\{\neg d,\neg a,c\}:3,7\}.\end{array}$$

(9)

Note that since the communication graph from Figure 3 is strongly connected, its Balatonboglár model is a black and white SAT problem; i.e., the SAT problem in (9) has only these two solutions: $\{a,b,c,d\}$, and $\{\neg a,\neg b,\neg c,\neg d\}$.

As a third example, we show the Balatonboglár model of the communication graph from Figure 5 (after each clause we list the indices of subsumed full-length clauses from (3)):

$$\begin{array}{c}\hfill \mathcal{BM}=\left\{\right\{\neg a,b\}:4,5,6,7,\{\neg b,a,c\}:10,11,\{\neg c,b,d\}:5,13,\\ \hfill \{\neg d,a\}:8,10,12,14,\{\neg a,\neg b,c\}:2,3,\{\neg b,\neg c,a\}:8,9,\\ \hfill \{\neg b,\neg c,d\}:1,9,\{\neg c,\neg d,a\}:8,12,\{\neg a,\neg d,b\}:4,6\}.\end{array}$$

(10)

Since there is no node which has more than two child nodes, there is no other possible Balatonboglár model for this graph.

Note that since the communication graph from Figure 5 is strongly connected, its Balatonboglár model (10) is a black and white SAT problem.

Our long term goal is to find out how to represent a 3-SAT problem as a directed graph. This model does not tell us how to do that; it gives only a link from the field of directed graphs to the field of 3-SAT problems, which might help us to find out in the future how to represent a 3-SAT problem as a directed graph. Thus, this remains an open question, which seems to be a very difficult one, because if we are able to translate a 3-SAT problem into a directed graph, then we could translate it to a 2-SAT problem using the result of our previous work, which means that we would have a 3-SAT to 2-SAT converter.

7. Theoretical Results

This section is the main contribution of this work. We prove that the new models, the weak one and the Balatonboglár one, have the same property as the strong one; i.e., the model of a communication graph is a black and white SAT problem iff the graph is strongly connected. To be able to prove this, we need some auxiliary lemmas. The first one states that the weak model has at least two solutions, the white one and the black one.

Lemma 1.

Let $\mathcal{D}$ be a communication graph. Let $\mathcal{WM}$ be the weak model of $\mathcal{D}$. Then $\mathcal{WM}$ has at least two solutions, namely, the white assignment ($WW$) and the black assignment ($BB$).

Proof. 

Let $\mathcal{D}$ be a communication graph. Let $\mathcal{WM}$ be the weak model of $\mathcal{D}$. Since there is a positive and also a negative literal in each clause of $\mathcal{WM}$, the white assignment ($WW$) and also the black assignment ($BB$) are solutions for $\mathcal{WM}$. □

The second lemma states that if the weak model has only two solutions, then each cycle in the communication graph has at least one exit point, except the cycle which contains all vertices of the graph.

Lemma 2.

Let $\mathcal{D}$ be a communication graph. Let $\mathcal{WM}$ be the weak model of $\mathcal{D}$. Assume that $\mathcal{WM}$ has only two solutions. Then for each cycle $C\in Cycles$ we have that $ExitPonts\left(C\right)$ is not empty or C contains all vertices of $\mathcal{D}$.

Proof. 

Let $\mathcal{D}$ be a communication graph. Let $\mathcal{WM}$ be the weak model of $\mathcal{D}$. Assume that $\mathcal{WM}$ has only two solutions. Lemma 1 makes sure that the solutions are $WW$ and $BB$. Assume that our goal is not true; i.e., there is a cycle $C=(a_1,a_2,\dots ,a_k)$, which has no exit point and does not contain all vertices of $\mathcal{D}$. We show that this assumption leads to a contradiction. Let us construct the following assignment: $\{a_1,\dots ,a_k,\neg b_1,\dots \neg b_m\}$, where $\{b_1,b_2,\dots ,b_m\}=\mathcal{V}\setminus C$, where $\mathcal{V}$ is the set vertices of $\mathcal{D}$. Since C has no exit point, there is no corresponding clause generated by $CycleRep$. Since there is no clause which would falsify the constructed assignment, this is a solution of $\mathcal{WM}$. However, this contradicts the assumption that $\mathcal{WM}$ has only two solutions—namely, $WW$ and $BB$. Thus, our original statement is true. □

The next lemma states that a black and white SAT problem may not contain pure literals.

Lemma 3.

If $\mathcal{S}$ is a black and white SAT problem, then it contains no pure literal.

Proof. 

Assume $\mathcal{S}$ is a black and white SAT problem. Then, by definition of a black and white SAT problem, we know that $\mathcal{S}$ has only two solutions, $WW$ and $BB$. Since there is no other solution of $\mathcal{S}$ and $\neg WW=BB$, we obtain that $\mathcal{S}$ may not contain a pure literal. □

The next lemma states that if we have a complete graph, then its weak model is a black and white SAT problem. This result is somehow natural, since the weak model of a complete graph is the biggest possible that we can generate and the weak model always has at least two solutions.

Lemma 4.

If $\mathcal{D}$ is a complete communication graph, and $\mathcal{WM}$ is the weak model of $\mathcal{D}$, then $\mathcal{WM}$ is a black and white SAT problem.

Proof. 

Assume $\mathcal{D}$ is a complete communication graph. Assume $\mathcal{WM}$ is the weak model of $\mathcal{D}$. Since $\mathcal{D}$ is complete, for any vertex a we have that $OutE\left(a\right)$ contains all other vertices, so $NodeRep$ contains all full-length clauses with one negative literal. Since any two vertices create a cycle where the exit points are the rest of the vertices, $CycleRep$ contains all full-length clauses with two negative literals. The same is true for any $k=2\dots n-1$ vertices, so $CycleRep$ contains all full-length clauses with $2,\dots ,n-1$ negative literals. However, $\mathcal{WM}$ does not subsume the full-length clause with no negative literals, i.e., the white clause ($WW$), nor the full-length clause with n negative literals, i.e., the black clause ($BB$). This means that $\mathcal{WM}$ has only two solutions, the white and the black assignment; i.e., $\mathcal{WM}$ is a black and white SAT problem. □

Now comes one of our main contributions, the theorem which states that the weak model of a strongly connected graph is a black and white SAT problem, which means that if the graph is strongly connected, then the weak model has the same power as the strong model. Since the proof is rather technical, we give also a high-level proof of it.

From left to right we prove the theorem in a constructive way: Let us have a sequence of vertices which can be built by Lemma 3 and by the construction of $NodeRep$. Eventually we will find a cycle at the end of this sequence. Lemma 2 ensures that there is an exit point from this cycle, which either results in a bigger cycle, or in a longer sequence. Using these two steps, eventually we construct a strongly connected component. From Lemma 2 it follows that it is also maximal (otherwise there would be an exit point from it which would allow one to do the above steps); i.e., the graph is strongly connected.

From right to left we use induction: We start the proof from a complete graph. We know that complete graphs are also strongly connected. As the induction step, we drop an edge from this graph such that it remains strongly connected. We assume that before the drop the weak model was black and white, which is true by Lemma 4. We show that it remains black and white also after the drop. To show this, we show that each clause in the model after the drop is a subset of some clause from the mode before the drop. Thus, the new model may not have more solutions then the old one. However, the new model has to have at least two solutions by Lemma 1. Thus, the new model is black and white. Since our graph can be constructed by dropping edges from a complete graph, which has the same set of vertices, its weak model is also black and white.

Theorem 2.

Let $\mathcal{D}$ be a communication graph. Let $\mathcal{WM}$ be the weak model of $\mathcal{D}$. Then $\mathcal{WM}$ is a black and white SAT problem if and only if $\mathcal{D}$ is strongly connected.

Proof. 

Let $\mathcal{D}$ be a communication graph. Let $\mathcal{WM}$ be the weak model of $\mathcal{D}$. We show that $\mathcal{WM}$ is a black and white SAT problem if and only if $\mathcal{D}$ is strongly connected.

(From left to right:) We assume $\mathcal{WM}$ is a black and white SAT problem; we show by construction that $\mathcal{D}$ is strongly connected.

(R0) Let $a_1$ be a vertex from $\mathcal{D}$. Let $j=1$.

(R1) Now we have a sequence of vertices: $a_1,\dots ,a_j$. We work with its last vertex: $a_j$. From Lemma 3 we know that literal $a_j$ is not pure in $\mathcal{WM}$, so $\neg a_j$ is present in $\mathcal{WM}$. Thus, there must be a clause in $\mathcal{WM}$ generated be $NodeRep$ for vertex $a_j$. Since $NodeRep$ is a subset of $CycleRep$, by Lemma 2, there is a clause $\{\neg a_j,b_1,\dots ,b_k\}$ in $\mathcal{WM}$. Let $a_{j+1}$ be a vertex from $b_1,\dots ,b_k$ such that $a_{j+1}$ is not in $\{a_1,\dots ,a_j\}$. If this is possible, then let $j=j+1$ and go to (R1). Note that this is not always possible because $\mathcal{D}$ is a final graph, so eventually each vertex from $b_1,\dots ,b_k$ must be in the set $\{a_1,\dots ,a_j\}$. In this case let $a_{j+1}$ be a vertex from $b_1,\dots ,b_k$ such that $a_{j+1}=a_i$, where $i<j$ and i is the smallest possible. This means that we have i such that $i<j$ and $a_i=a_{j+1}$; i.e., $(a_i,\dots ,a_j)$ is a cycle. Go to (R2).

(R2) Now we have a sequence of vertices $a_1,\dots ,a_j$, and the end of this sequence from $a_i$ to $a_j$ is a cycle. If $i=1$ and the cycle contains all the vertices from $\mathcal{D}$, then go to (R3). Otherwise, by creation of $CycleRep$ and by Lemma 2 we know that $\mathcal{WM}$ contains a clause $\{\neg a_i,\dots ,\neg a_j,b_1,\dots ,b_m\}$, where $b_1,\dots ,b_m$ are exit points of the cycle $(a_i,\dots ,a_j)$. Let $a_{j+1}$ be a vertex from $b_1,\dots ,b_m$ such that $a_{j+1}$ is not present in $a_1,\dots ,a_j$. If this is possible, then let $j=j+1$, and go to (R1). Note that this is not always possible because $\mathcal{D}$ is a final graph. so eventually each vertex from $b_1,\dots ,b_k$ must be in the set $\{a_1,\dots ,a_j\}$. In this case let $a_{j+1}$ be a vertex from $b_1,\dots ,b_m$, such that $a_{j+1}=a_{i^{\prime }}$ and $i^{\prime }$ is the smallest possible. Since $b_1,\dots ,b_m$ are exit points of the cycle $(a_i,\dots ,a_j)$, we know that $i^{\prime }$ is smaller than i because each vertex from $b_1,\dots ,b_m$ is different from $a_i,\dots ,a_j$. This means that we have $i^{\prime }$ such that $i^{\prime }<j$, and $i^{\prime }<i$ and $a_{i^{\prime }}=a_{j+1}$; i.e., $(a_i^{\prime },\dots ,a_j)$ is a cycle. Let $i=i^{\prime }$, and go to (R2).

(R3) Eventually (R2) exists to (R3) because, by Lemma 2, each cycle has at least one exit point, which results in a bigger cycle, or in a longer $a_1,\dots ,a_j$ sequence of vertices. Thus, eventually the sequence $a_1,\dots ,a_j$ will contain all vertices, and eventually i will be 1, so eventually we will find a cycle which contains all vertices. Hence, $\mathcal{D}$ is strongly connected.

(From right to left:) We assume $\mathcal{D}$ is strongly connected; we show by induction that $\mathcal{WM}$ is a black and white SAT problem. Let H be the complete communication graph which has the same set of vertices as $\mathcal{D}$. We know from Lemma 4 that the weak model of H is a black and white SAT problem. This is our induction base. It is well known that complete graphs are also strongly connected. We create G from H by deleting edges from H such that G remains strongly connected. Let Z be the weak model of G. Our induction hypothesis is that Z is a black and white SAT problem. Our induction step is that we delete an edge from G such that it remains strongly connected. Let $G^{\prime }$ be this graph. Let $Z^{\prime }$ be the weak model of $G^{\prime }$. We show that $Z^{\prime }$ is a black and white SAT problem. To show this, we show that $Z^{\prime }\ge Z$; i.e., $Z^{\prime }$ subsumes all clauses from Z. Without loss of generality let us assume that we deleted the edge from vertex a to vertex b. All clauses from Z are the same as the clauses of $Z^{\prime }$, except the ones generated by $CycleRep$ for those cycles which contain a. From those clauses let $D=\{\neg a_1,\dots ,\neg a_k,b_1,\dots ,b_m\}$ be an arbitrary but fixed one, where $(a_1,\dots ,a_k)$ is a cycle in Z and $b_1,\dots ,b_m$ are its exit points. We know that $k>=1$ and $a=a_i$ for some $i\in \{1,\dots ,k\}$, and b is one of the other vertices from this clause. There are the following cases:

• If b is one of the exit points and some other vertex from the cycle has an edge to b, then $Z^{\prime }$ contains the same clause: D.
• If b is one of the exit points, say $b=b_p$, where $p\in \{1,\dots ,m\}$, and no other vertex from the cycle has an edge to b, then $Z^{\prime }$ contains the clause $\{\neg a_1,\dots ,\neg a_k,b_1,\dots ,b_{p-1},b_{p+1},\dots b_m\}$, which is a subset of D. Note that the vertex sequence $b_1,\dots ,b_{p-1},b_{p+1},\dots b_m$ contains some vertices, because $G^{\prime }$ is a strongly connected graph; i.e., each cycle has an exit point, unless it contains all vertices.
• If b is one of the other vertices of the cycle, but b is not the next vertex after a in this cycle, then $Z^{\prime }$ contains the same clause, D.
• If b is one of the other vertices of the cycle, and b is the next vertex after a in this cycle, then $a_1,\dots ,a_k$ is not a cycle in $Z^{\prime }$. If there is no other child vertex of a in $\{a_1,\dots ,a_k\}$, then the clause generated by $NodeRep$ for a in $G^{\prime }$ is a subset of D. If there are other child vertices of a in $\{a_1,\dots ,a_k\}$, then there must be a subset of $\{a_1,\dots ,a_k\}$ which contains all other child vertices of a except b, and which is a cycle in $G^{\prime }$. The clause generated by $CycleRep$ for this cycle in $G^{\prime }$ is a subset of D.

We showed that $Z^{\prime }$ subsumes all clauses from Z. This means that $Z^{\prime }\ge Z$; i.e., $Z^{\prime }$ may have no other solutions than Z. By our induction, hypothesis Z has only two solutions, $BB$ and $WW$. We know from Lemma 1 that $BB$ and $WW$ are solutions for $Z^{\prime }$, because $Z^{\prime }$ is a weak model. In addition, since $Z^{\prime }$ may have no other solution, $Z^{\prime }$ is a black and white SAT problem. This means that the weak model of any strongly connected communication graph is a black and white SAT problem. Hence, $\mathcal{WM}$ is a blacked-and-white SAT problem, because $\mathcal{D}$ is strongly connected and $\mathcal{WM}$ is its weak model. □

The following lemma states that $\mathcal{SM}$ entails $\mathcal{WM}$ for any communication graph. This means that any solution of $\mathcal{SM}$ is also a solution of $\mathcal{WM}$. To show this, it is enough to show that $\mathcal{SM}$ subsumes all clauses from $\mathcal{WM}$.

Lemma 5.

Let $\mathcal{D}$ be a communication graph. Let $\mathcal{SM}$ be the strong model of $\mathcal{D}$. Let $\mathcal{WM}$ be the weak model of $\mathcal{D}$. Then $\mathcal{SM}\ge \mathcal{WM}$.

Proof. 

Assume $\mathcal{D}$ is a communication graph, $\mathcal{SM}$ is the strong model of $\mathcal{D}$ and $\mathcal{WM}$ is the weak model of $\mathcal{D}$. We show that $\mathcal{SM}\ge \mathcal{WM}$. To show this, it is enough to show that $\mathcal{SM}$ subsumes all clauses from $\mathcal{WM}$. Let C is an arbitrary but fixed element of $\mathcal{WM}$. If C is an element of $NodeRep$, then, without loss of generality, we may assume that $C=\{\neg a,b_1,b_2,\dots ,b_k\}$, where $k>0$. From the construction of $NodeRep$ we know that in $\mathcal{D}$ there are the following edges: $(a,b_1),(a,b_2),\dots ,(a,b_k)$. Since $\mathcal{SM}$ is generated from the same graph, by its definition we know that $\mathcal{SM}$ contains the clauses $\{\neg a,b_1\},\{\neg a,b_2\},\dots ,\{\neg a,b_k\}$ and all of these ones subsume C.

If C is an element of $Cycles$, then, without loss of generality, we may assume that $C=\{\neg d_1,\neg d_2,\dots ,\neg d_m,e_1,e_2,\dots ,e_n\}$, where $m>0$, and $n>0$. From the construction of $Cycles$ we know that in $\mathcal{D}$ there is an edge: $(d,e)$ such that d is one of the vertices from $d_1,d_2,\dots ,d_m$, and e is one of the vertices from $e_1,e_2,\dots ,e_m$. Since $\mathcal{SM}$ is generated from the same graph, by its definition we know that $\mathcal{SM}$ contains the clauses $\{\neg d,e\}$, which subsumes C.

Hence, $\mathcal{SM}\ge \mathcal{WM}$. □

The following lemma states that $\mathcal{SM}$ and $\mathcal{WM}$ are equivalent if the represented communication graph is strongly connected or there are no branches in the graph. If the communication graph is strongly connected, then both $\mathcal{SM}$ and $\mathcal{WM}$ are black and white SAT problems, so they are equivalent.

Lemma 6.

Let $\mathcal{D}$ be a communication graph. Let $\mathcal{SM}$ be the strong model of $\mathcal{D}$. Let $\mathcal{WM}$ be the weak model of $\mathcal{D}$. If

(I) 

$\mathcal{D}$ is strongly connected, or

(II) 

Each vertex in $\mathcal{D}$ has only one child,

then $\mathcal{SM}$ and $\mathcal{WM}$ are equivalent.

Proof. 

In the case of (I) we know that $\mathcal{D}$ is strongly connected, so by Theorem 1, and by Theorem 2 we know that $\mathcal{SM}$ and $\mathcal{WM}$ are black and white SAT problems, so by the definition of clause set equivalent-ness they are equivalent. In case of (II) we have that $NodeRep=\mathcal{SM}$ and $NodeRep\subseteq \mathcal{WM}$. From this we obtain that $\mathcal{WM}\ge \mathcal{SM}$. From Lemma 5 we know that $\mathcal{SM}\ge \mathcal{WM}$. Hence, $\mathcal{SM}$ and $\mathcal{WM}$ are equivalent. □

The following lemma gives a criterion for the communication graph which makes the strong model stronger than the weak model. This lemma is not needed to prove the following theorems but it is still interesting.

Lemma 7.

Let $\mathcal{D}$ be a communication graph. Let $\mathcal{SM}$ be the strong model of $\mathcal{D}$. Let $\mathcal{WM}$ be the weak model of $\mathcal{D}$. Then $\mathcal{SM}>\mathcal{WM}$ iff $\mathcal{D}$ is not strongly connected, and there is at least one vertex in it which has more than one child vertex.

Proof. 

(From left to right:) We assume $\mathcal{SM}>\mathcal{WM}$, so $\mathcal{SM}$ and $\mathcal{WM}$ are not equivalent. Since the right side of Lemma 6 is negated, the negation of the left side of Lemma 6 is implied. Hence, $\mathcal{D}$ is not strongly connected, and there is at least one vertex in it which has more than one child vertex.

(From right to left:) Assume $\mathcal{D}$ is not strongly connected, and there is at least one vertex in it, say a, which has more than one child vertex, say $b_1,b_2,\dots ,b_k$, where $k>1$. In this case $WW\setminus \left\{b_1\right\}\cup \{\neg b_1\}$ and $BB\setminus \neg a,\neg b_k\cup \{a,b_k\}$ are solutions for $\mathcal{WM}$ but they are not solutions of $\mathcal{SM}$, since they do not satisfy the clause $\{\neg a,b_1\}$ from $\mathcal{SM}$. Thus, $\mathcal{SM}$ and $\mathcal{WM}$ are not equivalent. From this and from Lemma 5 we obtain that Then $\mathcal{SM}>\mathcal{WM}$. □

The following theorem, the so called transitions theorem states that any “transition” between $\mathcal{SM}$ and $\mathcal{WM}$ is a black and white SAT problem iff the communication graph is strongly connected. This is one of the main results of this work.

Theorem 3

(Transitions Theorem). If for all communication graphs $\mathcal{D}$ we have $\mathcal{SM}\ge \mathcal{MM}\ge \mathcal{WM}$, where $\mathcal{SM}$ is the strong model of $\mathcal{D}$, $\mathcal{WM}$ is the weak model of $\mathcal{D}$ and $\mathcal{MM}$ is an arbitrary but fixed model of $\mathcal{D}$, then $\mathcal{MM}$ is a black and white SAT problem iff $\mathcal{D}$ is strongly connected.

Proof. 

Assume that $\mathcal{D}$ is a communication graph. Assume that $\mathcal{SM}$ is the strong model of $\mathcal{D}$, $\mathcal{WM}$ is the weak model of $\mathcal{D}$ and $\mathcal{MM}$ is an arbitrary but fixed model of $\mathcal{D}$. We show that $\mathcal{MM}$ is a black and white SAT problem iff $\mathcal{D}$ is strongly connected.

(From left to right:) Assume $\mathcal{MM}$ is a black and white SAT problem. From this and from the assumption that $\mathcal{SM}\ge \mathcal{MM}$, we have that $\mathcal{SM}$ is a black and white SAT problem, since any strong model has always at least two solutions, the white assignment and the black one; see [1]. From this and from Theorem 1 we have that $\mathcal{D}$ is strongly connected.

(From right to left:) Assume $\mathcal{D}$ is strongly connected. Then by Lemma 6 we know that $\mathcal{SM}$ and $\mathcal{WM}$ are equivalent. From this and from the assumption that $\mathcal{SM}\ge \mathcal{MM}\ge \mathcal{WM}$ it follows that $\mathcal{SM}$ and $\mathcal{MM}$ and $\mathcal{WM}$ are equivalent. Since $\mathcal{D}$ is strongly connected by Theorem 2 we know that $\mathcal{WM}$ is a black and white SAT problem. We know that $\mathcal{MM}$ and $\mathcal{WM}$ are equivalent; hence, $\mathcal{MM}$ is a black and white SAT problem. □

The following theorem shows that the Balatonboglár model of a communication graph is a transition between the strong and the weak model. Actually, Balatonboglár is a small city in Hungary next to lake Balaton. We spent quite a lot of time next to the lake thinking about a model which is 3-SAT and black and white if the directed graph is strongly connected. As the next theorem shows, we were successful. As a sign of appreciation for that great time, we gave the name Balatonboglár to that model.

Theorem 4.

Let $\mathcal{D}$ be a communication graph. Let $\mathcal{BM}$ be a Balatonboglár model of $\mathcal{D}$. Then $\mathcal{BM}$ is a black and white 3-SAT problem if and only if $\mathcal{D}$ is strongly connected.

Proof. 

Assume $\mathcal{D}$ is a communication graph. Assume $\mathcal{BM}$ is a Balatonboglár model of $\mathcal{D}$. We show $\mathcal{BM}$ is a black and white 3-SAT problem if and only if $\mathcal{D}$ is strongly connected. Due to the construction of $\mathcal{BM}$, it is a 3-SAT problem for any communication graph. Let $\mathcal{WM}$ be the weak model of $\mathcal{D}$. Let $\mathcal{SM}$ be the strong model of $\mathcal{D}$. Now we show that $\mathcal{BM}$ is a black and white 3-SAT problem if and only if $\mathcal{D}$ is strongly connected. From the transitions theorem (Theorem 3), we know that to show this, it is enough to show that $\mathcal{SM}\ge \mathcal{BM}\ge \mathcal{WM}$.

(I) As a first step, we show that $\mathcal{SM}\ge \mathcal{BM}$. To show this it is enough to show that $\mathcal{SM}$ subsumes all clauses from $\mathcal{BM}$. Let C be an arbitrary but fixed element of $\mathcal{BM}$. This means that C is either an element of $NodeRep2$, or $NodeRep3$, or $TagForward$. If C is an element of $NodeRep2$, then C is also element of $\mathcal{SM}$, so this case is trivial. If C is an element of $NodeRep3$, then, without loss of generality, we may assume that $C=\{\neg a,b,c\}$, where a is a vertex in $\mathcal{D}$ and $b\in OutE\left(a\right)$ and $c\in OutE\left(a\right)$ and $b\ne c$. From the construction of $NodeRep3$ we know that in $\mathcal{D}$ there are the following edges: $(a,b),(a,c)$. Since $\mathcal{SM}$ is generated from the same graph, by its definition we know that $\mathcal{SM}$ contains the clauses $\{\neg a,b\},\{\neg a,c\}$ and both of them subsume C. If C is an element of $TagForward$, then, without loss of generality, we may assume that $C=\{\neg d,\neg e,f\}$, where d is a vertex in $\mathcal{D}$, and $e\in OutE\left(d\right)$ and $f\in OutE\left(e\right)$. From the construction of $TagForward$ we know that in $\mathcal{D}$ there are the following edges: $(d,e),(e,f)$. Since $\mathcal{SM}$ is generated from the same graph, by its definition we know that $\mathcal{SM}$ contains the clause $\{\neg e,f\}$ which subsumes C.

(II) As a second step, we show $\mathcal{BM}\ge \mathcal{WM}$. To show this it is enough to show that $\mathcal{BM}$ subsumes all clauses from $\mathcal{WM}$. Let C be an arbitrary but fixed element of $\mathcal{WM}$. This means that C is an element of either $NodeRep$ or $Cycles$. If C is an element of $NodeRep$, then, without loss of generality, we may assume that $C=\{\neg a,b_1,b_2,\dots ,b_k\}$, where $k>0$. From the construction of $NodeRep$ we know that in $\mathcal{D}$ there are the following edges: $(a,b_1),(a,b_2),\dots ,(a,b_k)$. Since $\mathcal{BM}$ is generated from the same graph, by its definition we know that $\mathcal{BM}$ contains the clause $\{\neg a,b_1\}$, if $k=1$, or $\{\neg a,b,c\}$, where b and c are different vertices from $b_1,b_2,\dots ,b_k$, and that said clause subsumes C. If C is an element of $Cycles$, then, without loss of generality, we may assume that $C=\{\neg d_1,\neg d_2,\dots ,\neg d_m,e_1,e_2,\dots ,e_n\}$, where $m>0$ and $n>0$. If $m=1$ then C is an element of $NodeRep$, whose case was already considered, so we may assume that $m>1$. From the construction of $Cycles$ and from $m>1$ we know that in $\mathcal{D}$ there are these edges: $(d_i,d_{i+1})$ and $(d_{i+1},e)$ such that $d_i$ and $d_{i+1}$ are some of the vertices from $d_1,d_2,\dots ,d_m$, and e is one of the vertices from $e_1,e_2,\dots ,e_m$. Since $\mathcal{BM}$ is generated from the same graph, by its definition we know that $\mathcal{BM}$ contains the clause $\{\neg d_i,\neg d_{i+1},e\}$ which subsumes C.

Hence, $\mathcal{BM}$ is a black and white 3-SAT problem if and only if $\mathcal{D}$ is strongly connected. □

8. Future Work

This work is purely theoretical; there is no usage described here. That does not mean that it is not possible. In this section we list some possible usage.

The BaW 1.0 SAT solver solves the SAT problems generated by our strong model in linear time [13]. The proof of Theorem 2 suggests that we might find a similar algorithm for SAT problems generated by our weak model.

Most probably, this is not possible in the case of the Balatonboglár model, since in that model there is not enough information to reconstruct the input directed graph. It is an interesting question: in which cases is the reconstruction still possible? Most probably not in all cases, because then we could translate a 3-SAT problem into a directed graph, and then that directed graph into a 2-SAT problem. Although this direction seems to be unrealistic, it is still interesting and very challenging for us.

One of the problems is to do with those clauses in a 3-SAT problem, which subsumes the white clause or the black clause. To solve this problem we need a technique which creates a black and white SAT, if the input SAT problem is unsatisfiable.

Our latest results suggest that our weak model is the weakest possible model for communication graphs, because if we generate a weak model from a strongly connected graph and we add the black and the white clause to the model, then we get a minimal unsatisfiable SAT instance; i.e., there is no redundant clause in the weak model [12]. Our other models are quite redundant; see [14]. We plan to combine the good features of the weak and the Balatonboglár models. The first one is non-redundant; the second one can be constructed in a fast way.