From af2365ea259dcf4d1c41831a1111b50bedc3375b Mon Sep 17 00:00:00 2001 From: Hamed Gorjiara Date: Fri, 3 Aug 2018 01:27:18 -0700 Subject: [PATCH] Csolver encoding is working fine for hard examples ... --- hexiom/csolverHexiom.py | 123 ++++++++++++++++++++++++---------------- 1 file changed, 74 insertions(+), 49 deletions(-) diff --git a/hexiom/csolverHexiom.py b/hexiom/csolverHexiom.py index 65390588..361d3e6b 100755 --- a/hexiom/csolverHexiom.py +++ b/hexiom/csolverHexiom.py @@ -8,13 +8,14 @@ from hexiom_config import * import pycsolver as ps from ctypes import * import os +from itertools import combinations ############################################ #### # Helper functions ### def getType(name): - types = ['O','Nps_', 'Ns_', 'Eps', 'Es', 'Tps_', 'Ts_', 'SimEq_'] + types = ['P', 'O','Nps_', 'Ns_', 'Eps', 'Es', 'Tps_', 'Ts_', 'SimEq_'] for (i,str) in enumerate(types): if name.startswith(str): return i @@ -121,11 +122,38 @@ class RuleSet(object): index = index + vsrev[i+1]*(base+1) assert index < self.size return index - + +# def valuesOfIndex(self, n): +# for i in range(self.multipliers[0]): +# index = n*self.multipliers[0] +i +# val = self.csolverlb.getBooleanValue(self.csolver, self.csvars[index]) +# if val == 1: +# return i; +# print("ERROR: invalid value for index") +# sys.exit(1) +# +# def printVariables(self): +# vars = [] +# index = 0 +# ruller = [i for i in range(self.multipliers[0]+1)] +# print ruller +# for i, var in enumerate(self.csvars): +# if i!=0 and i%self.multipliers[0] == 0: +# print str(index) + "=>" + str(vars) +# vars[:]=[] +# index = index + 1 +# vars.append(str(hex(self.csvars[i]))+"="+str(self.csolverlb.getBooleanValue( self.csolver, self.csvars[i]))) +# print str(index) + "=>" + str(vars) + def VarSet(self, name, csolverlb, csolver, dims): return RuleSet.VariableSet(self, name, csolverlb, csolver, dims) - - + + def printAllVariables(self): + for name in list(self.vsets_by_name.keys()): + varset = self.vsets_by_name[name] + print "*******************"+str(name)+"******************" + varset.printVariables() + def get_varset_by_name(self, name): return self.vsets_by_name.get(name) @@ -148,19 +176,17 @@ class And(CSConstraint): def __init__(self, csolverlb, csolver, cs): self.csolverlb = csolverlb self.csolver = csolver - cs = [con.getConstraint() for con in cs] - b = (c_void_p*len(cs))(*cs) - self.constr = self.csolverlb.applyLogicalOperation(self.csolver, ps.LogicOps.SATC_AND, b, c_uint(len(cs))) + constrs = [con.getConstraint() for con in cs] + b = (c_void_p*len(constrs))(*constrs) + self.constr = self.csolverlb.applyLogicalOperation(self.csolver, ps.LogicOps.SATC_AND, b, c_uint(len(constrs))) - - class Or(CSConstraint): def __init__(self, csolverlb, csolver, cs): self.csolverlb = csolverlb self.csolver = csolver - cs=[con.getConstraint() for con in cs] - b = (c_void_p*len(cs))(*cs) - self.constr = self.csolverlb.applyLogicalOperation(self.csolver, ps.LogicOps.SATC_OR, b, c_uint(len(cs))) + constrs=[con.getConstraint() for con in cs] + b = (c_void_p*len(constrs))(*constrs) + self.constr = self.csolverlb.applyLogicalOperation(self.csolver, ps.LogicOps.SATC_OR, b, c_uint(len(constrs))) def Implies(csolverlb, csolver,a,b): return Or(csolverlb, csolver,[-a, +b]) @@ -185,16 +211,16 @@ def sumOfVariables(csolverlb, csolver, S, T, variables, maxk): # T(k) = there are k truthy values n = len(variables) - + if(maxk is None): maxk = n - + rules = [] - + ## S - + for i in range(0, n+1): rules.append( S(0, i) ) - + for k in range(1, maxk+1): rules.append( -S(k, 0) ) for i in range(1, n+1): @@ -205,17 +231,16 @@ def sumOfVariables(csolverlb, csolver, S, T, variables, maxk): And(csolverlb, csolver,[ variables[i-1], S(k-1, i-1) ]) ]) )) - + ## T for k in range(0, maxk): rules.append(Equivalent(csolverlb, csolver, T(k), And(csolverlb, csolver,[S(k, n), -S(k+1, n)]) )) - + rules.append(Equivalent(csolverlb, csolver, T(maxk), S(maxk,n) )) - return And(csolverlb, csolver,rules) def vectorLessThenOrEqual(csolverlb, csolver, E, xs, ys): @@ -505,33 +530,33 @@ def read_input(fil): def generateElements(csolverlb, csolver, slot_range, value_range): elems = [] for slot in range(slot_range[0], slot_range[-1]+1): - s1 = [ i for i in range(value_range[0],value_range[-1]+2)] + s1 = [ i for i in range(value_range[0],value_range[-1]+1)] set1 = (c_long* len(s1))(*s1) s1 = csolverlb.createSet(csolver, c_uint(11), set1, c_uint(len(s1))) e1 = csolverlb.getElementVar(csolver,s1) - csolverlb.mustHaveValue(csolver, e1) +# csolverlb.mustHaveValue(csolver, e1) elems.append(e1) return elems def Placement(csolverlb, csolver, elems, m, n): e1 = elems[m] - e2 = csolverlb.getElementConst(csolver, c_uint(12), n+1) + e2 = csolverlb.getElementConst(csolver, c_uint(12), n) equals = csolverlb.createPredicateOperator(csolver, c_uint(ps.CompOp.SATC_EQUALS)) inp = [e1,e2] inputs = (c_void_p*len(inp))(*inp) b= csolverlb.applyPredicate(csolver,equals, inputs, c_uint(2)) return CSConstraint(csolverlb, csolver, b) -def Occupied(csolverlb, csolver, elems, m): - e1 = elems[m] - e2 = csolverlb.getElementConst(csolver, c_uint(12), 0) - equals = csolverlb.createPredicateOperator(csolver, c_uint(ps.CompOp.SATC_EQUALS)) - inp = [e1,e2] - inputs = (c_void_p*len(inp))(*inp) - b= csolverlb.applyPredicate(csolver,equals, inputs, c_uint(2)) - return CSConstraint(csolverlb, csolver, b) +# def Occupied(csolverlb, csolver, elems, m): +# e1 = elems[m] +# e2 = csolverlb.getElementConst(csolver, c_uint(12), 7) +# equals = csolverlb.createPredicateOperator(csolver, c_uint(ps.CompOp.SATC_EQUALS)) +# inp = [e1,e2] +# inputs = (c_void_p*len(inp))(*inp) +# b= csolverlb.applyPredicate(csolver,equals, inputs, c_uint(2)) +# return CSConstraint(csolverlb, csolver, b) -def replaceWithElemConst(csolver, solver, elems, m, n): +def replaceWithElemConst(csolverlb, solver, elems, m, n): elems[m] = csolverlb.getElementConst(solver, c_uint(10), n) #### # Create clauses @@ -558,10 +583,10 @@ def SAT_formulation_from_board_input(board_input, csolverlb, csolver): # (m,n) = There is an n-valued tile at slot m # The m-th slot has n occupied neighbors -# Placement = ruleset.VarSet('P', [slot_range, value_range]) +# Placement = ruleset.VarSet('P', csolverlb, csolver, [slot_range, value_range]) elems = generateElements(csolverlb, csolver, slot_range, value_range) # (m) = is the m-th tile occupied? -# Occupied = ruleset.VarSet('O', csolverlb, csolver, [slot_range]) + Occupied = ruleset.VarSet('O', csolverlb, csolver, [slot_range]) # (m)(k,i) = m-th slot has k occupied slots among its first i neighbours NeighbourPartialSum = [] @@ -584,13 +609,13 @@ def SAT_formulation_from_board_input(board_input, csolverlb, csolver): replaceWithElemConst(csolverlb, csolver, elems, m, n) for m in board_input.blocked_positions: - csolverlb.addConstraint(csolver, (-Occupied(csolverlb, csolver, elems, m)).getConstraint() ) + csolverlb.addConstraint(csolver, (-Occupied(m)).getConstraint() ) print 'Creating tile placement rules...' rules =[] for m in topology.ps: csolverlb.addConstraint(csolver, BruteForceOnlyOne(csolverlb, csolver, - [-Occupied(csolverlb, csolver, elems, m)] + [+Placement(csolverlb, csolver, elems,m,n) for n in range(7)] + [-Occupied(m)] + [+Placement(csolverlb, csolver, elems,m,n) for n in range(7)] ).getConstraint()) adj_graph = topology.pos_adjacency_graph() @@ -611,20 +636,20 @@ def SAT_formulation_from_board_input(board_input, csolverlb, csolver): csolverlb.addConstraint(csolver, sumOfVariables(csolverlb, csolver, NPSum, NSum, - [+Occupied(csolverlb, csolver, elems, v) for v in adj_graph[m]], + [+Occupied(v) for v in adj_graph[m]], None ).getConstraint()) for n in range(0, nvs+1): csolverlb.addConstraint(csolver, Implies(csolverlb, csolver, - Occupied(csolverlb, csolver, elems, m), + Occupied(m), Equivalent(csolverlb, csolver, +Placement(csolverlb, csolver, elems,m,n), +NSum(n) ) ).getConstraint()) for n in range(nvs+1, 7): csolverlb.addConstraint(csolver, (-Placement(csolverlb, csolver, elems,m,n)).getConstraint() ) - print 'Creating constraints for the amount of tiles used...' + print 'Creating constraints for the number of empty cell...' empty_count = len(topology.ps) - sum([c for (_,c) in board_input.counts]) @@ -638,10 +663,10 @@ def SAT_formulation_from_board_input(board_input, csolverlb, csolver): csolverlb.addConstraint(csolver, sumOfVariables(csolverlb, csolver, EmptyPartialSum, EmptySum, - [ -Occupied(csolverlb, csolver, elems, m) for m in topology.ps ], + [ -Occupied(m) for m in topology.ps ], empty_count + 1 ).getConstraint()) - + print 'Creating constraints for the amount of tiles used...' for n in range(0, 7): tile_count = assoc_get(n, board_input.counts) @@ -680,7 +705,7 @@ def SAT_formulation_from_board_input(board_input, csolverlb, csolver): def vars_from_sim(ms): vs = [] for m in ms: - vs.append( +Occupied(csolverlb, csolver, elems, m) ) + vs.append( +Occupied(m) ) vs.extend([ +Placement(csolverlb, csolver, elems,m,n) for n in range(0, 7) ]) return vs @@ -714,11 +739,12 @@ def print_board_from_assignments(csolverlb, csolver, formulation): elems = formulation.elems layout = [None for p in topology.ps] - - for i, e in enumerate(elems): - elem= csolverlb.getElementValue(csolver, e) - if elem != 0: - layout[i]= elem + O = ruleset.get_varset_by_name('O') + + for i, var in enumerate(O.csvars): + val = csolverlb.getBooleanValue(csolver, var) + if val == 1: + layout[i] = csolverlb.getElementValue(csolver, elems[i]) print '=== Initial input: ===' formulation.board_input.print_to_stdout() @@ -753,8 +779,7 @@ def main(): formulation = SAT_formulation_from_board_input(board_input, csolverlb, csolver) print '=== Done! Calling CSolver solver now ===' -# csolverlb.serialize(csolver) - csolverlb.printConstraints(csolver) +# csolverlb.printConstraints(csolver) if csolverlb.solve(csolver) != 1: print '*** Got UNSAT result! ***' sys.exit(1) -- 2.34.1