From: Hamed Gorjiara Date: Thu, 19 Jul 2018 22:17:27 +0000 (-0700) Subject: Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/Benchmarks_CSolver X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=0f32382b6e682daffd9fb61902a0b60516f055f9;p=Benchmarks_CSolver.git Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/Benchmarks_CSolver --- 0f32382b6e682daffd9fb61902a0b60516f055f9 diff --cc killerSudoku/csolversudoku.py index 00000000,b3eb63c8..d6a169c6 mode 000000,100644..100644 --- a/killerSudoku/csolversudoku.py +++ b/killerSudoku/csolversudoku.py @@@ -1,0 -1,125 +1,116 @@@ + 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): - 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])) ] ++ 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): - valid(problem[:,i]) - valid(problem[i,:]) ++ 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)]) ++ 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 +