laba

from pysat.solvers import Glucose3
import sys

import_file = sys.argv[1]

def transform_index(N, k, v):
  return N * (k - 1) + v

def transform(edges, N, M, K):
  clauses = []
  for i in range(1, N + 1):
    to_add = []
    for k in range(1, K + 1):
      to_add.append(transform_index(N, k, i))
    clauses.append(to_add)

  #now edges
  for edge in edges:
    u, v = edge
    for k in range(1, K + 1):
      clauses.append([-transform_index(N, k, edge[0]), -transform_index(N, k, edge[1])])
  return clauses


with open (import_file, "r") as f:
  n, m = map(int, f.readline().split())
  edges = []
  for i in range(m):
    u, v = map(int, f.readline().split())
    edges.append([u, v])
  for c in range(1, n + 1):
    slv = Glucose3()
    clauses = transform(edges, n, m, c)
    for item in clauses:
      slv.add_clause(item)
    if slv.solve():
      print(c)
      cnt = 0
      for elem in slv.get_model():
        if elem > 0:
           print(elem % c + 1, end=' ')
      print('\n')
      break