From e60ed89eb50a70b4d05dff6d4c28264f03d4b0ef Mon Sep 17 00:00:00 2001
From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Tue, 9 Oct 2018 23:56:52 -0700
Subject: [PATCH] Generating constraints as same as original encoding
---
killerSudoku/csolversudoku.py | 101 ++++++++++++++++++++++++++++++----
killerSudoku/killerSolver.py | 2 +-
2 files changed, 92 insertions(+), 11 deletions(-)
diff --git a/killerSudoku/csolversudoku.py b/killerSudoku/csolversudoku.py
index cb603bed..a333277b 100644
--- 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 c4775044..803ef2f1 100644
--- 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()
--
2.34.1