killerSudoku/csolversudoku.py

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