After solving coloring problems with an ILP in the last exercise, we now want to study the strength of SAT solvers for this purpose. We continue using the same directory COLORING and main.py as yesterday
We use the same binary variables as in the assignment ILP formulation, i.e. one per vertex and color. SAT solvers usually read a SATISFIABILITY problem in conjunctive normal for (CNF). Here, a clause is a multi-OR function on a set of literals (variables or their negations) and we look for a truth assignment satisfying all given clauses. However, they cannot easily minimize or maximize an objective. But, for a given number k, we can use them to check if there is a k-coloring. We just need to search the minimum k in an outer loop.
We can easily translate each ILP constraint into a clause, e.g. for vertex i, a clause
x[i,1] v x[i,2] v ... v x_[i,k]requires the vertex to be colored with one of k colors and for an edge {v,w}, a clause
-x[v,j] v -x[w,j]forces that both endpoints cannot be colored with color j simultaneously, where - stands for a negation.
We will be using the SAT solver kissat developed by Armin Biere. As kissat does not have a python API, we will simply write out a CNF problem file in DIMACS format which is straight-forward. The first non-comment line has to start with
p cnf <number of variables> <number of clauses>.
Variables are numbered 1..<number of variables>. Then it contains one line for every clause, listing the literals in that clause. Each clause line is terminated with a 0. Negated variables are indicated by a minus in front of the variable index. Here is an example with 3 variables and 2 clauses
c I am a comment
p cnf 3 2
1 2 3 0
-2 -3 0It has a several truth assignments, e.g. x[1] = 0, x[2] = 0, x[3] = 1. To make things easier, we prepared a file ass_kissat.py that eliminates most of the technicalities:
cp /home/sheld/public/ass_kissat.py .
Similarly to yesterday, you can activate it via
import ass_kissat as colmip
The function color(…) first computes lower and upper bounds as yesterday. Then it conducts a simple linear search on k from the lower bound upwards.
You have to add code that writes out the model to the function def solve_k_coloring(G, k, time_limit): using the graph G (a networkx object) and the coloring number k. All other parts, including the call to kissat and reading its result, are already implemented.
Add the code between the following two lines:
##### ADD CODE TO WRITE THE SAT MODEL FOR K-COLORING BETWEEN THIS
##### AND THIS LINEOnce you are done, you can compare the running time on the instances that you have seen already, e.g. myciel*.col, DSJC125.*.col, as well as on other instances. Compare with the ILP model (and with exactcolors).
You can also add code to write the solution to the solution file, which is not written yet.
There are various ways to improve the formulation. Be creative!