PAA2007.1 - Projeto 1 - Componentes Fortemente Conectados

Definição do problema

Um componente fortemente conectado (SCC) de um grafo $G(V,E)$ é um conjunto maximal de vértices $C \in V$ tal que para cada $u,v \in C$, existe $u \leadsto v$ e $v \leadsto u$ em $G$.

No exemplo abaixo, o grafo $G$ contendo 10 vértices teve seus SCCs circulados, seguindo a definição acima.

exemploSCC.PNG

A partir desta definição de componentes fortemente conectados, foram implementados três algoritmos para encontrar as SCCs de um dado grafo $G$, detalhados a seguir.

Convenções

Foram adotadas as seguintes convenções nas implementações e nas suas análises de complexidade:

  • Seja um grafo $G(V,E)$. Então $n$= |V| e $m$= |E|
  • SCC denota o conjunto de componentes fortemente conectados de $G$
  • SCC($v$) denota o componente fortemente conectado do vértice $v$
  • $G_T(V,E_T)$ é definido como o grafo transposto de $G(V,E)$, tal que $E_T = {(u,v)}$ para todo $(v,u) \in E$. Em outras palavras, $G_T$ é o grafo $G$ com as arestas invertidas.
  • Seja $C$ um conjunto. |$C$| denota a cardinalidade do conjunto $C$.

Convenções nas implementações

Nos três algoritmos implementados, foram utilizadas as seguintes definições em comum:

  • Node denota um vetor de inteiros vector< int >
  • Graph denota um vetor de nós Node
  • SCC denota um vetor de inteiros vector< int >

Algoritmo 1 $O(n*(n+m))$

Descrição e análise de complexidade

Como abordagem inicial, o método para encontrar as SCCs de um grafo consiste em, a partir de cada vértice $v \in V$, realizar uma DFS para encontrar todos os vértices $u \in V$ tal que existe $v \leadsto u$. Depois, iniciamos o conjunto de SCCs com um SCC para cada vértice $v$ do grafo. Finalmente, para cada par de vértices $u,v \in V$ tal que existem $v \leadsto u$ e $u \leadsto v$, determinamos que $u,v$ pertencem ao mesmo SCC.
Nota: se existem $v \leadsto u$ e $u \leadsto v$, por transitividade, fazemos SCC($v$) $\leftarrow$ SCC($u$) $\leftarrow$ SCC($v$) $\cup$ SCC($u$).

O seguinte pseudo-código descreve o algoritmo:

find_SCC_Quadractic(G): # acha os SCCs do grafo G
    // passo 1
    para cada vértice v pertencente a V, fazer:
        DFS em G a partir de v, marcando vértice u visitado como alcançável a partir de v
    // passo 2
    para cada vértice v pertencente a V, fazer:
        criar um conjunto Union-Find contendo apenas v, representando uma SCC
    // passo 3
    para cada vértice v pertencente a V, fazer:
        para cada vértice u marcado como alcançável a partir de v, fazer:
            se v também for alcançável a partir de u, fazer:
                unir conjuntos Union-Find de u e de v
  • O passo 1 consiste em uma DFS (busca em profundidade) a partir de cada vértice $v \in V$ para encontrar o conjunto $Cv$ \subset V$ tal que, para todo $u \in Cv$, existe $v \leadsto u$ em $G$. Esta DFS tem custo $O(n+m)$, e como é repetida $n$ vezes, o custo total deste passo é $O(n*(n+m))$.
  • No passo 2, a criação de cada conjunto usando Union-Find $v \in V$ tem custo $O(1)$. Como isto é repetido $n$ vezes, este passo tem custo total $O(n)$.
  • No passo 3, determinam-se quais vértices pertencem ao mesmo SCC. Se utilizarmos uma matriz Pn x n para armazenar os vértices $u$ alcançáveis a partir de cada vértice $v$, identificar quais vértices pertencem ao mesmo SCC pode ser feito em tempo $\Theta (n^2)$. Como são feitas no máximo $n$ uniões de conjuntos, e cada união utilizando Union-Find com compressão de caminhos e união por altura custa $O(\alpha(n))$, este passo pode ser feito com custo total $\Theta(n^2) + O(n*\alpha(n))$.

