Como um exemplo, considere as figuras abaixo:
Na figura da esquerda temos um grafo com vértices A,B,C,D. Na segunda figura é mostrado um caminho, que começa no vértice C, que passa por cada aresta exatamente uma única vez.
Dada uma instância de um grafo você deverá criar uma fórmula em lógica proposicional cuja valoração que a satisfaz é um caminho euleriano. Para ter certeza de que o grafo possui de fato um caminho euleriano você poderá “trapacear” no jogo anteriormente mencionado (todas as instâncias possuem caminho euleriano).
Utilizar de um SAT-SOLVER para resolver uma entrada na forma normal conjuntiva.
Será necessário ter o python e pip instalados, e ter a biblioteca PySAT instalada para rodar o código.
É possível instalar o PySAT rodando o seguinte comando no terminal:
pip install python-sat
Com o PySAT instalado é necessário executar o comando abaixo na pasta do projeto para que o programa execute e exiba os resultados:
python code.py
Será necessário alterar o conteudo do arquivo entrada.txt
A seguinte tabela representa o grafico da figura 1 acima como uma entrada para o programa:
entrada.txt | Representação com letras |
---|---|
1 2 | A B |
1 3 | A C |
2 1 | B A |
2 3 | B C |
2 4 | B D |
3 1 | C A |
3 2 | C B |
3 4 | C D |
4 2 | D B |
4 3 | D C |
Cada linha no arquivo representa a conexão entre os vértices, é necessário colocar todos os possíveis caminhos no arquivo, sem repetição e em ordem crescente dos possíveis caminhos.
Executando o programa com o grafo da figura 1, o programa vai perguntar se o usuário deseja exibir a matriz de passos que é gerada com a entrada:
Com essa matriz é executada a função resolver que vai dizer na primeira linha da saída se é possível encontrar uma resolução com um determinado passo inicial. Exemplo de possíveis saidas:
Passo inicial inválido | Passo inicial válido |
---|---|
Se for uma resolução válida, teremos mais 3 linhas:
- Na segunda linha temos uma lista com todos os passos válidos se existerem, para resolver esse problema,os passos estão em ordem crescente mas não representam a ordem que deve ser feitos os passos, apenas quais são eles.
- Na terceira linha (opcional) mostra quais os conjunto de vértices vão ser usados para resolver o problemas, mas não estão ordenados como na linha 2;
- Na quarta linha da saída (opcional) mostra qual seria a sequência dos vértices que deve ser seguida para resolver o problema.
Essa saída será exibida para um array de possíveis primeiros passos gerado pela matriz. De tal modo que se as valorações forem falsas, então o grafo de entrada não possui um caminho eureliano, mas se tiver ao menos uma verdadeira significa que existe um caminho eureliano.