SHARE
TWEET

laba

a guest Sep 20th, 2019 64 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. from pysat.solvers import Glucose3
  2. import sys
  3.  
  4. import_file = sys.argv[1]
  5.  
  6. def transform_index(N, k, v):
  7.   return N * (k - 1) + v
  8.  
  9. def transform(edges, N, M, K):
  10.   clauses = []
  11.   for i in range(1, N + 1):
  12.     to_add = []
  13.     for k in range(1, K + 1):
  14.       to_add.append(transform_index(N, k, i))
  15.     clauses.append(to_add)
  16.  
  17.   #now edges
  18.   for edge in edges:
  19.     u, v = edge
  20.     for k in range(1, K + 1):
  21.       clauses.append([-transform_index(N, k, edge[0]), -transform_index(N, k, edge[1])])
  22.   return clauses
  23.  
  24.  
  25. with open (import_file, "r") as f:
  26.   n, m = map(int, f.readline().split())
  27.   edges = []
  28.   for i in range(m):
  29.     u, v = map(int, f.readline().split())
  30.     edges.append([u, v])
  31.   for c in range(1, n + 1):
  32.     slv = Glucose3()
  33.     clauses = transform(edges, n, m, c)
  34.     for item in clauses:
  35.       slv.add_clause(item)
  36.     if slv.solve():
  37.       print(c)
  38.       cnt = 0
  39.       for elem in slv.get_model():
  40.         if elem > 0:
  41.            print(elem % c + 1, end=' ')
  42.       print('\n')
  43.       break
RAW Paste Data
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
 
Top