Desse modo, alcançamos a complexidade total de $O(n*(n+m))$.

Prova de corretude

A corretude do algoritmo vem da própria definição do problema, já que o algoritmo encontra explicitamente os caminhos $v \leadsto u$ e $u \leadsto v$ para todo $u,v \in V$ e une os SCCs de $u,v$ nesse caso. Como este processo é executado para todo vértice do grafo, todos os SCCs de $G$ são determinados.

Implementação usando Union-Find com compressão de caminho e união por altura

Para a implementação do algoritmo quadrático, foi usada a classe Union-Find com compressão de caminhos e união por altura a fim de obter a complexidade $O(\alpha(n))$ para união dos SCCs. A referida implementação segue abaixo:

// find_SCC_Quadractic(G): # acha componentes fortemente conectados de um grafo em O(n*(n + m))
UnionFind *find_SCC_Quadractic( Graph G )
{
    int n = (int) G.size();
 
    // passo 1: encontra matriz de caminhos P do grafo
    // inicializa P toda com false: Theta(n^2)
    vector< vector < bool > > P( n, vector<bool>(n,false) );
 
    // DFS a partir de todo nó v, fazendo P[v,u] = true para todo u alcançável a partir de v
    for(int v =0; v < n; v++) {
        DFS(G, v, P);
    }
 
    // passo 2: cria estrutura UNION-FIND para conter as SCCs
    // inicialmente, contem n conjuntos disjuntos (1 para cada vertice do grafo)
    UnionFind *uf = new UnionFind(n);
 
    // passo 3: iterar na matriz P, encontrando vértices que pertencem ao mesmo SCC: Theta(n^2)
    for(int u =0; u < n; u++) {
        for(int v=0; v < n; v++) {
            // se existe caminho de v a u e vice-versa, une conjuntos de v e u em um só SCC
            if (P[u][v] && P[v][u] && uf->getClass(u) != uf->getClass(v)) {
                uf->unionClass( u, v );                 //  O(alpha(n))
            }
        }
    }
 
    return uf;
}
 
// DFS_Visit: visita vértice u do grafo G, atualizando o vetor marked
void DFS_Visit( Graph G, int u, vector<bool> & marked) {
    marked[u] = true;
 
    for(int i = 0; i < (int)G[u].size(); i++) {
        int v = G[u][i];
        if (!marked[v]) {
            DFS_Visit(G, v, marked);
        }
    }
}
 
// DFS: realiza uma DFS no grafo G iniciando do vértice u.
//            Atualiza a linha u da matriz P de bool, indicando quais
//            vértices são alcancáveis a partir de u
void DFS( Graph G, int u, vector< vector< bool > > & P ) {
 
    DFS_Visit(G, u, P[u]);
}

Algoritmo 2 $O(|SCC|*(n+m))$

Descrição e análise de complexidade

Podemos melhorar o primeiro algoritmo, atingindo uma menor complexidade assintótica, partindo da seguinte idéia: pela DFS a partir de um vértice $v$, encontramos todos os vértices $u$ tal que existe $v \leadsto u$ em $G$. De modo análogo, se fizermos um grafo transposto $G_T$ de $G$, e realizar outra DFS a partir de $v$ em $G_T$, encontraremos todos os vértices $u$ tal que existe $u \leadsto v$ em $G$. Depois disso, fazendo-se a interseção destes conjuntos de vértices encontrados pelas duas DFSs, podemos determinar SCC($v$) completamente. Podemos em seguida proceder para remover todos os vértices pertencentes a SCC($v$) do grafo $G$, e continuar o processo de busca das SCCs.

O pseudo-código abaixo descreve o algoritmo:

