#!/usr/bin/env python3 # -*- coding: utf-8 -*- import my_utils, SAT_lib import sys, re VERTICES=50 s=SAT_lib.SAT_lib(maxsat=True) f=open(sys.argv[1],"r") vertices=[s.create_var() for v in range(VERTICES)] # as much verties, as possible: for v in range(VERTICES): s.fix_soft_always_true(vertices[v], 1) edges=set() while True: raw=f.readline() l=raw.rstrip () if len(l)==0: break m=re.search('UndirectedEdge\[(.*), (.*)\]', l) if m!=None: v1=int(m.group(1))-1 v2=int(m.group(2))-1 edges.add((v1,v2)) edges.add((v2,v1)) for i in range(VERTICES): for j in range(VERTICES): if i==j: continue if (i,j) not in edges: # if there is no edge between a pair of vertices, # these two vertices cannot be included in the solution simultaneously: s.add_clause([s.neg(vertices[i]), s.neg(vertices[j])]) f.close() print ("first 10 solutions:") cnt=0 while s.solve(): solution=[] for v in range(VERTICES): val=s.get_var_from_solution(vertices[v]) if val!=0: solution.append(v+1) print (f"clique size {len(solution)}: {solution}") cnt+=1 if cnt==10: break s.add_negated_solution_as_clause()