sudoku-csolver/csolversudoku.py

   1 import pycsolver as ps
   2 from ctypes import *
   3 import numpy as np
   4 import sys
   5
   6 def generateProblem(N):
   7         return generateSudokuConstraints(N)
   8
   9 def solveProblem(N, problem):
  10         return generateSudokuConstraints(N, problem)
  11
  12 def replaceWithElemConstOptimization(elemConsts, problem, sudoku):
  13         for i,row in enumerate(sudoku):
  14                 for j, cell in enumerate(row):
  15                         if cell != 0:
  16                                 problem[i][j] = elemConsts[cell-1]
  17
  18
  19
  20 def extractItemInSetOptimization(csolverlb, solver, sudoku, N):
  21         sets =[ [[i for i in range(1, N+1)] for i in range(N)] for i in range (N)]
  22         root = int(N**(0.5))
  23         for i, row in enumerate(sudoku):
  24                 for j, item in enumerate(row):
  25                         if item != 0:
  26                                 for k in range(N):
  27                                         if item in sets[i][k]:
  28                                                 sets[i][k].remove(item)
  29                                 for k in range(N):
  30                                         if item in sets[k][j]:
  31                                                 sets[k][j].remove(item)
  32                                 ii = (i/root)*root
  33                                 jj = (j/root)*root
  34                                 for k in range(N):
  35                                         if item in sets[ii +k% root][ jj + k//root]:
  36                                                 sets[ii +k% root][ jj + k//root].remove(item)
  37         for i in range(N):
  38                 for j in range(N):
  39                         setSize = len(sets[i][j])
  40                         setp = (c_long*setSize)(*sets[i][j])
  41                         sets[i][j] = csolverlb.createSet(solver, c_uint(1), setp, c_uint(setSize))
  42
  43         return np.array([[csolverlb.getElementVar(solver,sets[i][j]) for j in range(N)] for i in range(N)])
  44
  45 def generateSudokuConstraints(N, sudoku = None):
  46         csolverlb = ps.loadCSolver()
  47         solver = csolverlb.createCCSolver()
  48         s1 = [ i for i in range(1, N+1)]
  49         set1 = (c_long* len(s1))(*s1)
  50         s1 = csolverlb.createSet(solver, c_uint(1), set1, c_uint(N))
  51         problem = np.array([[csolverlb.getElementVar(solver,s1) for i in range(N)] for i in range(N)]) if sudoku is None else extractItemInSetOptimization(csolverlb, solver, sudoku, N)
  52         elemConsts = [csolverlb.getElementConst(solver, c_uint(1), i) for i in range(1, N+1)]
  53
  54         # Is it a sudoku to solve?
  55         if sudoku is not None:
  56                 replaceWithElemConstOptimization(elemConsts, problem, sudoku)
  57
  58         def valid(cells):
  59                 for i, ei in enumerate(cells):
  60                         for j, ej in enumerate(cells):
  61                                 if i < j:
  62                                         si = csolverlb.getElementRange(solver, ei)
  63                                         sj = csolverlb.getElementRange(solver,ej)
  64                                         d = [si,sj]
  65                                         domain = (c_void_p *len(d))(*d)
  66                                         equals = csolverlb.createPredicateOperator(solver, c_uint(ps.CompOp.SATC_EQUALS), domain, c_uint(2))
  67                                         inp = [ei,ej]
  68                                         inputs = (c_void_p*len(inp))(*inp)
  69                                         b = csolverlb.applyPredicate(solver,equals, inputs, c_uint(2))
  70                                         b = csolverlb.applyLogicalOperationOne(solver, ps.LogicOps.SATC_NOT, b)
  71                                         csolverlb.addConstraint(solver,b);
  72
  73
  74         # ensure each cell at least has one value!
  75         for i,row in enumerate(problem):
  76                 for j, elem in enumerate(row):
  77                         constr = []
  78                         for econst in elemConsts:
  79                                 s1 = csolverlb.getElementRange(solver, elem)
  80                                 sconst = csolverlb.getElementRange(solver,econst)
  81                                 d = [s1,sconst]
  82                                 domain = (c_void_p *len(d))(*d)
  83                                 equals = csolverlb.createPredicateOperator(solver, c_uint(ps.CompOp.SATC_EQUALS), domain, c_uint(2))
  84                                 inp = [elem,econst]
  85                                 inputs = (c_void_p*len(inp))(*inp)
  86                                 constr.append( csolverlb.applyPredicate(solver,equals, inputs, c_uint(2)))
  87                         b = (c_void_p*len(constr))(*constr)
  88                         b = csolverlb.applyLogicalOperation(solver, ps.LogicOps.SATC_OR, b, len(constr))
  89                         csolverlb.addConstraint(solver,b);
  90
  91
  92         #ensure each cell at least has one value
  93 #       for i,row in enumerate(problem):
  94 #               for j, elem in enumerate(row):
  95 #                       csolverlb.mustHaveValue(solver, elem)
  96
  97         # ensure rows and columns have distinct values
  98         for i in range( N):
  99                 valid(problem[:,i])
 100                 valid(problem[i,:])
 101
 102         # ensure each block has distinct values
 103         root = int(N**(0.5))
 104         collections = [ root*i for i in range(root)]
 105         for i in collections:
 106                 for j in collections:
 107                         valid([problem[i + k % root, j + k // root] for k in range(N)])
 108
 109         #Serializing the problem before solving it ....
 110         csolverlb.serialize(solver)
 111         if csolverlb.solve(solver) != 1:
 112                 print "Problem is unsolvable!"
 113                 sys.exit(1)
 114         result = [[0 for i in range(N)] for i in range(N)]
 115         for i,row in enumerate(problem):
 116                 for j, elem in enumerate(row):
 117                         result[i][j] = csolverlb.getElementValue(solver, elem)
 118         return result
 119