find_SCC_almost_linear(G): # acha SCCs de um grafo em O(|SCC|(n+m)), onde SCC é o cjto de SCCs
    label = 0;
    // passo 1
    encontrar grafo G_T transposto de G
    para cada vértice v do grafo não rotulado como pertencente a um SCC, fazer:
        // passo 2
        executa DFS em G a partir de v, fazendo (arestas que saem de v):
            marcar todo vertice x visitado como alcancavel a partir de v: R_G[v,x] = true
        // passo 3
        executa DFS em G_T a partir de v, fazendo (arestas que chegam em v):
            marcar todo vertice x visitado como alcancavel a partir de v: R_G_T[v,x] = true
        // passo 4
        varrer R_G e R_G_T, sendo que a intersecao U entre eles é o SCC do vértice v:
            rotular todos os vértices de U com label
        label++;
  • No passo 1, encontra-se o grafo $G_T(V,E_T)$ transposto de $G$. Para isso, devem-se percorrer todos os vértices e todas as arestas de $G$, portanto o custo é $\Theta(n+m)$.
  • O passo 2 consiste em uma DFS a partir do vértice $v \in V$ para encontrar o conjunto $Cv$ \subset V$ tal que, para todo $u \in Cv$, existe $v \leadsto u$ em $G$. O custo da DFS é $O(n+m)$.
  • O passo 3, de forma análoga, consiste em uma DFS a partir do vértice $v \in V$ para encontrar o conjunto $Cv$ \subset V$ tal que, para todo $u \in Cv$, existe $u \leadsto v$ em $G$. O custo da DFS é $O(n+m)$.
  • No passo 4, encontra-se a interseção dos conjuntos encontrados com as DFSs acima. Como devemos percorrer R_G e R_G_T inteiramente para encontrar a interseção, este passo tem custo $O(n)$.

Os passos 2, 3 e 4 são feitos no máximo |SCC| vezes. Por isso, o custo total do algoritmo é $\Theta(n+m) + |SCC|*(O(n) + O(n+m))$. Desse modo, alcançamos a complexidade total de $O(|SCC|*(n+m))$.

Prova de corretude

De forma parecida ao primeiro algoritmo, a corretude desta implementação vem da própria definição do problema. A primeira DFS encontra os vértices alcancáveis a partir de $v$, e a segunda encontra todos os vértices que possuem um caminho para $v$. Desse modo, a interseção destes dois conjuntos nos dá SCC($v$). Como o algoritmo executa enquanto houver vértice não pertencente a um SCC, o algoritmo garantidamente encontra todos os SCCs do grafo $G$.

Implementação

// acha SCCs de um grafo em O(|SCC|(n+m)), onde SCC é o cjto de SCCs
SCC *find_SCC_almost_linear( Graph G )
{
    int n = (int) G.size();
 
    SCC *scc = new SCC(n, -1);
 
    Graph G_T(n);
    // transpor grafo G em G_T
    for(int u = 0; u < n; u++) {
        for(int i = 0; i < (int)G[u].size(); i++) {
            int v = G[u][i];
            G_T[v].push_back(u);
        }
    }
 
    int label = 0;
 
    // para cada vértice v do grafo não pertencente a um SCC, fazer:
    //        executa DFS em G a partir de v(arestas que saem de v), fazendo:
    //            marcar todo vertice x visitado como alcancavel a partir de v: P_G[v,x] = true
    //        executa DFS em G_T a partir de v(arestas que chegam em v), fazendo:
    //            marcar todo vertice x visitado como alcancavel a partir de v: P_G_T[v,x] = true
    vector< vector < bool > > P_G( n, vector<bool>(n,false) );
    // inicializa P toda com zeros: Theta(n^2)
    vector< vector < bool > > P_G_T( n, vector<bool>(n,false) );
    // executa DFS a partir de todo no v do grafo não pertencente a um SCC
    for(int v = 0; v < n; v++) {
        if ((*scc)[v] == -1) {
            DFS_2(G, v, P_G[v]);
            DFS_2(G_T, v, P_G_T[v]);
            // varrer P_G e P_G_T, sendo que a intersecao U entre eles é o SCC do vértice v:
            // rotular todos os vértices de U com label
            (*scc)[v] = label;
            for(int u =0; u < n; u++) {
                if (P_G[v][u] && P_G_T[v][u]) {
                    (*scc)[u] = label;
                }
            }
            label++;
        }
    }
    return scc;
}
 
