10. SAT solvers
At the seminar you have learned how to encode problems to SAT. Your task is to create a program that will find a perfect code of a graph using SAT solver:
Note: The set ] contains all the neighbors of as well as itself.
More precisely, you should create a program with the following specification.
Input
First line contains two integers N (number of vertices) and M (number of edges). Then M lines follow, each with two integer the endpoints of an edge. The vertices are labeled as integers from 1 to N. This is the example input which represents path on 4 vertices.
4 3
1 2
2 3
3 4Output
Use standard output for your answer. Answer on the first line single integer - the size of the found perfect code (the set ). (If there is none, print -1) On the second line write space separated integers - labels of vertices that make the set .
For the above example, this could be the answer:
2
1 4Instructions
- Read the task and solve it by yourself. In case of plagiarism, your homework will not be considered solved.
- Then, send a
.zipfile containing your program to jan.pokorny@fit.cvut.cz, the structure of the.zipfile is described in the next section. - The deadline for submission is May 1, 2024, 23:59:59. The deadline is strict.
Program specifications
Send a .zip file with your solution. It will be extracted into its own folder. Then if there is a Makefile, command make will be run (use it to compile your program if you need).
Then the program will be called as ./run.sh graph.txt, where run.sh is your program (make sure it is named that way) which handles the whole computation (can call other programs - encoding, the SAT solver, decoding). The first and only argument is the input graph in the format described earlier.
Provide detailed explanation of your encoding either as a separate .pdf file or as comments inside your encoding procedure.
Preferably use MiniSat.
You can use this code presented at the seminar as a starting point.