@@ -741,19 +741,36 @@ def MapColoringSAT(colors, neighbors):
741
741
if isinstance (neighbors , str ):
742
742
neighbors = parse_neighbors (neighbors )
743
743
colors = UniversalDict (colors )
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 ))
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 )
757
774
758
775
759
776
australia_sat = MapColoringSAT (list ('RGB' ), """SA: WA NT Q NSW V; NT: WA Q; NSW: Q V; T: """ )
0 commit comments