// DFS_Visit_2: visita vértice u do grafo G, atualizando o vetor marked
void DFS_Visit_2( Graph G, int u, vector< bool > & marked) {
    marked[u] = true;
 
    for(int i = 0; i < (int)G[u].size(); i++) {
        int v = G[u][i];
        if (!marked[v]) {
            DFS_Visit_2(G, v, marked);
        }
    }
}
 
// DFS_2: realiza uma DFS no grafo G iniciando do vértice u.
//            Atualiza um vetor de bool, indicando quais
//            vértices são alcancáveis a partir de u
void DFS_2( Graph G, int u, vector< bool > & marked ) {
 
    DFS_Visit_2(G, u, marked);
}

Algoritmo 3 $\Theta(n+m)$

Descrição e análise de complexidade

Podemos melhorar o algoritmo através de uma implementação simples, mas que possui uma prova de corretude não trivial. De modo similar ao algoritmo 2, este algoritmo faz uso do grafo $G_T$ transposto de $G$. O funcionamento do algoritmo pode ser visto no seguinte pseudo-código:

find_SCC_linear(G): # acha componentes fortemente conectados de um grafo em O(n + m)
    // passo 1
    gerar grafo G_T transposto de G
    // passo 2: encontrar lista de tempo de término de visita dos vértices por DFS
    lista finish = { }
    enquanto houver vértice v de G não visitado:
        fazer DFS a partir de v, colocando cada u no início de finish como POSWORK de DFS_Visit(u)
    // passo 3: rotular os vértices 
    rótulo = 1;
    para cada nó v de finish não visitado em G_T ainda:
        v.rotulo = rótulo;
        DFS em G_T a partir de v, fazendo u.rotulo = rótulo para u alcançável a partir de v 
        rótulo++;
  • No passo 1, encontra-se o grafo $G_T(V,E_T)$ transposto de $G$. Para isso, devem-se percorrer todos os vértices e todas as arestas de $G$, portanto o custo é $\Theta(n+m)$.
  • O passo 2 consiste em realizar DFS no grafo $G$ para determinar os tempos de término de visita de cada vértice $v$ de $G$ pela DFS. No caso, os vértices finalizados por último se encontram nas primeiras posições da lista finish. Este passo consiste em DFS no grafo $G$, e portanto custa $O(n+m)$.
  • De forma parecida, o passo 3 também realiza DFS no grafo $G_T$, mas respeitando a ordem dos vértices escolhidos para iniciar a busca pela lista finish. Cada vértice alcançado na DFS é rotulado com o índice do rótulo atual, identificando a qual SCC cada vértice pertence. Este passo também custa $O(n+m)$.

Desse modo, alcançamos a complexidade total de $\Theta(n+m)$.

Prova de corretude

Uma prova completa da corretude do algoritmo explicado acima encontra-se no livro "Introduction to Algorithms" de Cormen et al. Abaixo, apresentamos uma série de lemas e propriedades para justificar a corretudo do algoritmo. Para a prova formal destes lemas, sugerimos a consulta ao livro citado.

Lema 1: $G$ e $G_T$ possuem os mesmos SCCs.
Prova:
$u$ e $v$ são alcançáveis mutuamente em $G$ se e somente se forem alcançáveis mutuamente também em $G_T$.

Definição 1:
Definimos o grafo $SCC_G$ como o grafo das componentes fortemente conectadas de $G$:

  • Cada vértice de $SCC_G$ representa uma SCC de $G$.
  • Existe uma aresta [[($SCC_1,SCC_2$)]] em $SCC_G$ se existem $u,v$ de $G$ tal que $u \in SCC_1$ e $v \in SCC_2$.

