From efa5110e0b19cc26190b60ef1329c13c8ed0d1a6 Mon Sep 17 00:00:00 2001 From: Hamed Gorjiara Date: Wed, 1 Aug 2018 01:01:17 -0700 Subject: [PATCH] Making occupation constraint part of the element --- hexiom/csolverHexiom.py | 42 ++++++++++++++++++++++------------------- 1 file changed, 23 insertions(+), 19 deletions(-) diff --git a/hexiom/csolverHexiom.py b/hexiom/csolverHexiom.py index 1b1fad69..65390588 100755 --- a/hexiom/csolverHexiom.py +++ b/hexiom/csolverHexiom.py @@ -73,7 +73,6 @@ class RuleSet(object): self.vsets_by_name = {} self.csolver = csolver self.csolverlb= csolverlb - self.next_free_variable = 1 class VariableSet(object): def __init__(self, ruleset, name, csolverlb, csolver, dims): @@ -93,9 +92,6 @@ class RuleSet(object): raise Exception('repeated name %s'%name) ruleset.vsets_by_name[name] = self - self.first_variable = self.ruleset.next_free_variable - self.ruleset.next_free_variable += self.size - self.csvars = [csolverlb.getBooleanVar(csolver, c_uint(getType(name))) for i in range(self.size)] self.csolverlb = csolverlb self.csolver = csolver @@ -509,17 +505,26 @@ 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]+1)] + s1 = [ i for i in range(value_range[0],value_range[-1]+2)] 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) + e2 = csolverlb.getElementConst(csolver, c_uint(12), n+1) + 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) @@ -556,7 +561,7 @@ def SAT_formulation_from_board_input(board_input, csolverlb, csolver): # Placement = ruleset.VarSet('P', [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 = [] @@ -579,13 +584,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(m)).getConstraint() ) + csolverlb.addConstraint(csolver, (-Occupied(csolverlb, csolver, elems, m)).getConstraint() ) print 'Creating tile placement rules...' rules =[] for m in topology.ps: csolverlb.addConstraint(csolver, BruteForceOnlyOne(csolverlb, csolver, - [-Occupied(m)] + [+Placement(csolverlb, csolver, elems,m,n) for n in range(7)] + [-Occupied(csolverlb, csolver, elems, m)] + [+Placement(csolverlb, csolver, elems,m,n) for n in range(7)] ).getConstraint()) adj_graph = topology.pos_adjacency_graph() @@ -606,13 +611,13 @@ def SAT_formulation_from_board_input(board_input, csolverlb, csolver): csolverlb.addConstraint(csolver, sumOfVariables(csolverlb, csolver, NPSum, NSum, - [+Occupied(v) for v in adj_graph[m]], + [+Occupied(csolverlb, csolver, elems, v) for v in adj_graph[m]], None ).getConstraint()) for n in range(0, nvs+1): csolverlb.addConstraint(csolver, Implies(csolverlb, csolver, - Occupied(m), + Occupied(csolverlb, csolver, elems, m), Equivalent(csolverlb, csolver, +Placement(csolverlb, csolver, elems,m,n), +NSum(n) ) ).getConstraint()) @@ -633,7 +638,7 @@ def SAT_formulation_from_board_input(board_input, csolverlb, csolver): csolverlb.addConstraint(csolver, sumOfVariables(csolverlb, csolver, EmptyPartialSum, EmptySum, - [ -Occupied(m) for m in topology.ps ], + [ -Occupied(csolverlb, csolver, elems, m) for m in topology.ps ], empty_count + 1 ).getConstraint()) @@ -675,7 +680,7 @@ def SAT_formulation_from_board_input(board_input, csolverlb, csolver): def vars_from_sim(ms): vs = [] for m in ms: - vs.append( +Occupied(m) ) + vs.append( +Occupied(csolverlb, csolver, elems, m) ) vs.extend([ +Placement(csolverlb, csolver, elems,m,n) for n in range(0, 7) ]) return vs @@ -707,14 +712,13 @@ def print_board_from_assignments(csolverlb, csolver, formulation): ruleset = formulation.ruleset topology = formulation.topology elems = formulation.elems - O = ruleset.get_varset_by_name('O') layout = [None for p in topology.ps] - for i, bool in enumerate(O.csvars): - if csolverlb.getBooleanValue(csolver, bool): - e = elems[i] - layout[i]= csolverlb.getElementValue(csolver, e) + for i, e in enumerate(elems): + elem= csolverlb.getElementValue(csolver, e) + if elem != 0: + layout[i]= elem print '=== Initial input: ===' formulation.board_input.print_to_stdout() -- 2.34.1