Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/Benchmarks_CSolver

diff --cc killerSudoku/csolversudoku.py
index 0000000000000000000000000000000000000000,b3eb63c8e0fc8a8b7bfeff2606972bff5c222ed8..d6a169c685c1eacf9d973562590606d57e87ca70
mode 000000,100644..100644
--- /dev/null
--- 2/killerSudoku/csolversudoku.py
+++ b/killerSudoku/csolversudoku.py
@@@ -1,0 -1,125 +1,116 @@@
 -              cageSum = cage[0]
 -              cageSize = len(cage[1])
 -              cageCells = cage[1]
 -              cb = combinations([ii for ii in range(1, N+1)], cageSize)
 -              f = lambda x : sum(x) == cageSum
 -              comb = ifilter(f, cb) # all valid combinations
 -              allPossible = list(chain(comb))
 -              #s1 = [ allPossible[ i for i in range(1, N+1)]]
 -              set1 = (c_long* len(s1))(*s1)
 -              s1 = csolverlb.createSet(solver, c_uint(1), set1, c_uint(N))
 -              problem = np.array([[csolverlb.getElementVar(solver,s1) for i in range(N)] for i in range(N)])
 -              elements = [ problem[cage[1][i][0]][cage[1][i][1]] for i in range(len(cage[1])) ]
+ import pycsolver as ps
+ from ctypes import *
+ import numpy as np
+ import sys
+ from itertools import combinations, ifilter, chain
+ 
+ def solveProblem(N, killerRules):
+       
+       return generateKillerSudokuConstraints(N, killerRules)
+ 
+ 
+ def generateKillerSudokuConstraints(N, killerRules):
+       csolverlb = ps.loadCSolver()
+       solver = csolverlb.createCCSolver()
+       s1 = [ i for i in range(1, N+1)]
+       set1 = (c_long* len(s1))(*s1)
+       s1 = csolverlb.createSet(solver, c_uint(1), set1, c_uint(N))
+       problem = np.array([[csolverlb.getElementVar(solver,s1) for i in range(N)] for i in range(N)])
+       elemConsts = [csolverlb.getElementConst(solver, c_uint(1), i) for i in range(1, N+1)]
+       
+       
+       def valid(cells):
+               for i, ei in enumerate(cells):
+                       for j, ej in enumerate(cells):
+                               if i < j:
+                                       si = csolverlb.getElementRange(solver, ei)
+                                       sj = csolverlb.getElementRange(solver,ej)
+                                       d = [si,sj]
+                                       domain = (c_void_p *len(d))(*d)
+                                       equals = csolverlb.createPredicateOperator(solver, c_uint(ps.CompOp.SATC_EQUALS), domain, c_uint(2))
+                                       inp = [ei,ej]
+                                       inputs = (c_void_p*len(inp))(*inp)
+                                       b = csolverlb.applyPredicate(solver,equals, inputs, c_uint(2))
+                                       b = csolverlb.applyLogicalOperationOne(solver, ps.LogicOps.SATC_NOT, b)
+                                       csolverlb.addConstraint(solver,b);
+               
+       def getElement(cage):
 -                      valid(problem[:,i])
 -      valid(problem[i,:])
++              elems = [ problem[cage[1][i][0]][cage[1][i][1]] for i in range(len(cage[1])) ]
++              valid(elems)
++              return elems
+       
+       def generateSumConstraint(sumCage, elements):
+               d = []
+               for e in elements:
+                       d.append(csolverlb.getElementRange(solver, e))
+               domains = (c_void_p *len(d))(*d)
+               overflow = csolverlb.getBooleanVar(solver, c_uint(2));
+               esum = csolverlb.getElementConst(solver, c_uint(3), c_long(sumCage))
+               setSum = csolverlb.getElementRange(solver, esum)
+               f1 = csolverlb.createFunctionOperator(solver, ps.ArithOp.SATC_ADD, domains, c_uint(len(d)), setSum, ps.OverFlowBehavior.SATC_OVERFLOWSETSFLAG);
+               inputs = (c_void_p*len(elements))(*elements)
+               added = csolverlb.applyFunction(solver, f1, inputs, len(elements), overflow);
+               
+               d = [setSum,setSum]
+               domain = (c_void_p *len(d))(*d)
+               equals = csolverlb.createPredicateOperator(solver, c_uint(ps.CompOp.SATC_EQUALS), domain, c_uint(len(d)))
+               inp = [added,esum]
+               inputs = (c_void_p*len(inp))(*inp)
+               b = csolverlb.applyPredicate(solver,equals, inputs, c_uint(len(inp)))
+               csolverlb.addConstraint(solver,b);
+               csolverlb.addConstraint(solver, csolverlb.applyLogicalOperationOne(solver, ps.LogicOps.SATC_NOT, overflow));
+       
+       # Generating constraints for each cage
+       for cage in killerRules:
+               sumCage = cage[0]
+               if len(cage[1])==1:
+                       problem[cage[1][0][0]][cage[1][0][1]] = csolverlb.getElementConst(solver, c_uint(7), c_long(sumCage))
+                       continue
+               elements = getElement(cage)
+               generateSumConstraint(sumCage, elements)        
+               
+       # ensure each cell at least has one value!
+       for i,row in enumerate(problem):
+               for j, elem in enumerate(row):
+                       constr = []
+                       for econst in elemConsts:
+                               s1 = csolverlb.getElementRange(solver, elem)
+                               sconst = csolverlb.getElementRange(solver,econst)
+                               d = [s1,sconst]
+                               domain = (c_void_p *len(d))(*d)
+                               equals = csolverlb.createPredicateOperator(solver, c_uint(ps.CompOp.SATC_EQUALS), domain, c_uint(2))
+                               inp = [elem,econst]
+                               inputs = (c_void_p*len(inp))(*inp)
+                               constr.append( csolverlb.applyPredicate(solver,equals, inputs, c_uint(2)))
+                       b = (c_void_p*len(constr))(*constr)
+                       b = csolverlb.applyLogicalOperation(solver, ps.LogicOps.SATC_OR, b, len(constr))
+                       csolverlb.addConstraint(solver,b);
+       
+       
+       #ensure each cell at least has one value
+ #     for i,row in enumerate(problem):
+ #             for j, elem in enumerate(row):
+ #                     csolverlb.mustHaveValue(solver, elem)
+ 
+       # ensure rows and columns have distinct values
+       for i in range( N):
 -        collections = [ root*i for i in range(root)]
 -        for i in collections:
 -                for j in collections:
 -                        valid([problem[i + k % root, j + k // root] for k in range(N)])
++              valid(problem[:,i])
++              valid(problem[i,:])
+       
+       # ensure each block has distinct values
+       root = int(N**(0.5))
++      collections = [ root*i for i in range(root)]
++      for i in collections:
++              for j in collections:
++                      valid([problem[i + k % root, j + k // root] for k in range(N)])
+       
+       #Serializing the problem before solving it ....
+       csolverlb.serialize(solver)
+       if csolverlb.solve(solver) != 1:
+               return None
+       result = [[0 for i in range(N)] for i in range(N)]
+       for i,row in enumerate(problem):
+               for j, elem in enumerate(row):
+                       result[i][j] = csolverlb.getElementValue(solver, elem)
+       return result
+