O grafo de componentes fortemente conectadas do exemplo 1 segue abaixo:

componentGraph.PNG

Definição 2:
De modo análogo à definição 1, definimos o grafo $SCC_G__T$ como o grafo das componentes fortemente conectadas de $G_T$.

A partir do lema 1 e da definição de grafos transpostos, podemos facilmente provar que o grafo $SCC_G$ é composto pelos mesmos vértices de $SCC_G__T$, mas com as arestas invertidas. Ou seja, $SCC_G__T$ é o grafo transposto de $SCC_G$.

Lema 2: $SCC_G$ e $SCC_G__T$ são DAGs (grafo acíclicos direcionados, do inglês directed acyclic graphs).
Prova: encontra-se no livro citado, mas uma intuição é a seguinte: suponha que existisse um ciclo em $SCC_G$. Sejam $SCC_1,SCC_2$ dois vértices deste ciclo. Se isso fosse possível, existiriam $SCC_1 \leadsto SCC_2$ e $SCC_2 \leadsto SCC_1$ em $SCC_G$. Porém, isso contradiria a definição de componentes fortemente conectados, já que $SCC_1$ e $SCC_2$ não poderiam ser SCCs diferentes.

Lema 3: Sejam $SCC_1$ e $SCC_2$ duas SCCs distintas de $G$. Suponha que existe uma aresta $(u,v)$ em $G$ tal que $u \in SCC_1$ e $v \in SCC_2$. Seja $f[u]$ e $f[v]$ os respectivos tempos de término de visita dos vértices $u$ e $v$ em uma DFS em $G$. Então $f[u]$ > $f[v]$.
Prova: a prova completa se encontra no livro de Cormen et al.

Definição 3:
Seja $SCC_1$ um SCC de $G$. Definimos $f(SCC_1) = max_{u \in SCC_1}\{f[u]\}$.

A partir dos lemas acima, podemos descrever a corretude do algoritmo da seguinte forma: quando executamos a DFS em $G_T$, começamos a partir do SCC $C$ que contém o vértice $v$ tal que $f(C)$ é máximo. Se partimos de $v$ para realizar a DFS, podemos visitar exatamente todos os vértices que pertencem a $SCC(v)$. Depois disso, a próxima raiz da DFS é um vértice $u$ pertencente ao SCC $C'$ tal que $f(C')$ é máximo para todo $C' \neq C$. Esta DFS visita somente todos os vértices de $C'$, já que as arestas de saída de $C'$ só podem ser a $C$, cujos vértices já visitamos anteriormente. Repetimos o processo até visitar todos os SCCs de $SCC_G__T$.

Em suma, estamos visitando vértices de $SCC_G__T$ em ordem inversa de sua ordenação topológica. A prova disto também se encontra no livro de Cormen et al.

Implementação

Abaixo a implementação do algoritmo linear, que como dito anteriormente, é muito simples se comparado à sua prova de corretude.

// DFS_Visit_Ordem: realiza uma visita de uma DFS em um grafo direcionado,
//                atualizando uma lista finish de tempos de terminos de visita de vértices
void DFS_Visit_Ordem( Graph G, int u, vector<bool> & marked, list<int> & finish) {
    marked[u] = true;
 
    for(int i = 0; i < (int)G[u].size(); i++) {
        int v = G[u][i];
        if (!marked[v]) {
            DFS_Visit_Ordem(G, v, marked, finish);
        }
    }
    finish.push_front(u);
}
 
// DFS_Ordem: realiza uma DFS em um grafo direcionado,
//        atualizando uma lista finish nao crescente de tempos de terminos de visita de vértices
void DFS_Ordem( Graph G, list<int> & finish ) {
 
    vector<bool> marked(G.size(), false);
    for(int u = 0; u < (int)G.size(); u++) {
        if (!marked[u]) {
            DFS_Visit_Ordem(G, u, marked, finish);
        }
    }
}
 
