@@ -0,0 +1,672 @@
+from boolean import *%0A%0A#      0       1       2          3          4%0A# G = %5B%5B1, 2%5D, %5B0, 3%5D, %5B0, 3, 4%5D, %5B1, 2, 4%5D, %5B2, 3%5D%5D%0A%0Adef graphColouring2SAT(G, k):%0A    conj = %5B%5D%0A    for i in range(len(G)):%0A        conj.append(Or(*((i, j) for j in range(k))))%0A        for j in range(k):%0A            for jj in range(j+1, k):%0A                conj.append(Or(Not((i, j)), Not((i, jj))))%0A        for h in G%5Bi%5D:%0A            for j in range(k):%0A                conj.append(Or(Not((h, j)), Not((i, j))))%0A    return And(*conj)%0A%0Adef SAT2graphColouring(sol):%0A    d = %7Bi: j for (i, j), v in sol.items() if v%7D%0A    out = %5BNone%5D * len(d)%0A    for i, j in d.items():%0A        out%5Bi%5D = j%0A    return out%0A

Add graph colouring conversion