--- /dev/null
+*.pyc
+
+.project
+.pydevproject
+.settings/
+
+
+sat_in/*
+sat_out/*
+scratch/*
--- /dev/null
+#! /bin/sh
+rm ./*.pyc
+rm ./sat_in/*.cnf
+rm ./sat_out/*.txt
+rm ./scratch/*.txt
--- /dev/null
+../../bin/
\ No newline at end of file
--- /dev/null
+#! /usr/bin/python
+# - * - coding:utf-8 - * -
+
+############################################
+# CONFIGURATION
+############################################
+from hexiom_config import *
+import pycsolver as ps
+from ctypes import *
+import os
+############################################
+
+####
+# Helper functions
+###
+def getType(name):
+ types = ['O','Nps_', 'Ns_', 'Eps', 'Es', 'Tps_', 'Ts_', 'SimEq_']
+ for (i,str) in enumerate(types):
+ if name.startswith(str):
+ return i
+ print "Undefined type: " + name
+ os.abort()
+
+def enumerate1(xs):
+ ''' (x1,x2...) -> ((1,x1), (2,x2),...) '''
+ for (i,x) in enumerate(xs):
+ yield (i+1, x)
+
+def assoc_list(xs):
+ return list(enumerate(xs))
+
+def assoc_get(x, xs):
+ for (k,v) in xs:
+ if k == x:
+ return v
+ return None
+
+##
+# Building rules
+#
+
+def size_of_dims(dims):
+ s = 1
+ for (minv, maxv) in dims:
+ if minv <= maxv:
+ s *= (maxv - minv + 1)
+ else:
+ s *= 0
+ return s
+
+def dim_multipliers(dims):
+ ''' mult[i] = size_of(dims[i+1:])'''
+
+ multipliers = [None] * len(dims)
+ multipliers[-1] = 1
+
+ for i in range(len(dims)-2, -1, -1):
+ (minv, maxv) = dims[i+1]
+ multipliers[i] = \
+ multipliers[i+1] * \
+ (maxv - minv + 1)
+
+ return multipliers
+
+class InvalidVariable(Exception):
+ pass
+
+
+class RuleSet(object):
+
+ def __init__(self, csolverlb, csolver):
+ self.vsets = []
+ 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):
+ self.name = name
+
+ self.ndims = len(dims)
+ self.dims = dims
+
+ self.size = size_of_dims(dims)
+
+ self.multipliers = dim_multipliers(dims)
+
+ self.ruleset = ruleset
+ ruleset.vsets.append(self)
+
+ if ruleset.vsets_by_name.get(name):
+ 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
+
+ def __call__(self, *vs):
+ if self.ndims != len(vs):
+ raise InvalidVariable(
+ 'Expected %d dimensions, got %d'%(
+ self.ndims, len(vs))
+ )
+
+ for (val, (min_val, max_val)) in zip(vs, self.dims):
+ if not (min_val <= val <= max_val):
+ raise InvalidVariable(
+ 'Variable out of bounds:', self.name, vs, self.dims
+ )
+
+ return CSConstraint(self.csolverlb, self.csolver, self.csvars[self.varIndex(vs)])
+
+ def varIndex(self, vs):
+ assert len(vs) == len(self.dims) and len(vs) > 0
+ index = 0
+ vsrev = vs[::-1]
+ index = index + vsrev[0]
+ for i, (begin,base) in enumerate(self.dims[::-1]):
+ if i != len(self.dims)-1:
+ index = index + vsrev[i+1]*(base+1)
+ assert index < self.size
+ return index
+
+ def VarSet(self, name, csolverlb, csolver, dims):
+ return RuleSet.VariableSet(self, name, csolverlb, csolver, dims)
+
+
+ def get_varset_by_name(self, name):
+ return self.vsets_by_name.get(name)
+
+class CSConstraint(object):
+ def __init__(self, csolverlb, csolver, cs):
+ self.csolverlb = csolverlb
+ self.csolver = csolver
+ self.constr = cs
+
+ def __pos__(self):
+ return self
+
+ def __neg__(self):
+ return CSConstraint(self.csolverlb, self.csolver, self.csolverlb.applyLogicalOperationOne(self.csolver, ps.LogicOps.SATC_NOT, self.constr))
+
+ def getConstraint(self):
+ return self.constr
+
+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)))
+
+
+
+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)))
+
+def Implies(csolverlb, csolver,a,b):
+ return Or(csolverlb, csolver,[-a, +b])
+
+def Equivalent(csolverlb, csolver,a,b):
+ return And(csolverlb, csolver,[
+ Implies(csolverlb, csolver,a,b),
+ Implies(csolverlb, csolver,b,a)
+ ])
+
+def BruteForceOnlyOne(csolverlb, csolver,xs):
+ rs = [Or(csolverlb, csolver,xs)]
+ for (i,a) in enumerate(xs):
+ for (j,b) in enumerate(xs):
+ if (i != j):
+ rs.append( Implies(csolverlb, csolver,a, -b) )
+ return And(csolverlb, csolver,rs)
+
+def sumOfVariables(csolverlb, csolver, S, T, variables, maxk):
+ # S(k, i) = there are at leat k truthy values
+ # among the first i variables
+ # 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):
+ rules.append(Equivalent(csolverlb, csolver,
+ S(k, i),
+ Or(csolverlb, csolver,[
+ S(k, i-1),
+ 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):
+ # n = len(xs) = len(ys)
+ # E_i, i in [0,n] := xs[0:i] == ys[0:i]
+
+ n = len(xs)
+
+ if(len(ys) != n):
+ raise Exception('Imcompatible vector lengths')
+
+ rules = []
+
+ ## Eq
+ rules.append( +E(0) )
+ for (i, (x, y)) in enumerate1(zip(xs, ys)):
+ rules.append(Equivalent(csolverlb, csolver,
+ E(i),
+ And(csolverlb, csolver,[ E(i-1), Equivalent(csolverlb, csolver,x, y) ])
+ ))
+
+ ## x < y
+ for i in range(0,n):
+ rules.append(
+ Implies(csolverlb, csolver, E(i), Implies(csolverlb, csolver,xs[i], ys[i]) )
+ )
+
+ return +And(csolverlb, csolver,rules)
+
+###########
+# Neighbours
+###########
+
+# Radial Hexagonal coordinates
+# (r, c, d)
+# r = distance from center
+# c = vértice associado
+# d = indice no lado (0 é o vértice, r-1 é o último)
+#
+# |0__ |1
+# / \
+# 5 --
+# -- 2
+# \ /
+# 4| __3|
+
+#Directional Hexagonal coordinates
+# (a,b)
+# / a
+# - b
+#
+# (-1,-1) (-1, 0)
+# ( 0,-1) ( 0, 0) ( 0, 1)
+# ( 1, 0) (1, 1)
+
+# Positional coordinates, as they come
+# from the input:
+#
+# 0 1
+# 2 3 4
+# 5 6
+
+#Simmetry functions
+
+def reflect_0_5((r, c, d)):
+ if r == 0 and c == 0 and d == 0:
+ return (0,0,0)
+ else:
+ if d == 0:
+ return (r, 5-c, 0)
+ else:
+ return (r, (10-c)%6, r-d)
+
+def clockwise_rotate(n, (r,c,d)):
+ if r == 0 and c == 0 and d == 0:
+ return (0,0,0)
+ else:
+ return (r, (c+n)%6, d)
+
+class HexTopology(object):
+ def __init__(self, side):
+ self.rcd_to_m = {}
+ self.ab_to_m = {}
+
+ self.side = side
+
+ self.rcds = []
+ self.abs = []
+ self.ps = []
+
+ m_ = [0]
+ a_ = [None]
+ b_ = [None]
+ def match(rcd):
+ m = m_[0]
+ ab = (a_[0], b_[0])
+
+ self.abs.append(ab)
+ self.rcds.append(rcd)
+ self.ps.append(m)
+
+ self.rcd_to_m[rcd] = m
+ self.ab_to_m[ab] = m
+
+ m_[0] += 1
+ b_[0] += 1
+ #print ''.join(map(str,rcd)),
+
+ radius = side-1
+
+ #top half
+ for r in range(radius, 0, -1):
+ a_[0] = -r
+ b_[0] = -radius
+ #print ' '*r,
+ for i in range(0, radius-r):
+ match((radius-i, 5, r))
+ for i in range(r):
+ match((r, 0, i))
+ for i in range(0, radius+1-r):
+ match((r+i, 1, i))
+ #print
+
+ #middle divider
+ a_[0] = 0
+ b_[0] = -radius
+ #print '',
+ for r in range(radius, 0, -1):
+ match((r, 5, 0))
+ if(radius >= 0):
+ match((0,0,0))
+ for r in range(1, radius+1):
+ match((r, 2, 0))
+ #iprint
+
+ #lower half
+ for r in range(1, radius+1):
+ a_[0] = r
+ b_[0] = -(radius-r)
+ #print ' '*r,
+ for i in range(0, radius+1-r):
+ match((radius-i, 4, radius-r-i))
+ for i in range(r):
+ match((r, 3, r-i-1))
+ for i in range(0, radius-r):
+ match((r+1+i, 2, r))
+ #print
+
+ def print_in_hex(self, xs):
+ xs = list(reversed(xs))
+ side = self.side
+ lines = []
+
+ def show(n):
+ return ('.' if n is None else str(n))
+
+ #upper half (with middle line)
+ for (i,a) in enumerate(range(1-side, 0+1)):
+ line = []
+ for b in range(1-side, i+1):
+ line.append(show(xs.pop()))
+ lines.append( ' '*(side-i-1) + ' '.join(line) )
+ #lower half (without middle line)
+ for (i,a) in enumerate1(range(1, side)):
+ line = []
+ for b in range(1-side+i, side):
+ line.append(show(xs.pop()))
+ lines.append( ' '*i + ' '.join(line) )
+ return '\n'.join(lines)
+
+ def hex_adjacency_graph(self):
+ adj_list = {}
+
+ def add(m, n):
+ adj_list[m].append(n)
+
+ def is_adj(m,n):
+ add(m, n)
+ if not adj_list.has_key(n):
+ adj_list[n] = []
+ add(n, m)
+
+ for h in self.abs:
+ (a,b) = h
+
+ if not adj_list.has_key(h):
+ adj_list[h] = []
+
+ for h_ in [
+ (a-1, b-1), (a-1, b),
+ (a, b+1)
+ ]:
+ if self.ab_to_m.get(h_) is not None:
+ is_adj(h, h_)
+
+ for lst in adj_list.values():
+ lst.sort()
+
+ return adj_list
+
+ def pos_adjacency_graph(self):
+ adj_list = {}
+
+ for (k, vs) in self.hex_adjacency_graph().iteritems():
+ adj_list[ self.ab_to_m[k] ] =\
+ [ self.ab_to_m[v] for v in vs]
+
+ return adj_list
+
+ def simmetries(self):
+ simmetries = []
+
+ def add_sim(rcds):
+ simmetries.append([
+ self.rcd_to_m[rcd]
+ for rcd in rcds
+ ])
+
+ for n in range(6):
+ add_sim([
+ clockwise_rotate(n, rcd)
+ for rcd in self.rcds
+ ])
+
+ for n in range(6):
+ add_sim([
+ reflect_0_5(clockwise_rotate(n, rcd))
+ for rcd in self.rcds
+ ])
+
+ return simmetries
+
+###########
+# Input
+###########
+
+import re
+
+class ProblemInput(object):
+ def __init__(self, side, counts, blocked_positions, fixed_positions, lines):
+ self.side = side
+ self.counts = counts
+ self.blocked_positions = blocked_positions
+ self.fixed_positions = fixed_positions
+ self.lines = lines
+
+ def print_to_stdout(self):
+ print self.side
+ for line in self.lines:
+ print line,
+
+def read_input(fil):
+ side = int(fil.readline())
+ counts = [0]*7
+ blocked_positions = []
+ fixed_positions = []
+
+ lines = []
+
+ m=0
+ for line in fil:
+ lines.append(line)
+ for match in re.finditer(r'(\+?)(\.|\d)', line):
+ locked = (match.group(1) == '+')
+ n = (None if match.group(2) == '.' else int(match.group(2)))
+
+ if n is not None:
+ counts[n] += 1
+
+ if locked:
+ if n is None:
+ blocked_positions.append(m)
+ else:
+ fixed_positions.append( (m, n) )
+
+ m += 1
+
+ return ProblemInput(
+ side,
+ assoc_list(counts),
+ blocked_positions,
+ fixed_positions,
+ lines
+ )
+
+
+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)]
+ 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)
+ elems.append(e1)
+ return elems
+
+def Placement(csolverlb, csolver, elems, m, n):
+ e1 = elems[m]
+ 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 replaceWithElemConst(csolver, solver, elems, m, n):
+ elems[m] = csolverlb.getElementConst(solver, c_uint(10), n)
+####
+# Create clauses
+####
+
+class SATFormulation(object):
+ def __init__(self, board_input, ruleset, topology, elems):
+ self.board_input = board_input
+ self.ruleset = ruleset
+ self.topology = topology
+ self.elems = elems
+
+def SAT_formulation_from_board_input(board_input, csolverlb, csolver):
+ ruleset = RuleSet(csolverlb, csolver)
+ topology = HexTopology(board_input.side)
+
+ # Schema
+ ########
+
+ slot_range = (0, topology.ps[-1])
+ slot_count = len(topology.ps)
+
+ value_range = (0, 6)
+
+ # (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])
+ elems = generateElements(csolverlb, csolver, slot_range, value_range)
+ # (m) = is the m-th tile occupied?
+ Occupied = ruleset.VarSet('O', csolverlb, csolver, [slot_range])
+
+ # (m)(k,i) = m-th slot has k occupied slots among its first i neighbours
+ NeighbourPartialSum = []
+
+ # (m)(k) = m-th slot has k occupied slots among its neighbours
+ NeighbourSum = []
+
+
+ # (n)(k,i) = there are k n-valued tiles on the first i slots?
+ TilePartialSum = []
+
+ # Rules
+ #######
+
+ print '== Creating CNF description of level'
+
+ print 'Creating level-state rules...'
+
+ for (m, n) in board_input.fixed_positions:
+ replaceWithElemConst(csolverlb, csolver, elems, m, n)
+
+ for m in board_input.blocked_positions:
+ csolverlb.addConstraint(csolver, (-Occupied(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)]
+ ).getConstraint())
+
+ adj_graph = topology.pos_adjacency_graph()
+
+ print 'Constraining number of neighbour of occupied tiles...'
+
+ for m in topology.ps:
+ vs = adj_graph[m]
+ nvs = len(vs)
+
+ NPSum = ruleset.VarSet('Nps_'+str(m),csolverlb, csolver, [
+ (0, nvs), (0, nvs) ])
+ NeighbourPartialSum.append(NPSum)
+
+ NSum = ruleset.VarSet('Ns_'+str(m), csolverlb, csolver,[
+ (0, nvs) ])
+ NeighbourSum.append(NSum)
+
+ csolverlb.addConstraint(csolver, sumOfVariables(csolverlb, csolver,
+ NPSum, NSum,
+ [+Occupied(v) for v in adj_graph[m]],
+ None
+ ).getConstraint())
+
+ for n in range(0, nvs+1):
+ csolverlb.addConstraint(csolver, Implies(csolverlb, csolver,
+ 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...'
+
+ empty_count = len(topology.ps) - sum([c for (_,c) in board_input.counts])
+
+ # (k,i) = k empty slots among the first i slots
+ EmptyPartialSum = ruleset.VarSet('Eps', csolverlb, csolver, [
+ (0, empty_count+1), (0, slot_count) ])
+
+ EmptySum = ruleset.VarSet('Es', csolverlb, csolver, [
+ (0, empty_count+1)
+ ])
+
+ csolverlb.addConstraint(csolver, sumOfVariables(csolverlb, csolver,
+ EmptyPartialSum, EmptySum,
+ [ -Occupied(m) for m in topology.ps ],
+ empty_count + 1
+ ).getConstraint())
+
+ for n in range(0, 7):
+ tile_count = assoc_get(n, board_input.counts)
+
+ TPSum = ruleset.VarSet('Tps_'+str(n),csolverlb, csolver, [
+ (0, tile_count+1), (0, slot_count) ])
+ TilePartialSum.append(TPSum)
+
+ TSum = ruleset.VarSet('Ts_'+str(n), csolverlb, csolver, [
+ (0, tile_count+1) ])
+
+ csolverlb.addConstraint(csolver, sumOfVariables(csolverlb, csolver,
+ TPSum, TSum,
+ [ Placement(csolverlb, csolver, elems,m,n) for m in topology.ps ],
+ tile_count + 1
+ ).getConstraint())
+ csolverlb.addConstraint(csolver, +TSum(tile_count).getConstraint() )
+
+ print 'Adding simmetry-breaking rules...'
+
+ def simmetry_is_preserved(xs, ys):
+ xys = zip(xs, ys)
+
+ for m in board_input.blocked_positions:
+ m_ = assoc_get(m, xys)
+ if m_ not in board_input.blocked_positions:
+ #print m, 'to', m_, 'simmetry not found'
+ return False
+
+ for (m,v) in board_input.fixed_positions:
+ m_ = assoc_get(m, xys)
+ if (m_,v) not in board_input.fixed_positions:
+ #print (m,v), 'to', (m_, v), 'simmetry not found'
+ return False
+ return True
+
+ def vars_from_sim(ms):
+ vs = []
+ for m in ms:
+ vs.append( +Occupied(m) )
+ vs.extend([ +Placement(csolverlb, csolver, elems,m,n) for n in range(0, 7) ])
+ return vs
+
+ simms = topology.simmetries()
+ sim0 = simms[0]
+ vsim0 = vars_from_sim(sim0)
+ for (i,sim1) in enumerate1( simms[1:] ):
+ if simmetry_is_preserved(sim0, sim1):
+ print ' (Simmetry #%s found!)'%(i)
+ vsim1 = vars_from_sim(sim0)
+ csolverlb.addConstraint(csolver, vectorLessThenOrEqual(csolverlb, csolver,
+ ruleset.VarSet('SimEq_'+str(i), csolverlb, csolver, [(0, len(vsim0))]),
+ vsim0,
+ vsim1
+ ).getConstraint())
+
+ print 'Converting rules to CNF form...'
+
+ return SATFormulation(
+ board_input,
+ ruleset,
+ topology,
+ elems
+ )
+
+
+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)
+
+ print '=== Initial input: ==='
+ formulation.board_input.print_to_stdout()
+
+ print '=== Solution ==='
+ print
+ print topology.print_in_hex(layout)
+
+########
+# Main
+########
+
+import sys
+
+def main():
+
+ if len(sys.argv) <= 1:
+ print "usage: ./hexiom_solve.py [0-40]"
+ exit(1)
+
+ level_no = int(sys.argv[1])
+
+ input_filename = LEVEL_INPUT_FILENAME_PATTERN(level_no)
+
+ with open(input_filename, 'r') as fil:
+ board_input = read_input(fil)
+
+ print '== Level to solve== '
+ board_input.print_to_stdout()
+ csolverlb = ps.loadCSolver();
+ csolver = csolverlb.createCCSolver()
+ formulation = SAT_formulation_from_board_input(board_input, csolverlb, csolver)
+
+ print '=== Done! Calling CSolver solver now ==='
+# csolverlb.serialize(csolver)
+ csolverlb.printConstraints(csolver)
+ if csolverlb.solve(csolver) != 1:
+ print '*** Got UNSAT result! ***'
+ sys.exit(1)
+ else:
+ print '** Solution found! ***'
+ print_board_from_assignments(csolverlb, csolver, formulation)
+
+if __name__ == '__main__':
+ main()
--- /dev/null
+4\r
+ 2 1 1 2\r
+ 3 3 3 . .\r
+ 2 3 3 . 4 .\r
+ . 2 . 2 4 3 2\r
+ 2 2 . . . 2\r
+ 4 3 4 . .\r
+ 3 2 3 3\r
+ \r
--- /dev/null
+5\r
+ +3 4 3 3+3\r
+ 4 4 3 2 4 5\r
+ . 3 3 2 4 4 3\r
+ 2 . 2 . . . . 2\r
++3 4 . . 4 3 5 4+3\r
+ 5 4 4 4 4 2 4 3\r
+ 3 3 . . . . 3\r
+ 5 3 5 4 . 4\r
+ +3 5 4 4+3\r
+ \r
--- /dev/null
+
+LEVEL_INPUT_FILENAME_PATTERN = (lambda n: 'levels/level%02d.txt' % n )
+SAT_INPUT_FILENAME_PATTERN = (lambda n: 'sat_in/level%02d.cnf' % n )
+SAT_OUTPUT_FILENAME_PATTERN = (lambda n: 'sat_out/level%02d.txt' % n )
+
+NAMED_CNF_INPUT_FILE = 'scratch/formula.txt'
+NAMED_CNF_RESULT_FILE = 'scratch/result.txt'
+
+import subprocess
+
+def in_file_out_file(exe_name):
+ ''' Run a minisat style solver'''
+ def solve(infilename, outfilename):
+ return subprocess.call(
+ [exe_name, infilename, outfilename]
+ )
+ return solve
+
+def in_file_out_pipe(exe_name):
+ ''' Run a precosat style solver'''
+ def solve(infilename, outfilename):
+ with open(outfilename, 'w') as fil:
+ return subprocess.call(
+ [exe_name, infilename],
+ stdout=fil
+ )
+ return solve
+
+#SAT_SOLVE = in_file_out_pipe('./lingeling')
+#SAT_SOLVE = in_file_out_file('./cryptominisat')
+SAT_SOLVE = in_file_out_file('./glucose_static')
--- /dev/null
+#! /usr/bin/python
+# - * - coding:utf-8 - * -
+
+############################################
+# CONFIGURATION
+############################################
+
+from hexiom_config import *
+
+############################################
+
+####
+# Helper functions
+###
+
+def sign(n):
+ if n < 0:
+ return -1
+ elif n == 0:
+ return 0
+ else: #n > 0
+ return +1
+
+def enumerate1(xs):
+ ''' (x1,x2...) -> ((1,x1), (2,x2),...) '''
+ for (i,x) in enumerate(xs):
+ yield (i+1, x)
+
+def concat(xss):
+ ''' [[a]] -> [a] '''
+ return [x for xs in xss for x in xs]
+
+def permutations(xs):
+ def go(i):
+ if i >= len(xs):
+ yield []
+ else:
+ for x in xs[i]:
+ for p in go(i+1):
+ yield [x] + p
+ return go(0)
+
+def assoc_list(xs):
+ return list(enumerate(xs))
+
+def assoc_get(x, xs):
+ for (k,v) in xs:
+ if k == x:
+ return v
+ return None
+
+##
+# Building rules
+#
+
+def size_of_dims(dims):
+ s = 1
+ for (minv, maxv) in dims:
+ if minv <= maxv:
+ s *= (maxv - minv + 1)
+ else:
+ s *= 0
+ return s
+
+def dim_multipliers(dims):
+ ''' mult[i] = size_of(dims[i+1:])'''
+
+ multipliers = [None] * len(dims)
+ multipliers[-1] = 1
+
+ for i in range(len(dims)-2, -1, -1):
+ (minv, maxv) = dims[i+1]
+ multipliers[i] = \
+ multipliers[i+1] * \
+ (maxv - minv + 1)
+
+ return multipliers
+
+class InvalidVariable(Exception):
+ pass
+
+
+class RuleSet(object):
+
+ def __init__(self):
+ self.vsets = []
+ self.vsets_by_name = {}
+ self.next_free_variable = 1
+
+ class Variable(object):
+ def __init__(self, vset, vs):
+ self.vset = vset
+ self.vs = vs
+
+ def __str__(self):
+ return self.vset.name + '(' + ' '.join(map(str,self.vs)) + ')'
+
+ def __eq__(self, b):
+ return (self.vset is b.vset) and (self.vs == b.vs)
+
+ def offsetOf(self):
+ return self.toInt() - self.vset.first_variable
+
+ def toInt(self):
+ return self.vset.indexOfVariable(self)
+
+ class VariableSet(object):
+ def __init__(self, ruleset, name, dims):
+ self.name = name
+
+ self.ndims = len(dims)
+ self.dims = dims
+
+ self.size = size_of_dims(dims)
+
+ self.multipliers = dim_multipliers(dims)
+
+ self.ruleset = ruleset
+ ruleset.vsets.append(self)
+
+ if ruleset.vsets_by_name.get(name):
+ 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
+
+ def __call__(self, *vs):
+ if self.ndims != len(vs):
+ raise InvalidVariable(
+ 'Expected %d dimensions, got %d'%(
+ self.ndims, len(vs))
+ )
+
+ for (val, (min_val, max_val)) in zip(vs, self.dims):
+ if not (min_val <= val <= max_val):
+ raise InvalidVariable(
+ 'Variable out of bounds:', self.name, vs, self.dims
+ )
+
+ return Lit(+1, RuleSet.Variable(self, vs) )
+
+ def contains(self, n):
+ return 0 <= (n-self.first_variable) < self.size
+
+ def indexOfVariable(self, var):
+ if var.vset is not self:
+ raise Exception('Converting variable at the wrong place')
+
+ return self.first_variable + sum([
+ (val - minv)*mult
+ for (val, (minv, maxv), mult) in
+ zip(var.vs, self.dims, self.multipliers)
+ ])
+
+ def valuesOfIndex(self, n):
+ offset = n - self.first_variable
+
+ vs = []
+ for mult in self.multipliers:
+ vs.append(offset//mult)
+ offset = offset%mult
+
+ return tuple(vs)
+
+ def VarSet(self, name, dims):
+ return RuleSet.VariableSet(self, name, dims)
+
+ def print_cnf_file(self, formulation, fil):
+ ruleset = formulation.ruleset
+ clauses = formulation.clauses
+
+ with open(NAMED_CNF_INPUT_FILE, 'w') as dbg:
+
+ print >> fil, 'p cnf', ruleset.next_free_variable -1 , len(clauses)
+ for (i,clause) in enumerate(clauses):
+ for lit in clause:
+ print >> dbg, lit,
+ print >> dbg
+
+ intClause = [lit.sign*lit.var.toInt() for lit in clause]
+ for lit in intClause:
+ print >> fil, lit,
+ print >> fil, '0'
+
+ nvars = self.next_free_variable - 1
+
+ def get_varset_by_name(self, name):
+ return self.vsets_by_name.get(name)
+
+ def get_varset_by_variable(self, n):
+ beg = 0
+ end = len(self.vsets)
+ while(beg < end):
+ m = (beg + end) // 2
+ vset = self.vsets[m]
+ if n < vset.first_variable:
+ end = m
+ elif n >= vset.first_variable + vset.size:
+ beg = m+1
+ else:
+ return vset
+ return None
+
+ def cnfVarToLit(self, lit_n):
+ sgn = (1 if lit_n >= 0 else -1)
+ n = abs(lit_n)
+ varset = self.get_varset_by_variable(n)
+ return Lit(
+ sgn,
+ RuleSet.Variable(varset, varset.valuesOfIndex(n))
+ )
+#####
+# Logical connectives
+####
+
+class Logic(object):
+ def __pos__(self):
+ return self
+
+class Lit(Logic):
+ def __init__(self, sign, var):
+ self.sign = sign
+ self.var = var
+
+ def __str__(self):
+ sgn = ('+' if self.sign > 0 else '-')
+ return sgn + str(self.var)
+
+ def __neg__(self):
+ return Lit(-self.sign, self.var)
+
+ def to_cnf(self):
+ return [[self]]
+
+class And(Logic):
+ def __init__(self, cs):
+ self.cs = cs
+
+ def __neg__(self):
+ return Or([-c for c in self.cs])
+
+ def to_cnf(self):
+ return concat(c.to_cnf() for c in self.cs)
+
+class Or(Logic):
+ def __init__(self, cs):
+ self.cs = cs
+
+ def __neg__(self):
+ return And([-c for c in self.cs])
+
+ def to_cnf(self):
+ return map(concat, permutations( [c.to_cnf() for c in self.cs] ) )
+
+def Implies(a,b):
+ return Or([-a, +b])
+
+def Equivalent(a,b):
+ return And([
+ Implies(a,b),
+ Implies(b,a)
+ ])
+
+def BruteForceOnlyOne(xs):
+ rs = [Or(xs)]
+ for (i,a) in enumerate(xs):
+ for (j,b) in enumerate(xs):
+ if (i != j):
+ rs.append( Implies(a, -b) )
+ return And(rs)
+
+def sumOfVariables(S, T, variables, maxk):
+ # S(k, i) = there are at leat k truthy values
+ # among the first i variables
+ # 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):
+ rules.append(Equivalent(
+ S(k, i),
+ Or([
+ S(k, i-1),
+ And([ variables[i-1], S(k-1, i-1) ])
+ ])
+ ))
+
+ ## T
+ for k in range(0, maxk):
+ rules.append(Equivalent(
+ T(k), And([S(k, n), -S(k+1, n)])
+ ))
+
+ rules.append(Equivalent(
+ T(maxk), S(maxk,n)
+ ))
+
+ return And(rules)
+
+def vectorLessThenOrEqual(E, xs, ys):
+ # n = len(xs) = len(ys)
+ # E_i, i in [0,n] := xs[0:i] == ys[0:i]
+
+ n = len(xs)
+
+ if(len(ys) != n):
+ raise Exception('Imcompatible vector lengths')
+
+ rules = []
+
+ ## Eq
+ rules.append( +E(0) )
+ for (i, (x, y)) in enumerate1(zip(xs, ys)):
+ rules.append(Equivalent(
+ E(i),
+ And([ E(i-1), Equivalent(x, y) ])
+ ))
+
+ ## x < y
+ for i in range(0,n):
+ rules.append(
+ Implies( E(i), Implies(xs[i], ys[i]) )
+ )
+
+ return And(rules)
+
+###########
+# Neighbours
+###########
+
+# Radial Hexagonal coordinates
+# (r, c, d)
+# r = distance from center
+# c = vértice associado
+# d = indice no lado (0 é o vértice, r-1 é o último)
+#
+# |0__ |1
+# / \
+# 5 --
+# -- 2
+# \ /
+# 4| __3|
+
+#Directional Hexagonal coordinates
+# (a,b)
+# / a
+# - b
+#
+# (-1,-1) (-1, 0)
+# ( 0,-1) ( 0, 0) ( 0, 1)
+# ( 1, 0) (1, 1)
+
+# Positional coordinates, as they come
+# from the input:
+#
+# 0 1
+# 2 3 4
+# 5 6
+
+#Simmetry functions
+
+def reflect_0_5((r, c, d)):
+ if r == 0 and c == 0 and d == 0:
+ return (0,0,0)
+ else:
+ if d == 0:
+ return (r, 5-c, 0)
+ else:
+ return (r, (10-c)%6, r-d)
+
+def clockwise_rotate(n, (r,c,d)):
+ if r == 0 and c == 0 and d == 0:
+ return (0,0,0)
+ else:
+ return (r, (c+n)%6, d)
+
+class HexTopology(object):
+ def __init__(self, side):
+ self.rcd_to_m = {}
+ self.ab_to_m = {}
+
+ self.side = side
+
+ self.rcds = []
+ self.abs = []
+ self.ps = []
+
+ m_ = [0]
+ a_ = [None]
+ b_ = [None]
+ def match(rcd):
+ m = m_[0]
+ ab = (a_[0], b_[0])
+
+ self.abs.append(ab)
+ self.rcds.append(rcd)
+ self.ps.append(m)
+
+ self.rcd_to_m[rcd] = m
+ self.ab_to_m[ab] = m
+
+ m_[0] += 1
+ b_[0] += 1
+ #print ''.join(map(str,rcd)),
+
+ radius = side-1
+
+ #top half
+ for r in range(radius, 0, -1):
+ a_[0] = -r
+ b_[0] = -radius
+ #print ' '*r,
+ for i in range(0, radius-r):
+ match((radius-i, 5, r))
+ for i in range(r):
+ match((r, 0, i))
+ for i in range(0, radius+1-r):
+ match((r+i, 1, i))
+ #print
+
+ #middle divider
+ a_[0] = 0
+ b_[0] = -radius
+ #print '',
+ for r in range(radius, 0, -1):
+ match((r, 5, 0))
+ if(radius >= 0):
+ match((0,0,0))
+ for r in range(1, radius+1):
+ match((r, 2, 0))
+ #iprint
+
+ #lower half
+ for r in range(1, radius+1):
+ a_[0] = r
+ b_[0] = -(radius-r)
+ #print ' '*r,
+ for i in range(0, radius+1-r):
+ match((radius-i, 4, radius-r-i))
+ for i in range(r):
+ match((r, 3, r-i-1))
+ for i in range(0, radius-r):
+ match((r+1+i, 2, r))
+ #print
+
+ def print_in_hex(self, xs):
+ xs = list(reversed(xs))
+ side = self.side
+ lines = []
+
+ def show(n):
+ return ('.' if n is None else str(n))
+
+ #upper half (with middle line)
+ for (i,a) in enumerate(range(1-side, 0+1)):
+ line = []
+ for b in range(1-side, i+1):
+ line.append(show(xs.pop()))
+ lines.append( ' '*(side-i-1) + ' '.join(line) )
+ #lower half (without middle line)
+ for (i,a) in enumerate1(range(1, side)):
+ line = []
+ for b in range(1-side+i, side):
+ line.append(show(xs.pop()))
+ lines.append( ' '*i + ' '.join(line) )
+ return '\n'.join(lines)
+
+ def hex_adjacency_graph(self):
+ adj_list = {}
+
+ def add(m, n):
+ adj_list[m].append(n)
+
+ def is_adj(m,n):
+ add(m, n)
+ if not adj_list.has_key(n):
+ adj_list[n] = []
+ add(n, m)
+
+ for h in self.abs:
+ (a,b) = h
+
+ if not adj_list.has_key(h):
+ adj_list[h] = []
+
+ for h_ in [
+ (a-1, b-1), (a-1, b),
+ (a, b+1)
+ ]:
+ if self.ab_to_m.get(h_) is not None:
+ is_adj(h, h_)
+
+ for lst in adj_list.values():
+ lst.sort()
+
+ return adj_list
+
+ def pos_adjacency_graph(self):
+ adj_list = {}
+
+ for (k, vs) in self.hex_adjacency_graph().iteritems():
+ adj_list[ self.ab_to_m[k] ] =\
+ [ self.ab_to_m[v] for v in vs]
+
+ return adj_list
+
+ def simmetries(self):
+ simmetries = []
+
+ def add_sim(rcds):
+ simmetries.append([
+ self.rcd_to_m[rcd]
+ for rcd in rcds
+ ])
+
+ for n in range(6):
+ add_sim([
+ clockwise_rotate(n, rcd)
+ for rcd in self.rcds
+ ])
+
+ for n in range(6):
+ add_sim([
+ reflect_0_5(clockwise_rotate(n, rcd))
+ for rcd in self.rcds
+ ])
+
+ return simmetries
+
+###########
+# Input
+###########
+
+import re
+
+class ProblemInput(object):
+ def __init__(self, side, counts, blocked_positions, fixed_positions, lines):
+ self.side = side
+ self.counts = counts
+ self.blocked_positions = blocked_positions
+ self.fixed_positions = fixed_positions
+ self.lines = lines
+
+ def print_to_stdout(self):
+ print self.side
+ for line in self.lines:
+ print line,
+
+def read_input(fil):
+ side = int(fil.readline())
+ counts = [0]*7
+ blocked_positions = []
+ fixed_positions = []
+
+ lines = []
+
+ m=0
+ for line in fil:
+ lines.append(line)
+ for match in re.finditer(r'(\+?)(\.|\d)', line):
+ locked = (match.group(1) == '+')
+ n = (None if match.group(2) == '.' else int(match.group(2)))
+
+ if n is not None:
+ counts[n] += 1
+
+ if locked:
+ if n is None:
+ blocked_positions.append(m)
+ else:
+ fixed_positions.append( (m, n) )
+
+ m += 1
+
+ return ProblemInput(
+ side,
+ assoc_list(counts),
+ blocked_positions,
+ fixed_positions,
+ lines
+ )
+
+####
+# Create clauses
+####
+
+class SATFormulation(object):
+ def __init__(self, board_input, ruleset, topology, clauses):
+ self.board_input = board_input
+ self.ruleset = ruleset
+ self.topology = topology
+ self.clauses = clauses
+
+def SAT_formulation_from_board_input(board_input):
+
+ ruleset = RuleSet()
+ topology = HexTopology(board_input.side)
+
+ # Schema
+ ########
+
+ slot_range = (0, topology.ps[-1])
+ slot_count = len(topology.ps)
+
+ value_range = (0, 6)
+
+ # (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])
+
+ # (m) = is the m-th tile occupied?
+ Occupied = ruleset.VarSet('O', [slot_range])
+
+ # (m)(k,i) = m-th slot has k occupied slots among its first i neighbours
+ NeighbourPartialSum = []
+
+ # (m)(k) = m-th slot has k occupied slots among its neighbours
+ NeighbourSum = []
+
+
+ # (n)(k,i) = there are k n-valued tiles on the first i slots?
+ TilePartialSum = []
+
+ # Rules
+ #######
+
+ print '== Creating CNF description of level'
+
+ rules = []
+
+ print 'Creating level-state rules...'
+
+ for (m, n) in board_input.fixed_positions:
+ rules.append( +Placement(m, n) )
+
+ for m in board_input.blocked_positions:
+ rules.append( -Occupied(m) )
+
+ print 'Creating tile placement rules...'
+
+ for m in topology.ps:
+ rules.append( BruteForceOnlyOne(
+ [-Occupied(m)] + [+Placement(m,n) for n in range(7)]
+ ))
+
+ adj_graph = topology.pos_adjacency_graph()
+
+ print 'Constraining number of neighbour of occupied tiles...'
+ #For each
+ for m in topology.ps:
+ vs = adj_graph[m]
+ nvs = len(vs)
+
+ NPSum = ruleset.VarSet('Nps_'+str(m),[
+ (0, nvs), (0, nvs) ])
+ NeighbourPartialSum.append(NPSum)
+
+ NSum = ruleset.VarSet('Ns_'+str(m), [
+ (0, nvs) ])
+ NeighbourSum.append(NSum)
+
+ rules.append(sumOfVariables(
+ NPSum, NSum,
+ [+Occupied(v) for v in adj_graph[m]],
+ None
+ ))
+ #Number of placement == SUM
+ for n in range(0, nvs+1):
+ rules.append(Implies(
+ Occupied(m),
+ Equivalent( +Placement(m,n), +NSum(n) )
+ ))
+
+ for n in range(nvs+1, 7):
+ rules.append( -Placement(m,n) )
+
+ print 'Creating constraints for the amount of tiles used...'
+
+ empty_count = len(topology.ps) - sum([c for (_,c) in board_input.counts])
+
+ # (k,i) = k empty slots among the first i slots
+ EmptyPartialSum = ruleset.VarSet('Eps', [
+ (0, empty_count+1), (0, slot_count) ])
+
+ EmptySum = ruleset.VarSet('Es', [
+ (0, empty_count+1)
+ ])
+
+ rules.append(sumOfVariables(
+ EmptyPartialSum, EmptySum,
+ [ -Occupied(m) for m in topology.ps ],
+ empty_count + 1
+ ))
+
+ for n in range(0, 7):
+ tile_count = assoc_get(n, board_input.counts)
+
+ TPSum = ruleset.VarSet('Tps_'+str(n),[
+ (0, tile_count+1), (0, slot_count) ])
+ TilePartialSum.append(TPSum)
+
+ TSum = ruleset.VarSet('Ts_'+str(n), [
+ (0, tile_count+1) ])
+
+ rules.append(sumOfVariables(
+ TPSum, TSum,
+ [ Placement(m,n) for m in topology.ps ],
+ tile_count + 1
+ ))
+ rules.append( +TSum(tile_count) )
+
+ print 'Adding simmetry-breaking rules...'
+
+ def simmetry_is_preserved(xs, ys):
+ xys = zip(xs, ys)
+
+ for m in board_input.blocked_positions:
+ m_ = assoc_get(m, xys)
+ if m_ not in board_input.blocked_positions:
+ #print m, 'to', m_, 'simmetry not found'
+ return False
+
+ for (m,v) in board_input.fixed_positions:
+ m_ = assoc_get(m, xys)
+ if (m_,v) not in board_input.fixed_positions:
+ #print (m,v), 'to', (m_, v), 'simmetry not found'
+ return False
+ return True
+
+ def vars_from_sim(ms):
+ vs = []
+ for m in ms:
+ vs.append( +Occupied(m) )
+ vs.extend([ +Placement(m,n) for n in range(0, 7) ])
+ return vs
+
+ simms = topology.simmetries()
+ sim0 = simms[0]
+ vsim0 = vars_from_sim(sim0)
+ for (i,sim1) in enumerate1( simms[1:] ):
+ if simmetry_is_preserved(sim0, sim1):
+ print ' (Simmetry #%s found!)'%(i)
+ vsim1 = vars_from_sim(sim0)
+ rules.append(vectorLessThenOrEqual(
+ ruleset.VarSet('SimEq_'+str(i), [(0, len(vsim0))]),
+ vsim0,
+ vsim1
+ ))
+
+ print 'Converting rules to CNF form...'
+
+ return SATFormulation(
+ board_input,
+ ruleset,
+ topology,
+ And(rules).to_cnf()
+ )
+
+
+def get_SAT_assignments(fil):
+ assignments = []
+ for line in fil:
+ if 'UNSAT' in line.upper():
+ return None
+ for word in line.split():
+ if re.match(r'-?\d+$', word):
+ n = int(word)
+ if n == 0:
+ return assignments
+ else:
+ assignments.append(n)
+ return assignments
+
+
+def print_board_from_assignments(formulation, assignments):
+
+ ruleset = formulation.ruleset
+ topology = formulation.topology
+
+ P = ruleset.get_varset_by_name('P')
+
+ layout = [None for p in topology.ps]
+ with open(NAMED_CNF_RESULT_FILE, 'w') as result:
+ for lit in assignments:
+ sgn = sign(lit)
+ var = abs(lit)
+
+ print >> result, ruleset.cnfVarToLit(lit)
+
+ if sgn > 0 and P.contains(var):
+ (m,n) = P.valuesOfIndex(var)
+ layout[m] = n
+
+ print '=== Initial input: ==='
+ formulation.board_input.print_to_stdout()
+
+ print '=== Solution ==='
+ print
+ print topology.print_in_hex(layout)
+
+########
+# Main
+########
+
+import sys
+
+def main():
+
+ if len(sys.argv) <= 1:
+ print "usage: ./hexiom_solve.py [0-40]"
+ exit(1)
+
+ level_no = int(sys.argv[1])
+
+ input_filename = LEVEL_INPUT_FILENAME_PATTERN(level_no)
+ cnf_in_filename = SAT_INPUT_FILENAME_PATTERN(level_no)
+ cnf_out_filename = SAT_OUTPUT_FILENAME_PATTERN(level_no)
+
+ with open(input_filename, 'r') as fil:
+ board_input = read_input(fil)
+
+ print '== Level to solve== '
+ board_input.print_to_stdout()
+
+ formulation = SAT_formulation_from_board_input(board_input)
+
+ print '=== Writing CNF to file ==='
+ with open(cnf_in_filename, 'w') as fil:
+ formulation.ruleset.print_cnf_file(formulation, fil )
+ print '=== Done! Calling SAT solver now ==='
+
+ SAT_SOLVE(cnf_in_filename, cnf_out_filename)
+
+ with open(cnf_out_filename, 'r') as fil:
+ assignments = get_SAT_assignments(fil)
+
+ if assignments is None:
+ print '*** Got UNSAT result! ***'
+ else:
+ print '** Solution found! ***'
+ print_board_from_assignments(formulation, assignments)
+
+if __name__ == '__main__':
+ main()
--- /dev/null
+2\r
+ . .\r
+ 1 . 1\r
+ . .\r
--- /dev/null
+2\r
+ . 1\r
+ . 1 1\r
+ 1 .\r
--- /dev/null
+3\r
+ 2 . 2\r
+ . 2 2 .\r
+ 2 2 . 2 2\r
+ . 2 2 .\r
+ 2 . 2\r
--- /dev/null
+3\r
+ 3 . 3\r
+ . . . .\r
+ 3 .+6 . 3\r
+ . . . .\r
+ 3 . 3\r
--- /dev/null
+3\r
+ . .+1\r
+ 2 . . .\r
+ . . 1 . .\r
+ . . . 2\r
+ +2 . .\r
--- /dev/null
+3\r
+ 2 . 2\r
+ 2 . . .\r
+ . .+. . 2\r
+ +1+. . 2\r
+ +.+1 .\r
--- /dev/null
+3\r
+ . 1 2\r
+ . .+0 1\r
+ . . . . .\r
+ 1+0 . .\r
+ 2 1 .\r
--- /dev/null
+3\r
+ 4 1 4\r
+ 1 . . 1\r
+ 4 . 6 . 4\r
+ 1 . . 1\r
+ 4 1 4\r
--- /dev/null
+3\r
+ 3 1 3\r
+ +1+.+. 4\r
+ .+. .+. 3\r
+ 2 .+.+1\r
+ . 2 .\r
--- /dev/null
+3\r
+ +.+. .\r
+ +. 0 . 2\r
+ . 1+2 1 .\r
+ 2 . 0+.\r
+ .+.+.\r
--- /dev/null
+3\r
+ 2 .+2\r
+ . 1+. .\r
+ 2 1+. 1 2\r
+ .+. 1 .\r
+ +2 . 2\r
--- /dev/null
+3\r
+ . . .\r
+ . . . .\r
+ 3 . 3 . .\r
+ 1 1 1 3\r
+ 4 3 1\r
--- /dev/null
+3\r
+ 3 2 .\r
+ 4 . . 2\r
+ 3 . . . 3\r
+ 2 . . 4\r
+ . 2 3\r
--- /dev/null
+3\r
+ . 3 .\r
+ . 4 . .\r
+ . . 3 . 2\r
+ 3 . . .\r
+ . 2 3\r
--- /dev/null
+3\r
+ 2 4 .\r
+ . 2 . 2\r
+ 2 2 2 . 3\r
+ . . . .\r
+ 3 3 3\r
--- /dev/null
+3\r
+ 4 . 2\r
+ . 0 3 .\r
+ . 0 5 4 .\r
+ 4 3 3 .\r
+ 3 2 5\r
--- /dev/null
+3\r
+ 2 . 1\r
+ 2+. 3 .\r
+ 2+. .+. 2\r
+ . 3+. 2\r
+ 1 . 2\r
--- /dev/null
+3\r
+ 3 5 4\r
+ 4 . 3 2\r
++3 4+. 3+3\r
+ . 1+. .\r
+ 3 2+.\r
--- /dev/null
+3\r
+ . 2 3\r
+ . 2 2 2\r
+ . 1 3 2 .\r
+ 2 2 3 .\r
+ 3 1 .\r
--- /dev/null
+3\r
+ . 5 4\r
+ . 2+.+1\r
+ . 3+2 3 .\r
+ +2+. 5 .\r
+ . 3 .\r
--- /dev/null
+3\r
+ . 2 .\r
+ 1 2 2 .\r
+ 2 2 2 2 .\r
+ 1 2 2 .\r
+ 3 3 .\r
--- /dev/null
+4\r
+ . . 2 3\r
+ . 2 4 3 2\r
+ . 2 2 . 3 .\r
+ . 2 2 3 2 2 .\r
+ . 3 . 2 2 .\r
+ 2 2 4 2 .\r
+ 3 2 . .\r
+ \r
--- /dev/null
+4\r
+ . . . 1\r
+ 1+.+.+. 1\r
+ 1+. . .+. 2\r
+ 1+. 0 . .+. 1\r
+ .+. . .+. 1\r
+ 2+.+.+. 1\r
+ 2 1 1 2\r
+ \r
--- /dev/null
+3\r
+ 4 2 3\r
+ 5 4 . 2\r
+ 3 . 4 4 4\r
+ . . . 5\r
+ 3 . 3\r
--- /dev/null
+3\r
+ 4 . .\r
+ . . 2 .\r
+ 4 3 2 . 4\r
+ 2 2 3 .\r
+ 4 2 4\r
--- /dev/null
+3\r
+ +. . 3\r
+ 2 2 1 4\r
+ 1 2 . . . \r
+ 2 4 3 4\r
+ 4 4+.\r
--- /dev/null
+3\r
+ +3 2 6\r
+ . .+4 3\r
+ 5 4 1 4 6\r
+ . 3+3 .\r
+ 3 1 .\r
--- /dev/null
+4\r
+ 2 2 3 4\r
+ 2 2 5 2 2\r
+ 3 5 . . 2 4\r
+ 4 2 . . .+. 3\r
+ 2 2 . .+. 3\r
+ 4+.+.+. .\r
+ 3 3 . .\r
+ \r
--- /dev/null
+4\r
+ . 4 6 .\r
+ 4 4 2 . 4\r
+ . 4 . 2 4 .\r
+ . . . . . . 4\r
+ 6 4 . 4 4 .\r
+ 4 . 2 . 4\r
+ . 2 . 4\r
+ \r
--- /dev/null
+4\r
+ 5 5 . .\r
+ 3 . 2+2 6\r
+ 3 . 2 . 5 .\r
+ . 3 3+4 4 . 3\r
+ 4 5 4 . 5 4\r
+ 5+2 . . 3\r
+ 4 . . .\r
+ \r
--- /dev/null
+3\r
+ 5 3 2\r
+ . . 3 2\r
+ 3 3 . . .\r
+ 3 4 3 5\r
+ 3 5 4\r
--- /dev/null
+4\r
+ +2 . 4+.\r
+ . 4 4 . 3\r
+ . 3 3 4 . .\r
++2 3 3+. 5 3+2\r
+ 2 . 4 4 4 3\r
+ 3 . . . 4\r
+ +. 3 .+2\r
+ \r
--- /dev/null
+4\r
+ +2 . 2 .\r
+ 3+5 . . 4\r
+ 3 2+4 3 4 4\r
+ 6 4 3+4 . . 3\r
+ 1 4 3+5 2 4\r
+ . . .+5 3\r
+ . 2 .+3\r
+ \r
--- /dev/null
+4\r
+ 4 2 4 2\r
+ . . .+. 3\r
+ 2+. .+. . 2\r
+ 4 2+. .+. 2 4\r
+ . 2+. .+. 2\r
+ 4+. 3 2 .\r
+ 2 . 2 4\r
+ \r
--- /dev/null
+4\r
+ . 3 . .\r
+ . 6 3 2 6\r
+ 6 3 4 . 4 4\r
+ . 6 . . . . .\r
+ 4 2 3 . 3 .\r
+ 3 . . . .\r
+ 4 4 . .\r
+ \r
--- /dev/null
+4\r
+ 2 1 1 2\r
+ 3 3 3 . .\r
+ 2 3 3 . 4 .\r
+ . 2 . 2 4 3 2\r
+ 2 2 . . . 2\r
+ 4 3 4 . .\r
+ 3 2 3 3\r
+ \r
--- /dev/null
+4\r
+ 1 4 . 1\r
+ 4 . 6 2 5\r
+ . 5 . 2 . 4\r
+ . 2 2 4+4 . .\r
+ 1 2+5 3 3 3\r
+ 5 2 . 4 .\r
+ 4 3 . 3\r
+ \r
--- /dev/null
+5\r
+ +3 4 3 3+3\r
+ 4 4 3 2 4 5\r
+ . 3 3 2 4 4 3\r
+ 2 . 2 . . . . 2\r
++3 4 . . 4 3 5 4+3\r
+ 5 4 4 4 4 2 4 3\r
+ 3 3 . . . . 3\r
+ 5 3 5 4 . 4\r
+ +3 5 4 4+3\r
+ \r
--- /dev/null
+5\r
+ 6 4+2 3 .\r
+ . 5 6+. 4 5\r
+ +2 . 2 2+. 3 3\r
+ .+. . 3 . . 2 4\r
+ 4 4+. 4 4 3+. 4 .\r
+ . 4 2 3 2 .+. .\r
+ 4 2+. . . .+2\r
+ 3 2+. 4 2 3\r
+ 4 3+2 3 4\r
+ \r
--- /dev/null
+6\r
+ 4 3 5 3 5 .\r
+ 4 4 2 4 5 . .\r
+ 4 4 4 2 . 4 . 5\r
+ 4 5 5 4 5 . 6 5 .\r
+ 3 . 5 3 4 4 . 3 6 3\r
+ . . 5 3 3 . 4 5 4 4 4\r
+ 5 6 4 4 4 4 . 6 5 5\r
+ 3 . 6 5 2 4 4 3 3\r
+ 5 5 5 . 5 4 5 5\r
+ 2 . 5 3 3 4 3\r
+ 6 4 4 4 4 4\r
+ \r
--- /dev/null
+Using an industrial-strength SAT solver to solve the Hexiom puzzle
+==================================================================
+
+Recently there was some talk on Reddit
+([here](http://www.reddit.com/r/programming/comments/p54v2/solving_hexiom_perhaps_you_can_help/) and
+[here](http://www.reddit.com/r/programming/comments/pjx99/solving_hexiom_using_constraints/)) about using custom algorithms to play
+[Hexiom](http://www.kongregate.com/games/Moonkey/hexiom), a cute little Flash puzzle game from Kongregate.
+
+The original submitter has published some solutions using traditional backtracking and exaustive search on [his repository](https://github.com/slowfrog/hexiom), but I wandered
+if I could do better then him by leveraging a Boolean Satisfability solver. In particular, one of the problem sets (level 38) would take hours to complete and I wanted to see if I could do better then that.
+
+Why bother with a SAT solver?
+-----------------------------
+
+Why should I complicate things with a SAT solver instead of tinkering with an existing backtracking solution? My motivations are basically that
+
+* Modern SAT solvers have very optimized and smart brute forcing engines. They can do many tricks that most people do not know about or do not go through the trouble of implementing most of the time:
+ * Non chronological backtracking (can go back multiple levels at once)
+ * Efficient data structures / watched literals (backtracking is O(1))
+ * Clause learning (avoids searching the same space multiple times)
+ * Random and aggressive restarts (avoids staying too long in a dead end)
+ * ...and much more!
+
+* SAT solver problem input is declarative so it is easy to add new rules and solving strategies without needing to rewrite the tricky backtracking innards.
+ * This will be particularly important when we get to the symmetry-breaking optimizations.
+
+Or in other words, SAT solvers are very fast and let me easily do things I would usually not try to do using a more traditional approach.
+
+My final results
+----------------
+
+In terms of speed, I **managed to solve the case that used to take hours in took hours in just over one minute**, while also still taking just a couple of seconds for the other easy problems.
+
+In terms of programming and algorithms, the good part is precisely that **I didn't have to do anything very special**.
+Besides encoding the problem using SAT, **the underlying algorithm is still exaustive backtracking, without any Hexiom-specific heuristics added<sup>1</sup>.**
+
+<sup>1</sup> (Well, one might try to count the symmetry-breaking as Hexiom-specific but the overall techinique is still pretty general...)
+
+-----------------------------
+
+How this all works
+==================
+
+The puzzle
+----------
+
+A Hexiom puzzle instance consists of an hexagonal playing field and a set of numbered, hexagonal, tiles. The objective consists in placing the tiles in slots on the board in such a way that the number on each tile corresponds to the amount of neighboring tiles it has.
+
+For example, level 8 presents the following initial placement of tiles (the dots represent empty board slots):
+
+ 4 1 4
+ 1 . . 1
+ 4 . 6 . 4
+ 1 . . 1
+ 4 1 4
+
+And has the following solution
+
+ 1 . 1
+ . 4 4 .
+ 1 4 6 4 1
+ . 4 4 .
+ 1 . 1
+
+Note how each **1** is surrounded by one other number, how each **4** is surrounded by four other numbers and how the **6** has a full set of 6 neighboring tiles around it.
+
+The Boolean Satisfiability Problem
+----------------------------------
+
+SAT solvers, as the name indicates, solve the [boolean satisfiability](https://en.wikipedia.org/wiki/Boolean_satisfiability_problem) problem. This problem consists of determining, given a set of boolean variables and a set of propositional predicates over these variables, whether there is a true-false assignment of the variables that satisfies all the predicates.
+
+For example, given variables `x`, `y`, and predicates
+
+ 1) (NOT x) OR y
+ 2) y OR z
+ 3) (NOT y) OR (NOT z)
+ 4) x
+
+We can produce the assignment {X=1, Y=1, Z=0} that satisfies all 4 clauses.
+
+However if where to add the 5-th clause
+
+ 5) (NOT x) OR z
+
+then there would be no solutions.
+
+Modeling Hexiom using as a SAT instance.
+----------------------------------------
+
+I used the following variable encodings to model the problem domain:
+
+* O<sub>m</sub> := The m-th slot of the board has a tile on it.
+* P<sub>m,n</sub> := There is a n-valued tile on the m-th slot on the board
+* N<sub>m,k</sub> := The m-th slot has k tiles neighboring it.
+* T<sub>n,k</sub> := There are k n-valued tiles placed on the board.
+* ... and other helper variables for the cardinality constraints, etc.
+
+From this on its a matter of writing the predicates:
+
+* General predicates to define the variables as we intend them to be. They are mostly shared by all Hexiom instances of the same hegagon side length:
+ * A cardinality constraint to say that a board slot is either empty or has a single slot on it
+ * Cardinality constraints to define N<sub>m,k</sub>
+ * Cardinality constraints to define T<sub>n,k</sub>
+
+* Level-dependant predicates, to describe the specific Hexiom level:
+ * Set T<sub>n,k</sub> according to the actual number ot tiles available.
+ * Set P<sub>m,n</sub> and O<sub>m</sub> for slots that come with preset values that cannot be changed.
+
+The only hard bit up to here is the cardinality constraints. For the small case (the rule for only a tile per slot) I " brute-forced" (O(n^2)) it and made a rule for each pair of variables saying at least one of them must be false.
+
+For the other cardinality constraints, I used an unary encoding, with helper variables such as `Nps(m, k, i) := There are at least k occupied tiles among the first i neighbors of tile m`. This gives a compact encoding, unlike the naïve version that lists all exponentialy-many possibilities.
+
+First results
+-------------
+
+With the initial description of the problem I already was already able to achieve results similar to those from the manually written backtracking search: all levels could be solved in under a couple of seconds, except for level 38, which took around half an hour to solve.
+
+Breaking symmetries
+-------------------
+
+The Hexiom instance that took the longest to solve was highly symmetrical so I suspected that the solver (and the backtracking-based approach) were wasting many cycles trying the same things multiple times (but in mirrored ways). I added *symmetry-breaking predicates* to rule out equivalent solutions from the search space.
+
+Hexagonal symmetries can be boiled down to the following 12 rotations and reflections (the 12 comes from 6 possible rotations times 2 for either doing a reflection or not):
+
+
+ Rotations
+
+ 1 2 6 1 5 6
+ 6 0 3 5 0 2 4 0 1 ... and 3 more ...
+ 5 4 4 3 4 2
+
+ Reflections
+
+ 1 6 6 5 5 4
+ 2 0 5 1 0 4 6 0 3 ... and 3 more ...
+ 3 4 2 3 1 2
+
+The trick behind writing a symmetry-breaking predicate is that if we arrange the variables corresponding to a solution in one of the permutations
+
+ VX = O(1), P(1, 1..6), O(2), P(2, 1..6), ..., O(6), P(6, 1..6)
+
+And the corresponding variables after a symmetric transformation (say a clockwise rotation of 1/6th of a turn)
+
+ VY = O(2), P(2, 1..6), O(3), P(3, 1..6), ..., O(1), P(1, 1..6)
+
+It is clear that given a satisfying assignment in VX we can find a symmetric assignment via VY. By imposing an arbitrary total order on these assignments we can force it so that only one of them is allowed (saving the SAT solver from exploring its reflections multiple times). The standard way to do this is to think of VX and VY as bit vectors representing integers and then write predicates that state the equivalent of `VX <= VY`.
+
+----------------------
+
+How do I run this thing then?
+=============================
+
+ python hexiom_solve.py NN
+
+Where NN is a number from 0 to 40 standing for the number of the level you want to solve. It will use an input file from the levels folder I copied from Slowfrog's project.
+
+Where do I get a SAT solver?
+=============================
+
+I am including copies of some SAT solver executables in this repo but I am not sure they will work on other computers and platforms.
+
+In any case, the hexiom solver was designed to be able to handle any SAT solver that uses the relatively standard DIMACS input and output formats. You can find a good selection of state of the art solvers in the websites of the annual [SAT Competition](http://satcompetition.org/).
+
+[Page of the SAT competition with links to the solver websites](http://www.cril.univ-artois.fr/SAT11/)
+
+Here are some of the best preforming SAT solvers from last year if you want to check them out:
+
+* [Glucose](http://www.lri.fr/~simon/?page=glucose) - [Source link](http://www.lri.fr/~simon/downloads/glucose-2-compet.tgz)
+* [Cryptominisat](http://www.msoos.org/cryptominisat2/) - [Source Link](https://gforge.inria.fr/frs/download.php/30138/cryptominisat-2.9.2.tar.gz)
+* [Lingeling](http://fmv.jku.at/lingeling/) - [Source Link](http://fmv.jku.at/lingeling/lingeling-587f-4882048-110513.tar.gz)
+
+As far as compiling goes, all the solvers I linked to are written in C or C++ and all of them come with an easy to use makefile or build script.
--- /dev/null
+#!/bin/bash
+
+export PYTHONPATH=./csolver
+export LD_LIBRARY_PATH=./csolver
+# For Mac OSX
+export DYLD_LIBRARY_PATH=./csolver
+# For sat_solver
+export PATH=./csolver:.:$PATH
+
+$@
projects / Benchmarks_CSolver.git / commitdiff