// DFS_Visit_SCC: realiza uma visita de uma DFS em um grafo direcionado,
//                atualizando um vetor indicando a qual SCC o vértice u pertence
void DFS_Visit_SCC( Graph G, int u, vector<bool> & marked, SCC & scc, int label) {
    marked[u] = true;
 
    for(int i = 0; i < (int)G[u].size(); i++) {
        int v = G[u][i];
        if (!marked[v]) {
            DFS_Visit_SCC(G, v, marked, scc, label);
        }
    }
    scc[u] = label;
}
 
// DFS_SCC: realiza uma visita de uma DFS em um grafo direcionado iniciando do vértice u.
//            Atualiza uma lista não crescente finish de tempos de término de visita de nós.
void DFS_SCC( Graph G, list<int> finish, SCC & scc ) {
    int label = 0;
    vector<bool> marked(G.size(), false);
 
    for(list<int>::iterator it = finish.begin(); it != finish.end(); it++) {
        int u = *it;
        if (!marked[u]) {
            DFS_Visit_SCC( G, u, marked, scc, label );
            label++;
        }
    }
}
// find_SCC_linear(G): # acha componentes fortemente conectados de um grafo em O(n + m)
SCC *find_SCC_linear( Graph G )
{
    int n = (int)G.size();
 
    SCC *scc = new SCC(n, -1);
 
    // Passo 1: encontrar grafo G_T transposto de G
    Graph G_T(n);
    for(int u = 0; u < n; u++) {
        for(int i = 0; i < (int)G[u].size(); i++) {
            int v = G[u][i];
            G_T[v].push_back(u);
        }
    }
 
    // Passo 2: encontrar lista de tempo de término de visita de G
    // Inicializa lista finish: lista de nos a serem visitados futuramente
    list<int> finish;
 
    // fazer DFS no grafo original, inserindo vertices finalizado no inicio de Ordem
    DFS_Ordem(G, finish);
 
    // Passo 3: rotular vértices
    // fazer DFS nos vertices do grafo transposto, atualizando seu rotulo de SCC
    DFS_SCC(G_T, finish, *scc);
 
    return scc;
}

Aplicação dos algoritmos: 2-SAT

Definição do problema

O problema de satisfabilidade consiste em determinar se existe uma atribuição de variáveis em uma expressão booleana que a faça ser avaliada para TRUE.
O algoritmo 2-Satisfatibilidade (2-SAT) é um caso especial de satisfabilidade, em que as expressões são escritas na forma conjuntiva normal (CNF) com duas variáveis por cláusula (2-CNF) - ou seja, a expressão booleana consiste em disjunções (AND) de cláusulas, em que cada cláusula é uma disjunção (OR) de literais. Abaixo um exemplo 1 de uma expressão booleana escrita na 2-CNF:

$(A \vee B) \wedge (C \vee D) \wedge (A \vee D)$

Modelagem como um grafo

Para modelar uma expressão booleana na 2-CNF como um grafo, temos que partir da seguinte idéia:

  • uma cláusula na 2-CNF $(A \vee B)$ é equivalente a $(\~A \rightarrow B) \wedge (\~B \rightarrow A)$

Desse modo, podemos reescrever a expressão usada no exemplo 1 como:

$(\~A \rightarrow B) \wedge (\~B \rightarrow A) \wedge (\~D \rightarrow C) \wedge (\~C \rightarrow D) \wedge (\~A \rightarrow D) \wedge (\~D \rightarrow A)$

Ou seja, transformamos nossa expressão na 2-CNF em uma expressão formada somente por conjunções (AND) de implicações.

Podemos perceber que uma expressão nesse formato não será satisfatível se ela contiver um par de implicações tal que:

$(\~A \rightarrow A) \wedge (A \rightarrow \~A)$

