Skip to content

Scroga/SAT-Project

Repository files navigation

Documentation

Problem description

The Rural Postman problem involves finding a cycle in a graph that efficiently covers specific edges while adhering to certain limitations. Specifically, given an undirected graph $G$ with a set of nodes and edges, along with a subset $F$ of required edges, the challenge is to determine if there exists a cycle that includes every edge in $F$, uses at most $k$ edges in total. More information about the Rural Postman problem can be found online.

An example of a valid input format is:

5
4
0 1 1
0 2 0
1 2 0
1 3 0
2 3 1
2 4 0

where the first line is the number of vertices in th graph. Second line is k (maximum length of the cycle). The other lines represent the edges of the graph. The first two numbers of the lines are the indecies of the vertices that form the edge, the third number of the line is a value 1 or 0, True or False, which represents whether the edge is required (in a subset F).

if the cycle exists, the output will be the edges in the found cycle and their indices

Cycle contains edges:
(0, 1):  index 1
(0, 2):  index 2
(1, 3):  index 4
(2, 3):  index 5

Encoding

The problem is encoded using variables, where each edge in the graph is represented by a variable that indicates whether or not the edge is in a cycle. Each variable is represented by an integer, and variables are numbered starting from 1.

To represent the decision problem of determining whether there is a cycle of length less than or equal to $k$ in the graph $G$ that contains every edge in $F$ the graph, we use the following constraints:

  • The cycle must include all edges from $F$, so all variables corresponding to edges in $F$ must be set to $True$ in the CNF.

  • The cycle must contain no more than $k$ edges, so all combinations of more than $k$ edges are not allowed.

  • All edges in the cycle must have at least two neighboring edges (each of its vertices must have a degree of at least 2); otherwise, the edge cannot be part of the cycle.

  • All edges in the cycle must have no more than two neighboring edges. Any combination of more than two neighbors is not allowed to be true in the CNF.

  • All edges form the subset $F$ must be in the same component.

User documentation

Basic usage:

rural_postman.py [-h] [-i INPUT] [-o OUTPUT] [-s SOLVER] [-v {0,1}]

Command-line options:

  • -h, --help : Show a help message and exit.
  • -i INPUT, --input INPUT : The instance file. Default: "input.in".
  • -o OUTPUT, --output OUTPUT : Output file for the DIMACS format (i.e. the CNF formula).
  • -s SOLVER, --solver SOLVER : The SAT solver to be used.
  • -v {0,1}, --verb {0,1} : Verbosity of the SAT solver used.

Additionally, the project repository contains Python file graph_generater.py, which generates a complete graph with $n$ vertices. This simple script writes the graph in the required format for the rural_postaman.py file. The subset $F$ will contain 2 edges (the first generated edge and the last generated edge), and the $k$ will be set by the user.

Basic usage:

graph_generater.py [-h] [-n INT] [-k INT] [-o OUTPUT]

Command-line options:

  • -h, --help : Show a help message and exit.
  • -n INT, --nr_nodes INt : The number of vertices. Default: 4.
  • -k INT, : Max. number of edges in the cycle. Default: 4.
  • -o OUTPUT, --output OUTPUT : Output file for the script rural_postman.py.

Example instances

  • input-5.in: A simple graph containing 5 vertices and having a cycle of length less than or equal to 4 edges.
  • input-6-unsat.in: A simple graph containing 6 vertices, doesnt contain a cycle of length less than or equal to 6 edges.
  • input-7-unsat.in: Graph in the shape of a star, doesnt contain any cycles.
  • input-7.in: Slightly more complex graph that contain 7 vertices.
  • input-11.in: Complex multiple component graph that contain 11 vertices.
  • input-hard.in: Completed graph with 10 vertices and 45 edges.

Experiments

Experiments were run on AMD Ryzen 9 5900HX and 16 GB RAM on Ubuntu inside WSL2 (Windows 11).

We focus on the graph generated by the graph_generater.py script. The graph will have only two edges, but we aim to test how the number of vertices in the complete graph and $k$ affect the runtime of the SAT solver. For this purpose, I wrote a script run_experiment.sh to measure the processing time taken by the SAT-solver to compute the CNF generated by the rural_postman.py script. All results of run_experiment.sh are written to the execution_times.log file.

  • N - the number of vertices
  • K - the max. length of the cycle
  • time (s)
N \ K 1 2 3 4 5 6 7 8
1 0.223 0.251 0.253 0.251 0.242 0.267 0.232 0.234
2 0.049 0.052 0.051 0.050 0.050 0.048 0.047 0.047
3 0.049 0.049 0.255 0.246 0.186 0.191 0.181 0.181
4 0.052 0.049 0.046 0.051 0.048 0.048 0.051 0.051
5 0.052 0.053 0.054 0.061 0.056 0.057 0.053 0.054
6 0.196 0.200 0.304 0.341 0.441 0.551 0.576 0.454
7 13.236 13.562 22.185 28.980 61.849 162.047 383.051 686.601

From the results of the experiments, it is evident that the performance of the SAT solver significantly degrades as the number of vertices N and the maximum cycle length K increase. While the program handles small graphs efficiently (for example: $N$ $\leq$ 6 and $K$ $\leq$ 5), the runtime rapidly increases for larger graphs and cycles. For instance:

  • When $N$ = 7 and $K$ = 8, the execution time reaches 686.601 seconds, showing exponential growth compared to smaller values.
  • For larger graphs ($N$ > 6), even small increments in K result in a significant increase in processing time, indicating that the program struggles with scalability.

This demonstrates that the my implementation is not efficient for larger problem instances. The inefficiency likely arises due to the exponential growth in the size of the CNF formula as the graph and constraints increase.

About

Solving Postman Problem

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published