@@ -741,36 +741,19 @@ def MapColoringSAT(colors, neighbors):
741741 if isinstance (neighbors , str ):
742742 neighbors = parse_neighbors (neighbors )
743743 colors = UniversalDict (colors )
744- part = str ()
745- t = str ()
746- for x in neighbors .keys ():
747- part += '('
748- l = 0
749- for c in colors [x ]:
750- l += 1
751- part += str (x ) + '_' + str (c )
752- t += str (x ) + '_' + str (c )
753- if l != len (colors [x ]):
754- part += ' | '
755- t += '|'
756- part += ') & '
757- list = t .split ('|' )
758- t = str ()
759- for idx , val in enumerate (list ):
760- for x in list [idx + 1 :]:
761- part += '~(' + val + ' & ' + x + ') & '
762- not_part = str ()
763- visit = set ()
764- for x in neighbors .keys ():
765- adj = set (neighbors [x ])
766- adj = adj - visit
767- visit .add (x )
768- for n in adj :
769- for col in colors [n ]:
770- not_part += '~(' + str (x ) + '_' + str (col ) + ' & '
771- not_part += str (n ) + '_' + str (col ) + ') & '
772- clause = part + not_part [:len (not_part ) - 2 ]
773- return expr (clause )
744+ clauses = []
745+ for state in neighbors .keys ():
746+ clause = [expr (state + '_' + c ) for c in colors [state ]]
747+ clauses .append (clause )
748+ for t in itertools .combinations (clause , 2 ):
749+ clauses .append ([~ t [0 ], ~ t [1 ]])
750+ visited = set ()
751+ adj = set (neighbors [state ]) - visited
752+ visited .add (state )
753+ for n_state in adj :
754+ for col in colors [n_state ]:
755+ clauses .append ([expr ('~' + state + '_' + col ), expr ('~' + n_state + '_' + col )])
756+ return associate ('&' , map (lambda c : associate ('|' , c ), clauses ))
774757
775758
776759australia_sat = MapColoringSAT (list ('RGB' ), """SA: WA NT Q NSW V; NT: WA Q; NSW: Q V; T: """ )
0 commit comments