API tools faq
paste
Advertisement
Guest User

Untitled

a guest
Oct 27th, 2016
60
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 13.99 KB | None | 0 0
raw download clone embed print report
  1. from collections import OrderedDict
  2. import os
  3. import subprocess
  4. import sys
  5. import multiprocessing
  6. import itertools
  7.  
  8.  
  9. def split_seq(iterable, size):
  10. it = iter(iterable)
  11. item = list(itertools.islice(it, size))
  12. while item:
  13. yield item
  14. item = list(itertools.islice(it, size))
  15.  
  16.  
  17. class buffered_subprocess_handler(object):
  18. def __init__(self):
  19. self.bu = []
  20.  
  21. def write(self, s):
  22. self.bu.append(s)
  23.  
  24. def close(self):
  25. pass
  26.  
  27. def get_stdout(self):
  28. self.proc = subprocess.Popen(['./cryptominisat5_simple'], stdout=subprocess.PIPE, stdin=subprocess.PIPE)
  29. return self.proc.communicate(''.join(self.bu))[0]
  30.  
  31.  
  32. class subprocess_handler(object):
  33. def __init__(self):
  34. self.proc = subprocess.Popen(['./cryptominisat5_simple'], stdout=subprocess.PIPE, stdin=subprocess.PIPE)
  35. self.r = self.proc.stdin
  36.  
  37. def write(self, s):
  38. try:
  39. for i in range(0, len(s), 128):
  40. self.r.write(s[i:i+128])
  41. # self.r.write(s)
  42. except:
  43. print s
  44. raise
  45.  
  46. def close(self):
  47. pass
  48.  
  49. def get_stdout(self):
  50. return self.proc.communicate()[0]
  51.  
  52.  
  53. class SATGenerator(object):
  54. def __init__(self, traces, maxx, maxy, maxz):
  55.  
  56. all_coords = [traces[t][io] for t in traces for io in traces[t]]
  57. duped_coords = list(all_coords) ; [duped_coords.remove(t) for t in set(all_coords)]
  58. assert len(set(all_coords)) == len(all_coords), 'coords duplicated: {}'.format(duped_coords)
  59.  
  60. self.maxx = maxx
  61. self.maxy = maxy
  62. self.maxz = maxz
  63. self.xrange = range(self.maxx)
  64. self.yrange = range(self.maxy)
  65. self.zrange = range(self.maxz)
  66.  
  67. self.vars_per_plane = maxx * maxy
  68.  
  69. self.output_path = 'output.cnf'
  70. self.vars = []
  71. self.traces = traces
  72. self.traces_keys = self.traces.keys()
  73. self.toti = (len(self.traces) * self.maxx * self.maxy * self.maxz)
  74. self.tot = float(len(self.traces) * self.maxx * self.maxy * self.maxz)
  75.  
  76.  
  77. self.setup_output()
  78. print('setup output done')
  79. print('creating vars')
  80. self.create_vars()
  81. print('creating clauses')
  82. self.create_clauses()
  83. print('solving')
  84. self.solve()
  85.  
  86. def setup_output(self):
  87. # self.output = open(self.output_path, 'w')
  88. #self.output = buffered_subprocess_handler()
  89. self.output = subprocess_handler()
  90. self.output.write('p cnf 0 0{}'.format(os.linesep))
  91.  
  92. def solve(self):
  93. self.output.close()
  94. # proc = subprocess.Popen(['./cryptominisat5', self.output_path], stdout=subprocess.PIPE)
  95. # stdout, stderr = self.proc.communicate()
  96. stdout = self.output.get_stdout()
  97. stdout = stdout.strip()
  98. with open('solver_out', 'w') as so:
  99. so.write(stdout)
  100. if stdout.endswith('UNSATISFIABLE'):
  101. print 'FAILED'
  102. sys.exit(1)
  103. else:
  104. print('solved')
  105. sol = []
  106. for line in stdout.split('\n'):
  107. if not line.startswith('v'):
  108. continue
  109. # print 'line is: {}'.format(line)
  110. for chunk in line[1:].split():
  111. # print chunk
  112. if not chunk.startswith('-') and not chunk.strip() == '0':
  113. m, x, y, z, trace = self.vars[int(chunk)-1]
  114. sol.append((trace, x, y, z))
  115. print m
  116. o = open('sol_out', 'w')
  117. l = ''
  118. for trace in list(self.traces) + ['SE']:
  119. if len(trace) > len(l):
  120. l = trace
  121. l = len(l)
  122.  
  123. for trace in self.traces:
  124. o.write('\n trace OUT\n')
  125. for z in range(self.maxz):
  126. o.write('Z {}\n'.format(z))
  127. for x in range(self.maxx):
  128. for y in range(self.maxy):
  129. #for x in self.locations_traces[trace]:
  130. # for y in self.locations_traces[trace][x]:
  131. if (trace, x, y, z) in self.start_end:
  132. o.write('SE{} '.format(' ' * (l - 2)))
  133. elif (trace, x, y, z) in sol:
  134. o.write('{}{} '.format(trace, ' ' * (l - len(trace))))
  135. else:
  136. o.write('0{} '.format(' ' * (l - 1)))
  137. o.write('\n')
  138. o.write('\n')
  139. o.close()
  140.  
  141. def var(self, name):
  142. self.vars.append(name)
  143. return self.num_vars
  144.  
  145. @property
  146. def num_vars(self):
  147. return len(self.vars)
  148.  
  149. def locations_traces(self, trace, x, y, z):
  150. traces_offset = (self.vars_per_plane * self.maxz * self.traces_keys.index(trace))
  151. z_offset = z
  152. per_plane_offsett = (y ) + ((self.maxz-1)*y) + z + (x * self.maxy * self.maxz)
  153.  
  154. ret = traces_offset + per_plane_offsett + 1
  155. #self.locations_traces_check(trace, x, y, z, ret,traces_offset,z_offset,per_plane_offsett)
  156. return ret
  157.  
  158. def locations_traces_check(self, trace, x, y, z, other,traces_offset, z_offset, per_plane_offsett):
  159. i=0
  160. for _trace in self.traces_keys:
  161. # print('{} '.format(_trace))
  162. # trace_xyz = OrderedDict()
  163. for _x in range(self.maxx):
  164. # ys = OrderedDict()
  165. for _y in range(self.maxy):
  166. # zs = OrderedDict()
  167. for _z in range(self.maxz):
  168. # print('{} {} {} {} {}'.format(_trace, _x, _y, _z, i))
  169. i+=1
  170. if (trace, x, y, z) == (_trace, _x, _y, _z):
  171. assert i == other, '\nx {} y {} z {}\ni {} - other {} - traces_offset {} - z_offset {} - per_plane_offsett {}\n _trace {} trace {}'.format(_x, _y, _z, i, other,traces_offset, z_offset, per_plane_offsett, _trace, trace)
  172. break
  173.  
  174. # break
  175. # print('done check')
  176. # sys.exit(1)
  177.  
  178. def create_vars(self):
  179. # setup location grid
  180. # self.locations_traces = OrderedDict()
  181. for trace in self.traces:
  182. # trace_xyz = OrderedDict()
  183. for x in self.xrange:
  184. # ys = OrderedDict()
  185. for y in self.yrange:
  186. # zs = OrderedDict()
  187. for z in self.zrange:
  188. v = self.var(('x {} y {} z {} was utilized by trace {}'.format(x, y, z, trace),x, y, z, trace))
  189. print('{}%'.format(self.locations_traces(trace, x, y, z)/self.tot))
  190.  
  191. # zs[z] = v
  192. # ys[y] = zs
  193. # trace_xyz[x] = ys
  194. # self.locations_traces[trace] = trace_xyz
  195.  
  196. def create_clauses(self):
  197. # for every space
  198. print(' * one trace per voxel')
  199. #q = multiprocessing.Queue()
  200. #p = multiprocessing.Pool(4)
  201. def mp_worker(xs, qq):
  202. for x in xs:
  203. for y in self.yrange:
  204. for z in self.zrange:
  205. locs = []
  206. # for every trace
  207. for trace in self.traces:
  208. _loc = self.locations_traces(trace, x, y, z)
  209. locs.append(_loc)
  210. # allow only one trace in this space
  211. #self._naive_mutex_q(locs, qq)
  212. self._naive_mutex(locs)
  213. #print('{}%'.format(self.locations_traces(self.traces_keys[0], x, y, z)/self.tot))
  214. mp_worker(self.xrange, None)
  215. #p.map(mp_worker, [(seq,q) for seq in split_seq(self.xrange, 4)])
  216. #while True:
  217. # item = q.get()
  218. # if item is None:
  219. # break
  220. # self.output.write(item)
  221.  
  222. # for every start and end, require at least one neighbor
  223. print(' * start/end')
  224. self.start_end = []
  225. for trace in self.traces:
  226. for io in ['input', 'output']:
  227. x,y,z = self.traces[trace][io]
  228. v = self.locations_traces(trace, x, y, z)
  229. self.comment('{} at x {} y {} z {}'.format(io, x, y, z))
  230. self.clause([v])
  231. self._neighbor_constraint(trace, x, y, z)
  232. self.start_end.append((trace, x, y, z))
  233. #self.output.ttt= True
  234. print(' * neighbor per trace per voxel')
  235. for trace in self.traces:
  236. for x in self.xrange:
  237. for y in self.yrange:
  238. for z in self.zrange:
  239. if (trace, x, y, z) in self.start_end:
  240. continue
  241. self._two_neighbor_constraint(trace, x, y, z)
  242. print('{}%'.format(self.locations_traces(trace, x, y, z)/self.tot))
  243.  
  244.  
  245. def clause(self, v_list):
  246. svs = [str(v) for v in v_list]
  247. self.output.write('{} 0{}'.format(' '.join(svs), os.linesep))
  248.  
  249. def comment(self, comment):
  250. self.output.write('c {}{}'.format(comment, os.linesep))
  251.  
  252. def _kleiber_kwon(self, vs):
  253. pass
  254.  
  255. def _naive_mutex_q(self, vs, q, cmdr_list=None):
  256. self.output.w = self.output.write
  257. self.output.write = q.put
  258. self._naive_mutex(vs, cmdr_list)
  259. self.output.write = self.output.w
  260.  
  261. def _naive_mutex(self, vs, cmdr_list=None):
  262. self.comment('_naive_mutex to follow{}'.format(' with cmdrs {} and {}'.format(cmdr_list, vs) if cmdr_list is not None else ''))
  263. pre = cmdr_list if cmdr_list is not None else []
  264. for i, vi in enumerate(vs):
  265. if (i+1)>=len(vs):
  266. continue
  267. for vj in vs[i+1:]:
  268. self.clause((pre) + [-vi, -vj])
  269. self.comment('_naive_mutex finished')
  270.  
  271. def _neighbor_constraint(self, trace, x, y, z):
  272. try:
  273. v = self.locations_traces(trace, x, y, z)
  274. except:
  275. print self.locations_traces.keys()
  276. raise
  277. # if v is utilized, then any of the following can be true
  278. nvs = [-v]
  279. ensure = 3+2+3
  280. # for xx in [x-1,x,x+1]:
  281. # if xx<0 or xx>=self.maxx:
  282. # ensure = None
  283. # continue
  284. # for yy in [y-1,y,y+1]:
  285. # if yy<0 or yy>=self.maxy:
  286. # ensure = None
  287. # continue
  288. # for zz in [z-1,z,z+1]:
  289. # if xx<0 or xx>=self.maxx or yy<0 or yy>=self.maxy or zz<0 or zz>=self.maxz:
  290. # ensure = None
  291. # continue
  292. # if x==xx and y==yy and z==zz:
  293. # continue
  294. # # if x==xx and y==yy and z==zz:
  295. # # continue
  296. # nvs.append(self.locations_traces[trace][xx][yy][zz])
  297. nvs += self._get_circumferential_locs(trace, x, y, z)
  298. # if ensure is not None:
  299. # assert nvs == ensure+1, 'nvs was {}'.format(nvs)
  300. self.comment('if v {} then any neighbor for trace {} xyz {} {} {}'.format(v, trace, x, y, z))
  301. self.clause(nvs)
  302. # it can only go in one direction
  303. # self._naive_mutex(nvs[1:])
  304.  
  305. def _two_neighbor_constraint(self, trace, x, y, z):
  306. try:
  307. v = self.locations_traces(trace, x, y, z)
  308. except:
  309. print self.locations_traces.keys()
  310. raise
  311. # if v is utilized, then any of the following can be true
  312. nvs = [-v]
  313.  
  314. circumferential_locs = self._get_circumferential_locs(trace, x, y, z)
  315. for cl in circumferential_locs:
  316. others = list(circumferential_locs); others.remove(cl)
  317. # if v and cl, then one of the others
  318. self.clause([-cl, -v] + others)
  319. self._naive_mutex(others, cmdr_list=[-cl, -v])
  320. nvs.append(cl)
  321.  
  322. self.comment('if v {} then any neighbor for trace {} xyz {} {} {}'.format(v, trace, x, y, z))
  323. self.clause(nvs)
  324. # it can only go in one direction
  325. # self._naive_mutex(nvs[1:])
  326.  
  327. def _get_circumferential_locs(self, trace, x,y,z):
  328. #ensure = 3+2+3
  329. nvs = []
  330.  
  331. #disallow_fortyfives = True
  332.  
  333. for xx in [x-1,x,x+1]:
  334. if xx<0 or xx>=self.maxx:
  335. #ensure = None
  336. continue
  337. for yy in [y-1,y,y+1]:
  338. if yy<0 or yy>=self.maxy:
  339. #ensure = None
  340. continue
  341. for zz in [z-1,z,z+1]:
  342. if xx<0 or xx>=self.maxx or yy<0 or yy>=self.maxy or zz<0 or zz>=self.maxz:
  343. #ensure = None
  344. continue
  345. if x==xx and y==yy and z==zz:
  346. continue
  347. # restrict vias to vertical Z transitions only
  348. if (xx!=x or yy!=y) and zz!=z:
  349. continue
  350. # if disallow_fortyfives:
  351. if abs(xx-x) == 1 and abs(yy-y) == 1:
  352. continue
  353.  
  354. nvs.append(self.locations_traces(trace, xx ,yy ,zz))
  355. #if ensure is not None:
  356. # assert nvs == ensure, 'nvs was {}'.format(nvs)
  357. return nvs
  358.  
  359.  
  360.  
  361. # traces = OrderedDict([('t1', {'input': (0,0,0),
  362. # 'output': (10,10,0)}),
  363. # ('t2', {'input': (0,10,0),
  364. # 'output': (10,1,0)}),
  365. # ('t3', {'input': (0,0,0),
  366. # 'output': (10,10,1)}),
  367. # ('t4', {'input': (1,3,0),
  368. # 'output': (10,4,0)})])
  369. traces = OrderedDict([('t1', {'input': (0,1,0),
  370. 'output': (10,10,0)}),
  371. ('t2', {'input': (0,10,0),
  372. 'output': (10,1,0)}),
  373. ('t3', {'input': (0,0,0),
  374. 'output': (10,10,1)}),
  375. ('t4', {'input': (1,3,0),
  376. 'output': (10,4,0)})])
  377. SATGenerator(traces, maxx = 20, maxy = 20, maxz = 2)
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!