cphb/chapter17.tex

564 lines
17 KiB
TeX
Raw Permalink Normal View History

2017-02-28 21:02:48 +01:00
\chapter{Strong connectivity}
2016-12-28 23:54:51 +01:00
2017-01-08 21:17:46 +01:00
\index{strongly connected graph}
2017-02-06 20:33:11 +01:00
In a directed graph,
the edges can be traversed in one direction only,
2017-01-08 21:17:46 +01:00
so even if the graph is connected,
2017-02-06 20:33:11 +01:00
this does not guarantee that there would be
a path from a node to another node.
For this reason, it is meaningful to define a new concept
that requires more than connectivity.
2017-01-08 21:17:46 +01:00
A graph is \key{strongly connected}
if there is a path from any node to all
other nodes in the graph.
For example, in the following picture,
2017-02-06 20:33:11 +01:00
the left graph is strongly connected
2017-01-08 21:17:46 +01:00
while the right graph is not.
2016-12-28 23:54:51 +01:00
\begin{center}
\begin{tikzpicture}[scale=0.9]
\node[draw, circle] (1) at (1,1) {$1$};
\node[draw, circle] (2) at (3,1) {$2$};
\node[draw, circle] (3) at (1,-1) {$3$};
\node[draw, circle] (4) at (3,-1) {$4$};
\path[draw,thick,->] (1) -- (2);
\path[draw,thick,->] (2) -- (4);
\path[draw,thick,->] (4) -- (3);
\path[draw,thick,->] (3) -- (1);
\node[draw, circle] (1b) at (6,1) {$1$};
\node[draw, circle] (2b) at (8,1) {$2$};
\node[draw, circle] (3b) at (6,-1) {$3$};
\node[draw, circle] (4b) at (8,-1) {$4$};
\path[draw,thick,->] (1b) -- (2b);
\path[draw,thick,->] (2b) -- (4b);
\path[draw,thick,->] (4b) -- (3b);
\path[draw,thick,->] (1b) -- (3b);
\end{tikzpicture}
\end{center}
2017-01-08 21:17:46 +01:00
The right graph is not strongly connected
because, for example, there is no path
from node 2 to node 1.
2016-12-28 23:54:51 +01:00
2017-01-08 21:17:46 +01:00
\index{strongly connected component}
\index{component graph}
2016-12-28 23:54:51 +01:00
2017-01-08 21:17:46 +01:00
The \key{strongly connected components}
of a graph divide the graph into strongly connected
2017-02-06 20:33:11 +01:00
parts that are as large as possible.
2017-01-08 21:17:46 +01:00
The strongly connected components form an
acyclic \key{component graph} that represents
the deep structure of the original graph.
2016-12-28 23:54:51 +01:00
2017-01-08 21:17:46 +01:00
For example, for the graph
2016-12-28 23:54:51 +01:00
\begin{center}
\begin{tikzpicture}[scale=0.9,label distance=-2mm]
\node[draw, circle] (1) at (-1,1) {$7$};
\node[draw, circle] (2) at (-3,2) {$3$};
\node[draw, circle] (4) at (-5,2) {$2$};
\node[draw, circle] (6) at (-7,2) {$1$};
\node[draw, circle] (3) at (-3,0) {$6$};
\node[draw, circle] (5) at (-5,0) {$5$};
\node[draw, circle] (7) at (-7,0) {$4$};
\path[draw,thick,->] (2) -- (1);
\path[draw,thick,->] (1) -- (3);
\path[draw,thick,->] (3) -- (2);
\path[draw,thick,->] (2) -- (4);
\path[draw,thick,->] (3) -- (5);
\path[draw,thick,->] (4) edge [bend left] (6);
\path[draw,thick,->] (6) edge [bend left] (4);
\path[draw,thick,->] (4) -- (5);
\path[draw,thick,->] (5) -- (7);
\path[draw,thick,->] (6) -- (7);
\end{tikzpicture}
\end{center}
2017-01-08 21:17:46 +01:00
the strongly connected components are as follows:
2016-12-28 23:54:51 +01:00
\begin{center}
\begin{tikzpicture}[scale=0.9]
\node[draw, circle] (1) at (-1,1) {$7$};
\node[draw, circle] (2) at (-3,2) {$3$};
\node[draw, circle] (4) at (-5,2) {$2$};
\node[draw, circle] (6) at (-7,2) {$1$};
\node[draw, circle] (3) at (-3,0) {$6$};
\node[draw, circle] (5) at (-5,0) {$5$};
\node[draw, circle] (7) at (-7,0) {$4$};
\path[draw,thick,->] (2) -- (1);
\path[draw,thick,->] (1) -- (3);
\path[draw,thick,->] (3) -- (2);
\path[draw,thick,->] (2) -- (4);
\path[draw,thick,->] (3) -- (5);
\path[draw,thick,->] (4) edge [bend left] (6);
\path[draw,thick,->] (6) edge [bend left] (4);
\path[draw,thick,->] (4) -- (5);
\path[draw,thick,->] (5) -- (7);
\path[draw,thick,->] (6) -- (7);
\draw [red,thick,dashed,line width=2pt] (-0.5,2.5) rectangle (-3.5,-0.5);
\draw [red,thick,dashed,line width=2pt] (-4.5,2.5) rectangle (-7.5,1.5);
\draw [red,thick,dashed,line width=2pt] (-4.5,0.5) rectangle (-5.5,-0.5);
\draw [red,thick,dashed,line width=2pt] (-6.5,0.5) rectangle (-7.5,-0.5);
\end{tikzpicture}
\end{center}
2017-01-08 21:17:46 +01:00
The corresponding component graph is as follows:
2016-12-28 23:54:51 +01:00
\begin{center}
\begin{tikzpicture}[scale=0.9]
\node[draw, circle] (1) at (-3,1) {$B$};
\node[draw, circle] (2) at (-6,2) {$A$};
\node[draw, circle] (3) at (-5,0) {$D$};
\node[draw, circle] (4) at (-7,0) {$C$};
\path[draw,thick,->] (1) -- (2);
\path[draw,thick,->] (1) -- (3);
\path[draw,thick,->] (2) -- (3);
\path[draw,thick,->] (2) -- (4);
\path[draw,thick,->] (3) -- (4);
\end{tikzpicture}
\end{center}
2017-01-08 21:17:46 +01:00
The components are $A=\{1,2\}$,
$B=\{3,6,7\}$, $C=\{4\}$ and $D=\{5\}$.
A component graph is an acyclic, directed graph,
2017-02-06 20:33:11 +01:00
so it is easier to process than the original graph.
Since the graph does not contain cycles,
we can always construct a topological sort and
use dynamic programming techniques like those
presented in Chapter 16.
2017-01-08 21:17:46 +01:00
\section{Kosaraju's algorithm}
\index{Kosaraju's algorithm}
2017-02-21 00:17:36 +01:00
\key{Kosaraju's algorithm}\footnote{According to \cite{aho83},
S. R. Kosaraju invented this algorithm in 1978
but did not publish it. In 1981, the same algorithm was rediscovered
and published by M. Sharir \cite{sha81}.} is an efficient
2017-01-08 21:17:46 +01:00
method for finding the strongly connected components
of a directed graph.
2017-02-06 20:33:11 +01:00
The algorithm performs two depth-first searches:
2017-01-08 21:17:46 +01:00
the first search constructs a list of nodes
according to the structure of the graph,
and the second search forms the strongly connected components.
\subsubsection{Search 1}
2017-02-06 20:33:11 +01:00
The first phase of Kosaraju's algorithm constructs
2017-01-08 21:17:46 +01:00
a list of nodes in the order in which a
depth-first search processes them.
The algorithm goes through the nodes,
and begins a depth-first search at each
unprocessed node.
Each node will be added to the list
after it has been processed.
2017-02-06 20:33:11 +01:00
In the example graph, the nodes are processed
2017-01-08 21:17:46 +01:00
in the following order:
2016-12-28 23:54:51 +01:00
\begin{center}
\begin{tikzpicture}[scale=0.9,label distance=-2mm]
\node[draw, circle] (1) at (-1,1) {$7$};
\node[draw, circle] (2) at (-3,2) {$3$};
\node[draw, circle] (4) at (-5,2) {$2$};
\node[draw, circle] (6) at (-7,2) {$1$};
\node[draw, circle] (3) at (-3,0) {$6$};
\node[draw, circle] (5) at (-5,0) {$5$};
\node[draw, circle] (7) at (-7,0) {$4$};
\node at (-7,2.75) {$1/8$};
\node at (-5,2.75) {$2/7$};
\node at (-3,2.75) {$9/14$};
\node at (-7,-0.75) {$4/5$};
\node at (-5,-0.75) {$3/6$};
\node at (-3,-0.75) {$11/12$};
\node at (-1,1.75) {$10/13$};
\path[draw,thick,->] (2) -- (1);
\path[draw,thick,->] (1) -- (3);
\path[draw,thick,->] (3) -- (2);
\path[draw,thick,->] (2) -- (4);
\path[draw,thick,->] (3) -- (5);
\path[draw,thick,->] (4) edge [bend left] (6);
\path[draw,thick,->] (6) edge [bend left] (4);
\path[draw,thick,->] (4) -- (5);
\path[draw,thick,->] (5) -- (7);
\path[draw,thick,->] (6) -- (7);
\end{tikzpicture}
\end{center}
2017-01-08 21:17:46 +01:00
The notation $x/y$ means that
2017-02-18 13:00:23 +01:00
processing the node started
at time $x$ and finished at time $y$.
Thus, the corresponding list is as follows:
2016-12-28 23:54:51 +01:00
\begin{tabular}{ll}
\\
2017-02-18 13:00:23 +01:00
node & processing time \\
2016-12-28 23:54:51 +01:00
\hline
4 & 5 \\
5 & 6 \\
2 & 7 \\
1 & 8 \\
6 & 12 \\
7 & 13 \\
3 & 14 \\
\\
\end{tabular}
2017-02-06 20:33:11 +01:00
%
% In the second phase of the algorithm,
% the nodes will be processed
% in reverse order: $[3,7,6,1,2,5,4]$.
2016-12-28 23:54:51 +01:00
2017-01-08 21:17:46 +01:00
\subsubsection{Search 2}
2016-12-28 23:54:51 +01:00
2017-01-08 21:17:46 +01:00
The second phase of the algorithm
forms the strongly connected components
of the graph.
First, the algorithm reverses every
edge in the graph.
2017-02-18 13:00:23 +01:00
This guarantees that during the second search,
2017-02-06 20:33:11 +01:00
we will always find strongly connected
components that do not have extra nodes.
2016-12-28 23:54:51 +01:00
2017-02-06 20:33:11 +01:00
After reversing the edges,
the example graph is as follows:
2016-12-28 23:54:51 +01:00
\begin{center}
\begin{tikzpicture}[scale=0.9,label distance=-2mm]
\node[draw, circle] (1) at (-1,1) {$7$};
\node[draw, circle] (2) at (-3,2) {$3$};
\node[draw, circle] (4) at (-5,2) {$2$};
\node[draw, circle] (6) at (-7,2) {$1$};
\node[draw, circle] (3) at (-3,0) {$6$};
\node[draw, circle] (5) at (-5,0) {$5$};
\node[draw, circle] (7) at (-7,0) {$4$};
\path[draw,thick,<-] (2) -- (1);
\path[draw,thick,<-] (1) -- (3);
\path[draw,thick,<-] (3) -- (2);
\path[draw,thick,<-] (2) -- (4);
\path[draw,thick,<-] (3) -- (5);
\path[draw,thick,<-] (4) edge [bend left] (6);
\path[draw,thick,<-] (6) edge [bend left] (4);
\path[draw,thick,<-] (4) -- (5);
\path[draw,thick,<-] (5) -- (7);
\path[draw,thick,<-] (6) -- (7);
\end{tikzpicture}
\end{center}
2017-02-06 20:33:11 +01:00
After this, the algorithm goes through
2017-05-29 19:39:30 +02:00
the list of nodes created by the first search,
2017-02-06 20:33:11 +01:00
in \emph{reverse} order.
If a node does not belong to a component,
2017-01-08 21:17:46 +01:00
the algorithm creates a new component
2017-02-06 20:33:11 +01:00
and starts a depth-first search
that adds all new nodes found during the search
to the new component.
2016-12-28 23:54:51 +01:00
2017-01-08 21:17:46 +01:00
In the example graph, the first component
begins at node 3:
2016-12-28 23:54:51 +01:00
\begin{center}
\begin{tikzpicture}[scale=0.9,label distance=-2mm]
\node[draw, circle] (1) at (-1,1) {$7$};
\node[draw, circle] (2) at (-3,2) {$3$};
\node[draw, circle] (4) at (-5,2) {$2$};
\node[draw, circle] (6) at (-7,2) {$1$};
\node[draw, circle] (3) at (-3,0) {$6$};
\node[draw, circle] (5) at (-5,0) {$5$};
\node[draw, circle] (7) at (-7,0) {$4$};
\path[draw,thick,<-] (2) -- (1);
\path[draw,thick,<-] (1) -- (3);
\path[draw,thick,<-] (3) -- (2);
\path[draw,thick,<-] (2) -- (4);
\path[draw,thick,<-] (3) -- (5);
\path[draw,thick,<-] (4) edge [bend left] (6);
\path[draw,thick,<-] (6) edge [bend left] (4);
\path[draw,thick,<-] (4) -- (5);
\path[draw,thick,<-] (5) -- (7);
\path[draw,thick,<-] (6) -- (7);
\draw [red,thick,dashed,line width=2pt] (-0.5,2.5) rectangle (-3.5,-0.5);
\end{tikzpicture}
\end{center}
2017-02-18 13:00:23 +01:00
Note that since all edges are reversed,
2017-02-06 20:33:11 +01:00
the component does not ''leak'' to other parts in the graph.
2016-12-28 23:54:51 +01:00
\begin{samepage}
2017-01-08 21:17:46 +01:00
The next nodes in the list are nodes 7 and 6,
2017-05-29 19:39:30 +02:00
but they already belong to a component,
so the next new component begins at node 1:
2016-12-28 23:54:51 +01:00
\begin{center}
\begin{tikzpicture}[scale=0.9,label distance=-2mm]
\node[draw, circle] (1) at (-1,1) {$7$};
\node[draw, circle] (2) at (-3,2) {$3$};
\node[draw, circle] (4) at (-5,2) {$2$};
\node[draw, circle] (6) at (-7,2) {$1$};
\node[draw, circle] (3) at (-3,0) {$6$};
\node[draw, circle] (5) at (-5,0) {$5$};
\node[draw, circle] (7) at (-7,0) {$4$};
\path[draw,thick,<-] (2) -- (1);
\path[draw,thick,<-] (1) -- (3);
\path[draw,thick,<-] (3) -- (2);
\path[draw,thick,<-] (2) -- (4);
\path[draw,thick,<-] (3) -- (5);
\path[draw,thick,<-] (4) edge [bend left] (6);
\path[draw,thick,<-] (6) edge [bend left] (4);
\path[draw,thick,<-] (4) -- (5);
\path[draw,thick,<-] (5) -- (7);
\path[draw,thick,<-] (6) -- (7);
\draw [red,thick,dashed,line width=2pt] (-0.5,2.5) rectangle (-3.5,-0.5);
\draw [red,thick,dashed,line width=2pt] (-4.5,2.5) rectangle (-7.5,1.5);
%\draw [red,thick,dashed,line width=2pt] (-4.5,0.5) rectangle (-5.5,-0.5);
%\draw [red,thick,dashed,line width=2pt] (-6.5,0.5) rectangle (-7.5,-0.5);
\end{tikzpicture}
\end{center}
\end{samepage}
2017-02-06 20:33:11 +01:00
\begin{samepage}
Finally, the algorithm processes nodes 5 and 4
2017-05-02 16:53:18 +02:00
that create the remaining strongly connected components:
2016-12-28 23:54:51 +01:00
\begin{center}
\begin{tikzpicture}[scale=0.9,label distance=-2mm]
\node[draw, circle] (1) at (-1,1) {$7$};
\node[draw, circle] (2) at (-3,2) {$3$};
\node[draw, circle] (4) at (-5,2) {$2$};
\node[draw, circle] (6) at (-7,2) {$1$};
\node[draw, circle] (3) at (-3,0) {$6$};
\node[draw, circle] (5) at (-5,0) {$5$};
\node[draw, circle] (7) at (-7,0) {$4$};
\path[draw,thick,<-] (2) -- (1);
\path[draw,thick,<-] (1) -- (3);
\path[draw,thick,<-] (3) -- (2);
\path[draw,thick,<-] (2) -- (4);
\path[draw,thick,<-] (3) -- (5);
\path[draw,thick,<-] (4) edge [bend left] (6);
\path[draw,thick,<-] (6) edge [bend left] (4);
\path[draw,thick,<-] (4) -- (5);
\path[draw,thick,<-] (5) -- (7);
\path[draw,thick,<-] (6) -- (7);
\draw [red,thick,dashed,line width=2pt] (-0.5,2.5) rectangle (-3.5,-0.5);
\draw [red,thick,dashed,line width=2pt] (-4.5,2.5) rectangle (-7.5,1.5);
\draw [red,thick,dashed,line width=2pt] (-4.5,0.5) rectangle (-5.5,-0.5);
\draw [red,thick,dashed,line width=2pt] (-6.5,0.5) rectangle (-7.5,-0.5);
\end{tikzpicture}
\end{center}
2017-02-06 20:33:11 +01:00
\end{samepage}
2016-12-28 23:54:51 +01:00
2017-02-06 20:33:11 +01:00
The time complexity of the algorithm is $O(n+m)$,
because the algorithm
2017-02-18 13:00:23 +01:00
performs two depth-first searches.
2016-12-28 23:54:51 +01:00
2017-01-08 21:17:46 +01:00
\section{2SAT problem}
2016-12-28 23:54:51 +01:00
2017-01-08 21:17:46 +01:00
\index{2SAT problem}
2016-12-28 23:54:51 +01:00
2017-02-28 21:02:48 +01:00
Strong connectivity is also linked with the
2017-02-25 17:21:27 +01:00
\key{2SAT problem}\footnote{The algorithm presented here was
introduced in \cite{asp79}.
There is also another well-known linear-time algorithm \cite{eve75}
that is based on backtracking.}.
2017-01-08 21:17:46 +01:00
In this problem, we are given a logical formula
2016-12-28 23:54:51 +01:00
\[
(a_1 \lor b_1) \land (a_2 \lor b_2) \land \cdots \land (a_m \lor b_m),
\]
2017-01-08 21:17:46 +01:00
where each $a_i$ and $b_i$ is either a logical variable
2016-12-28 23:54:51 +01:00
($x_1,x_2,\ldots,x_n$)
2017-01-08 21:17:46 +01:00
or a negation of a logical variable
($\lnot x_1, \lnot x_2, \ldots, \lnot x_n$).
The symbols ''$\land$'' and ''$\lor$'' denote
logical operators ''and'' and ''or''.
Our task is to assign each variable a value
2017-02-06 20:33:11 +01:00
so that the formula is true, or state
that this is not possible.
2017-01-08 21:17:46 +01:00
For example, the formula
2016-12-28 23:54:51 +01:00
\[
L_1 = (x_2 \lor \lnot x_1) \land
(\lnot x_1 \lor \lnot x_2) \land
(x_1 \lor x_3) \land
(\lnot x_2 \lor \lnot x_3) \land
(x_1 \lor x_4)
\]
2017-02-18 13:00:23 +01:00
is true when the variables are assigned as follows:
\[
\begin{cases}
x_1 = \textrm{false} \\
x_2 = \textrm{false} \\
x_3 = \textrm{true} \\
x_4 = \textrm{true} \\
\end{cases}
\]
2017-01-08 21:17:46 +01:00
However, the formula
2016-12-28 23:54:51 +01:00
\[
L_2 = (x_1 \lor x_2) \land
(x_1 \lor \lnot x_2) \land
(\lnot x_1 \lor x_3) \land
(\lnot x_1 \lor \lnot x_3)
\]
2017-02-06 20:33:11 +01:00
is always false, regardless of how we
2017-02-18 13:00:23 +01:00
assign the values.
2017-02-06 20:33:11 +01:00
The reason for this is that we cannot
2017-02-18 13:00:23 +01:00
choose a value for $x_1$
2017-01-08 21:17:46 +01:00
without creating a contradiction.
If $x_1$ is false, both $x_2$ and $\lnot x_2$
2017-02-18 13:00:23 +01:00
should be true which is impossible,
2017-01-08 21:17:46 +01:00
and if $x_1$ is true, both $x_3$ and $\lnot x_3$
2017-02-18 13:00:23 +01:00
should be true which is also impossible.
2017-01-08 21:17:46 +01:00
The 2SAT problem can be represented as a graph
2017-02-06 20:33:11 +01:00
whose nodes correspond to
2017-01-08 21:17:46 +01:00
variables $x_i$ and negations $\lnot x_i$,
2017-02-06 20:33:11 +01:00
and edges determine the connections
2017-01-08 21:17:46 +01:00
between the variables.
Each pair $(a_i \lor b_i)$ generates two edges:
$\lnot a_i \to b_i$ and $\lnot b_i \to a_i$.
2017-02-06 20:33:11 +01:00
This means that if $a_i$ does not hold,
2017-01-08 21:17:46 +01:00
$b_i$ must hold, and vice versa.
2017-02-06 20:33:11 +01:00
The graph for the formula $L_1$ is:
2016-12-28 23:54:51 +01:00
\\
\begin{center}
\begin{tikzpicture}[scale=1.0,minimum size=2pt]
\node[draw, circle, inner sep=1.3pt] (1) at (1,2) {$\lnot x_3$};
\node[draw, circle] (2) at (3,2) {$x_2$};
\node[draw, circle, inner sep=1.3pt] (3) at (1,0) {$\lnot x_4$};
\node[draw, circle] (4) at (3,0) {$x_1$};
\node[draw, circle, inner sep=1.3pt] (5) at (5,2) {$\lnot x_1$};
\node[draw, circle] (6) at (7,2) {$x_4$};
\node[draw, circle, inner sep=1.3pt] (7) at (5,0) {$\lnot x_2$};
\node[draw, circle] (8) at (7,0) {$x_3$};
\path[draw,thick,->] (1) -- (4);
\path[draw,thick,->] (4) -- (2);
\path[draw,thick,->] (2) -- (1);
\path[draw,thick,->] (3) -- (4);
\path[draw,thick,->] (2) -- (5);
\path[draw,thick,->] (4) -- (7);
\path[draw,thick,->] (5) -- (6);
\path[draw,thick,->] (5) -- (8);
\path[draw,thick,->] (8) -- (7);
\path[draw,thick,->] (7) -- (5);
\end{tikzpicture}
\end{center}
2017-02-06 20:33:11 +01:00
And the graph for the formula $L_2$ is:
2016-12-28 23:54:51 +01:00
\\
\begin{center}
\begin{tikzpicture}[scale=1.0,minimum size=2pt]
\node[draw, circle] (1) at (1,2) {$x_3$};
\node[draw, circle] (2) at (3,2) {$x_2$};
\node[draw, circle, inner sep=1.3pt] (3) at (5,2) {$\lnot x_2$};
\node[draw, circle, inner sep=1.3pt] (4) at (7,2) {$\lnot x_3$};
\node[draw, circle, inner sep=1.3pt] (5) at (4,3.5) {$\lnot x_1$};
\node[draw, circle] (6) at (4,0.5) {$x_1$};
\path[draw,thick,->] (1) -- (5);
\path[draw,thick,->] (4) -- (5);
\path[draw,thick,->] (6) -- (1);
\path[draw,thick,->] (6) -- (4);
\path[draw,thick,->] (5) -- (2);
\path[draw,thick,->] (5) -- (3);
\path[draw,thick,->] (2) -- (6);
\path[draw,thick,->] (3) -- (6);
\end{tikzpicture}
\end{center}
2017-02-18 13:00:23 +01:00
The structure of the graph tells us whether
it is possible to assign the values
of the variables so
that the formula is true.
It turns out that this can be done
exactly when there are no nodes
$x_i$ and $\lnot x_i$ such that
both nodes belong to the
same strongly connected component.
If there are such nodes,
the graph contains
a path from $x_i$ to $\lnot x_i$
2017-01-08 21:17:46 +01:00
and also a path from $\lnot x_i$ to $x_i$,
2017-02-18 13:00:23 +01:00
so both $x_i$ and $\lnot x_i$ should be true
2017-01-08 21:17:46 +01:00
which is not possible.
2017-02-06 20:33:11 +01:00
In the graph of the formula $L_1$
there are no nodes $x_i$ and $\lnot x_i$
such that both nodes
2017-01-08 21:17:46 +01:00
belong to the same strongly connected component,
2017-05-29 19:39:30 +02:00
so a solution exists.
2017-02-06 20:33:11 +01:00
In the graph of the formula $L_2$
2017-01-08 21:17:46 +01:00
all nodes belong to the same strongly connected component,
2017-05-29 19:39:30 +02:00
so a solution does not exist.
2017-01-08 21:17:46 +01:00
If a solution exists, the values for the variables
2017-02-18 13:00:23 +01:00
can be found by going through the nodes of the
2017-01-08 21:17:46 +01:00
component graph in a reverse topological sort order.
2017-02-06 20:33:11 +01:00
At each step, we process a component
that does not contain edges that lead to an
unprocessed component.
If the variables in the component
have not been assigned values,
2017-01-08 21:17:46 +01:00
their values will be determined
2017-02-06 20:33:11 +01:00
according to the values in the component,
2017-01-08 21:17:46 +01:00
and if they already have values,
2017-02-06 20:33:11 +01:00
they remain unchanged.
2017-05-07 20:18:56 +02:00
The process continues until each variable
has been assigned a value.
2017-01-08 21:17:46 +01:00
2017-02-06 20:33:11 +01:00
The component graph for the formula $L_1$ is as follows:
2016-12-28 23:54:51 +01:00
\begin{center}
\begin{tikzpicture}[scale=1.0]
\node[draw, circle] (1) at (0,0) {$A$};
\node[draw, circle] (2) at (2,0) {$B$};
\node[draw, circle] (3) at (4,0) {$C$};
\node[draw, circle] (4) at (6,0) {$D$};
\path[draw,thick,->] (1) -- (2);
\path[draw,thick,->] (2) -- (3);
\path[draw,thick,->] (3) -- (4);
\end{tikzpicture}
\end{center}
2017-01-08 21:17:46 +01:00
The components are
2016-12-28 23:54:51 +01:00
$A = \{\lnot x_4\}$,
$B = \{x_1, x_2, \lnot x_3\}$,
2017-01-08 21:17:46 +01:00
$C = \{\lnot x_1, \lnot x_2, x_3\}$ and
2016-12-28 23:54:51 +01:00
$D = \{x_4\}$.
2017-01-08 21:17:46 +01:00
When constructing the solution,
2017-02-06 20:33:11 +01:00
we first process the component $D$
2017-01-08 21:17:46 +01:00
where $x_4$ becomes true.
2017-02-06 20:33:11 +01:00
After this, we process the component $C$
2017-01-08 21:17:46 +01:00
where $x_1$ and $x_2$ become false
and $x_3$ becomes true.
2017-05-29 19:39:30 +02:00
All variables have been assigned values,
2017-01-08 21:17:46 +01:00
so the remaining components $A$ and $B$
2017-02-06 20:33:11 +01:00
do not change the variables.
2017-01-08 21:17:46 +01:00
2017-02-18 13:00:23 +01:00
Note that this method works, because the
2017-05-29 19:39:30 +02:00
graph has a special structure:
if there are paths from node $x_i$ to node $x_j$
2017-01-08 21:17:46 +01:00
and from node $x_j$ to node $\lnot x_j$,
then node $x_i$ never becomes true.
The reason for this is that there is also
a path from node $\lnot x_j$ to node $\lnot x_i$,
and both $x_i$ and $x_j$ become false.
\index{3SAT problem}
2017-05-29 19:39:30 +02:00
A more difficult problem is the \key{3SAT problem},
2017-01-08 21:17:46 +01:00
where each part of the formula is of the form
2016-12-28 23:54:51 +01:00
$(a_i \lor b_i \lor c_i)$.
2017-02-22 20:44:42 +01:00
This problem is NP-hard, so no efficient algorithm
2017-02-28 21:02:48 +01:00
for solving the problem is known.