From: Hamed Gorjiara Date: Wed, 10 Oct 2018 06:56:52 +0000 (-0700) Subject: Generating constraints as same as original encoding X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=e60ed89eb50a70b4d05dff6d4c28264f03d4b0ef;p=Benchmarks_CSolver.git Generating constraints as same as original encoding --- 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()