Neste caso, é óbvio que, qualquer que seja a atribuição escolhida para a variável $A$, será impossível satisfazer a expressão.
Nota: Não necessariamente o par de implicações acima deve aparecer explicitamente na expressão. Deve-se levar em conta também a transitividade. Desse modo, temos a seguinte equivalência de expressões:

$(A \rightarrow \~A) \wedge (\~A \rightarrow D) \wedge (D \rightarrow A) \equiv (A \rightarrow \~A) \wedge (\~A \rightarrow A) \wedge (\~A \rightarrow D) \wedge (D \rightarrow A)$.

Ou seja, neste caso a expressão não é satisfatível.

Sendo assim, podemos modelar o seguinte grafo $G(V,E)$ para representar a expressão booleana na forma de conjunções (AND) de implicações:

  • Cada vértice $v \in V$ representa um literal da expressão
  • Existe uma aresta $(u,v) \in E$ somente se existe a implicação $(u \rightarrow v)$ na expressão

Dessa forma, um grafo $G$ formado a partir do exemplo 1 acima seria:

grafo2SAT.JPG

O problema de 2-SAT agora se reduz a determinar se existe uma SCC em $G$ que contenha alguma variável $A$ e também sua negação $\~A$. Neste caso, isso indica que existem $A \leadsto \~A$ e $\~A \leadsto A$. Como argumentamos, isso indica que a expressão NÃO é satisfatível.

O algoritmo do 2-SAT pode então ser descrito pelo seguinte pseudo-código:

2-SAT-Problem(G): # retorna TRUE caso uma expressão na forma 2-CNF seja satisfatível
    // passo 1
    interpretar entrada para representar expressão boolean na 2-CNF

    // passo 2
    converter expressão lida no passo 1 para conjunções de implicações

    // passo 3
    gerar grafo G a partir da expressão criada no passo 3

    // passo 4
    encontrar SCCs do grafo G

    // passo 5
    para cada SCC entrada no passo 4, fazer:
        se tanto a variável A quanto ~A pertencer a esse SCC, retornar FALSE

    retornar TRUE

Resultados

Usou-se uma bateria de testes com instâncias de 2-SAT para teste do desempenho das 3 implementações do problema de encontrar as SCCs de um grafo: usando o Algoritmo 1 $O(n*(n+m))$, Algoritmo 2 $O(|SCC|*(n+m))$ e Algoritmo 3 $\Theta(n+m)$. Foram testados grafos com 20, 100, 200, 1000, 2000, 20000 e 40000 vértices. Além de variar o número de vértices, variou-se também o número de arestas em cada grafo.

Abaixo, uma tabela com o desempenho de cada algoritmo para uma amostra dos testes aplicados:

tabresult2sat2.PNG

O gráfico abaixo representa o desempenho dos algoritmos na coleção toda de testes:

grafico2.PNG

Conforme esperado, percebemos que o Algoritmo 3 é assintoticamente mais rápido do que os outros 2 algoritmos, sendo que o mais lento é o Algoritmo 1, de complexidade quadrática.
No gráfico, o eixo horizontal representa o log do número de vértices do grafo usado no teste, e o vertical o tempo em segundos gasto pelo respectivo algoritmo para encontrar as componentes fortemente conectadas do grafo (ou seja, não foi computabilizado o tempo para leitura dos arquivos de entrada ou a verificação da satisfatibilidade da expressão fornecida).
Podemos observar que, para grafos com muitos vértices, 20000 e 40000 vértices (2 últimos degraus), o desempenho do algoritmo 1 e do algoritmo 2 foi muito similar. Isso certamente se deve ao fato de o número de componentes fortemente conectadas de tais grafos serem números próximos a $n$, o número de vértices.

No total, da bateria de 117 testes aplicados, o número de expressões satisfatíveis foi de 25, contra 92 não satisfatíveis. As expressões satisfatíveis foram as com número de literais igual a 10000 ou 20000.

Unless otherwise stated, the content of this page is licensed under Creative Commons Attribution-Share Alike 2.5 License.