Issue #141 is started

Author: Hamid Gasmi

4-np-complete-problems/1-np_complete_problems/sudokusolver.py

@@ -0,0 +1,80 @@
+import itertools
+import os
+
+puzzle=[
+    "5***1***4",
+    "***2*6***",
+    "**8*9*6**",
+    "*4*****1*",
+    "7*1*8*4*6",
+    "*5*****3*",
+    "**6*4*1**",
+    "***5*2***",
+    "2***6***8",
+]
+
+clauses = []
+
+digits = range(1, 10)
+
+def varnum(i, j, k):
+    assert(i in digits and j in digits and k in digits)
+    return 100 * i + 10 * j + k
+
+def exactly_one_of(literals):
+    clauses.append([l for l in literals])
+
+    for pair in itertools.combinations(literals, 2):
+        clauses.append([-l for l in pair])
+
+# cell [i, j] contains exactly on digit
+for (i, j) in itertools.product(digits, repeat=2):
+    exactly_one_of([varnum(i, j, k) for k in digits])
+
+# k appears exactly once in row i
+for (i, k) in itertools.product(digits, repeat=2):
+    exactly_one_of([varnum(i, j, k) for k in digits])
+
+# k appears exactly once in column j
+for (j, k) in itertools.product(digits, repeat=2):
+    exactly_one_of([varnum(i, j, k) for k in digits])
+
+# k appears exactly once in a 3x3 block:
+for (i, j) in itertools.product([1, 4, 7], repeat=2):
+    for k in digits:
+        exactly_one_of([varnum(i + deltai, j + deltaj, k) for (deltai, deltaj) in itertools.product(range(3), repeat = 2)])
+
+for (i, j) in itertools.product(digits, repeat=2):
+    if puzzle[i - 1][j - 1] != "*":
+        k = int(puzzle[i - 1][j - 1])
+        assert(k in digits)
+        #[i,j] already contains k:
+        clauses.append(varnum(i, j, k))
+
+with open('temp.cnf', 'w') as f:
+    f.write("p cnf {} {}\n".format(999, len(clauses)))
+    for c in clauses:
+        c.append(0)
+        f.write(" ".join(map(str, c))+"\n")
+
+os.system("minisat tmp.cnf tmp.sat")
+
+with open("tmp.sat", "r") as satfile:
+    for line in satfile:
+        if line.split()[0] == "UNSAT":
+            print("There is no solution")
+
+        elif line.split()[0] == "SAT":
+            pass
+
+        else:
+            assignment = [int(x) for x in line.split()]
+
+            for i in digits:
+                for j in digits:
+                    for k in digits:
+                        if varnum(i, j, k) in assignment:
+                            print(k, end="")
+                            break
+
+                print("")