Generating constraints as same as original encoding

diff --git a/killerSudoku/csolversudoku.py b/killerSudoku/csolversudoku.py
index cb603bed166c2d5e94969801a860ea72a0f5c55e..a333277b01a5de5a7df977da6a3d8d1400e670c8 100644 (file)
--- a/killerSudoku/csolversudoku.py
+++ b/killerSudoku/csolversudoku.py
@@ -27,10 +27,22 @@ def generateSumRange(domain1, domain2, totalSum):
                                range.add(d1+d2)
        return range
 
+def generateEqualityConstraint(csolverlb, solver, e1, e2):
+        equals = csolverlb.createPredicateOperator(solver, c_uint(ps.CompOp.SATC_EQUALS))
+        inp = [e1,e2]
+        inputs = (c_void_p*len(inp))(*inp)
+        b = csolverlb.applyPredicate(solver,equals, inputs, c_uint(2))
+        return b
+
 def generateKillerSudokuConstraints(N, killerRules, serialize):
        csolverlb = ps.loadCSolver()
        solver = csolverlb.createCCSolver()
-       problem = np.array([[None for i in range(N)] for i in range(N)])
+       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)])
+       
+       #problem = np.array([[None 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)]
        
        
@@ -48,7 +60,7 @@ def generateKillerSudokuConstraints(N, killerRules, serialize):
                                        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):
                cageSum = cage[0]
                cageSize = len(cage[1])
@@ -71,7 +83,7 @@ def generateKillerSudokuConstraints(N, killerRules, serialize):
                assert len(elements) >1
                parDomain = domain
                parElem = elements[0]
-               overflow = csolverlb.getBooleanVar(solver, c_uint(2));
+               overflow = csolverlb.getBooleanVar(solver, c_uint(1));
                for i in range(len(elements)):
                        if i< len(elements) -1: 
                                elem = elements[i+1]
@@ -98,13 +110,82 @@ def generateKillerSudokuConstraints(N, killerRules, serialize):
                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(1), c_long(sumCage))
-                       continue
-               elements, domain = getElement(cage)
-               generateSumConstraint(sumCage, elements, domain)        
+       #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(1), c_long(sumCage))
+       #               continue
+       #       elements, domain = getElement(cage)
+       #       generateSumConstraint(sumCage, elements, domain)        
+       
+       # find all possible combination of each cell
+       for k in killerRules:
+               cageSum = k[0]
+               cageSize = len(k[1])
+               cageCells = k[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))
+               #         print '\nall possible: ', allPossible
+               common = []
+               for i in range (1,N+1):
+                       flag = True # means it is a common one
+                       for j in allPossible:
+               #                 print 'test on', list(j)
+                               if not(i in list(j)):
+               #                     print i, ' is not in ', list(j)
+                                       flag = False
+                       if flag == True:
+               #                 print '************this is a common one: ', i
+                               common.append(i)
+
+               different = []
+               for p in allPossible:
+                       pl = list(p)
+                       for r in common:
+                               if r in pl:
+                                       pl.remove(r)
+                       if (pl != []):
+                               different.append(pl)
+               dic = {}
+               for num in range(1, N+1):
+                       dic[num] = csolverlb.getBooleanVar(solver, c_uint(1))
+                       tmp =[]
+                       for cc in cageCells:
+                               equal = generateEqualityConstraint(csolverlb, solver, problem[cc[0]][cc[1]], elemConsts[num-1])
+                               proxy = csolverlb.applyLogicalOperationTwo(solver, ps.LogicOps.SATC_IMPLIES, equal, dic[num]) 
+                               csolverlb.addConstraint(solver, proxy)
+                               tmp.append(equal)                # left arrow
+                       tmp.append(csolverlb.applyLogicalOperationOne(solver, ps.LogicOps.SATC_NOT,dic[num]))
+                       clause = (c_void_p*len(tmp))(*tmp)
+                       csolverlb.addConstraint(solver, csolverlb.applyLogicalOperation(solver, ps.LogicOps.SATC_OR,clause, c_uint(len(tmp))))
+               for num in common:
+               #             print num, '  is a common number'
+                       csolverlb.addConstraint(solver, dic[num])
+               x_list = []
+               for dif in different: # for example, [[3,4,8], [3,5,7], [4,5,6]
+                       # for cc in cageCells:
+                       # we need to convert from DNF to CNF
+                       # first, we need to convert that x1 = 3 /\ 4 /\ 8
+                       # again, we need to introduce our x1, for 348, x2 for 357 , etc
+                       x = csolverlb.getBooleanVar(solver, c_uint(1))
+                       # x -> 3 4 8
+                       for d in dif:
+                               csolverlb.addConstraint(solver, csolverlb.applyLogicalOperationTwo(solver, ps.LogicOps.SATC_IMPLIES, x, dic[d]))
+                       # print ' for ', d, ' -- ', dic[d]
+                       # ~(3, 4, 8) \/ x
+                       # i.e. -3 \/ -4 \/ -8 \/ x
+                       tmp = map ((lambda x : csolverlb.applyLogicalOperationOne(solver, ps.LogicOps.SATC_NOT, dic[x])), dif)
+                       tmp.append(x)
+                       # print ' == ', tmp
+                       clause = (c_void_p*len(tmp))(*tmp)
+                       csolverlb.addConstraint(solver, csolverlb.applyLogicalOperation(solver, ps.LogicOps.SATC_OR,clause, c_uint(len(tmp))))
+                       x_list.append(x)
+               if x_list != []:
+                       # print '***************', x_list
+                       clause = (c_void_p*len(x_list))(*x_list)
+                       csolverlb.addConstraint(solver, csolverlb.applyLogicalOperation(solver, ps.LogicOps.SATC_OR,clause, c_uint(len(x_list))))
        # Ensure there's no undefined element (for each cell we have a rule)
        validateElements(problem)
        # ensure each cell at least has one value!

diff --git a/killerSudoku/killerSolver.py b/killerSudoku/killerSolver.py
index c4775044ee5f4fa17e4b85d4c8f7ed769589f0b4..803ef2f182c0169d76a0216600d9fc1a33d3657e 100644 (file)
--- a/killerSudoku/killerSolver.py
+++ b/killerSudoku/killerSolver.py
@@ -343,4 +343,4 @@ def main ():
     
               
 if __name__ == '__main__':
-    main()
\ No newline at end of file
+    main()