A simple python code which reduces the Graph Colorablity Problem to Boolean Satisfiability Problem.
- Python 3
- minisat solver from https://github.com/niklasso/minisat
- cd to your home directory
cd ~ - create new folder for git repositories
mkdir gitRepos - cd to the newly created folder
cd gitRepos - clone this repo to you folder
git clone https://github.com/hackrush01/GCPToSAT.git - cd to the repo
cd GCPToSAT - run
sudo pip3 install -r pip.txt - run using
python3 GCP_To_SAT.py <path-to-graph-file>
Note: Complete installation instructions for MiniSat Solver are mentioned in it's respective repository but in short:
- cd to your git repo folder created above
cd ~/gitRepos - clone minisat
git clone https://github.com/niklasso/minisat.git - cd to minisat directory
cd minisat - install using
sudo make install
Just install the minisat solver in your preferred linux distro. After that just execute the python file.
Make a graph.txt file in the same directory as the git repository or run the program as follows
python3 GCP_To_SAT.py <path-to-graph-file>.
It's important to note that the graph text file must adhere to the standard input format i.e.
- First line contains exactly one number defining the number of vertices.
- After that each line should contain exactly one edge with space separated vertices.(e.g. 5 8, indicates an edge between 5th and 8th vertices)
- All edges are 1-indexed.
- Since the graph is undirectional, so the edges should not be repeated. It doesn't change the solution but the number of clauses increases, decreasing the performance. One example graph.txt file is included.